Threshold normalization for MCSP

This module caps binary MCSP thresholds at a concrete unconditional truth-table-size bound, proves that the cap preserves membership, and derives a raw-witness length bound that is polynomial in encoded instance length.

theorem Complexity.MCSP.Instance.arity_le_tableLength (arity : ℕ) : arity ≤ 2 ^ arity

Function arity never exceeds its truth-table length.

theorem Complexity.MCSP.Instance.exists_circuit_size_le_trivialCircuitSizeBound (inst : Instance) [NeZero inst.arity] : ∃ (internalGates : ℕ) (circuit : Circuit Basis.andOr2 inst.arity 1 internalGates), circuit.size ≤ inst.trivialCircuitSizeBound ∧ circuit.Computes inst.function

Every Boolean function has an andOr2 circuit within the chosen coarse truth-table-square bound.

theorem Complexity.MCSP.Instance.hasCircuitAtMost_trivialCircuitSizeBound (inst : Instance) : (inst.withThreshold inst.trivialCircuitSizeBound).HasCircuitAtMost

The unconditional bound itself always makes an instance a yes-instance, including the explicit zero-arity case.

theorem Complexity.MCSP.Instance.effectiveThreshold_le_threshold (inst : Instance) : inst.effectiveThreshold ≤ inst.threshold

The effective threshold never exceeds the threshold supplied in the input.

theorem Complexity.MCSP.Instance.effectiveThreshold_le_trivialCircuitSizeBound (inst : Instance) : inst.effectiveThreshold ≤ inst.trivialCircuitSizeBound

The effective threshold never exceeds the unconditional circuit bound.

theorem Complexity.MCSP.Instance.hasCircuitAtMost_normalizeThreshold_iff (inst : Instance) : inst.normalizeThreshold.HasCircuitAtMost ↔ inst.HasCircuitAtMost

Capping an oversized threshold preserves MCSP yes/no semantics exactly.

theorem Complexity.MCSP.Instance.trivialCircuitSizeBound_le_encodeLength (inst : Instance) : inst.trivialCircuitSizeBound ≤ (inst.encode.length + 2) ^ 2

The unconditional cap is at most a square in total encoded input length.

theorem Complexity.MCSP.Instance.IsRawCircuitWitness.normalizeThreshold_length_le_encode (inst : Instance) {code : List Bool} (hwitness : inst.normalizeThreshold.IsRawCircuitWitness code) : code.length ≤ rawWitnessLengthPolynomial inst.encode.length

Every witness accepted against the normalized threshold has length bounded by the fixed polynomial in the original canonical instance-code length.

theorem Complexity.MCSP.Instance.rawWitnessLengthPolynomial_polyBound : PolyBound rawWitnessLengthPolynomial

The normalized raw-witness envelope is pointwise polynomially bounded.

theorem Complexity.MCSP.Instance.exists_isRawCircuitWitness_length_le_encode (inst : Instance) (hsmall : inst.HasCircuitAtMost) : ∃ (code : List Bool), inst.IsRawCircuitWitness code ∧ code.length ≤ rawWitnessLengthPolynomial inst.encode.length

Every MCSP yes-instance has a canonical raw-circuit witness whose code length is bounded by one fixed polynomial in the encoded instance length.

theorem Complexity.MCSP.rawWitnessRelation_polyBalanced : PolyBalanced RawWitnessRelation

The normalized raw-circuit relation is polynomially balanced: every accepted witness, not merely one selected witness, has polynomial length.

theorem Complexity.MCSP.mem_MCSP_iff_exists_rawWitnessRelation (bits : List Bool) : bits ∈ MCSP ↔ ∃ (witness : List Bool), RawWitnessRelation bits witness

MCSP membership is exactly existential acceptance by the normalized raw circuit witness relation, with malformed inputs rejected on both sides.