Threshold slices of MCSP

This module exposes the arity-indexed language MCSP.atThreshold s and its canonical total re-encoding map. The exact length theorem retains the binary width of both the old and new threshold rather than hiding it in asymptotic notation.

@[simp]

theorem Complexity.MCSP.Instance.minimumSize_withThreshold (inst : Instance) (threshold : ℕ) : (inst.withThreshold threshold).minimumSize = inst.minimumSize

Changing an instance threshold preserves its minimum circuit size.

theorem Complexity.MCSP.decode?_rethreshold_of_decode?_eq_some (threshold : ℕ → ℕ) {bits : List Bool} {inst : Instance} (hdecode : Instance.decode? bits = some inst) : Instance.decode? (rethreshold threshold bits) = some (inst.withThreshold (threshold inst.arity))

Rethresholding a decodable code produces the corresponding canonical code.

@[simp]

theorem Complexity.MCSP.rethreshold_encode (threshold : ℕ → ℕ) (inst : Instance) : rethreshold threshold inst.encode = (inst.withThreshold (threshold inst.arity)).encode

Rethresholding a canonical code changes only its threshold field.

theorem Complexity.MCSP.rethreshold_comp (first second : ℕ → ℕ) (bits : List Bool) : rethreshold second (rethreshold first bits) = rethreshold second bits

Only the final requested threshold matters after repeated re-encoding.

theorem Complexity.MCSP.length_rethreshold_of_decode?_eq_some (threshold : ℕ → ℕ) {bits : List Bool} {inst : Instance} (hdecode : Instance.decode? bits = some inst) : (rethreshold threshold bits).length + 2 * inst.threshold.size = bits.length + 2 * (threshold inst.arity).size

Exact output-length accounting for rethresholding a decodable instance.

@[simp]

theorem Complexity.MCSP.mem_atThreshold_encode_iff (threshold : ℕ → ℕ) (inst : Instance) : inst.encode ∈ atThreshold threshold ↔ inst.threshold = threshold inst.arity ∧ inst.HasCircuitAtMost

Canonical membership in a threshold slice exposes both the forced threshold field and the ordinary MCSP predicate.

theorem Complexity.MCSP.rethreshold_encode_mem_atThreshold_iff (threshold : ℕ → ℕ) (inst : Instance) : rethreshold threshold inst.encode ∈ atThreshold threshold ↔ (inst.withThreshold (threshold inst.arity)).HasCircuitAtMost

Rethresholding always installs the requested threshold, leaving exactly the corresponding circuit-size question.