Threshold normalization for MCSP -- proof internals

The proof uses the library's explicit DNF circuit over unbounded AND/OR and its verified gate-chain compilation to Basis.andOr2. The resulting coarse square bound is sufficient to make canonical raw witnesses polynomial in truth-table input length.

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

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

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

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

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

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

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

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

theorem Complexity.MCSP.Instance.rawWitnessLengthPolynomial_polyBound_internal : PolyBound rawWitnessLengthPolynomial

theorem Complexity.MCSP.rawWitnessRelation_polyBalanced_internal : PolyBalanced RawWitnessRelation

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

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