Threshold slices of MCSP -- proof internals

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

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

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

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

theorem Complexity.MCSP.length_rethreshold_of_decode?_eq_some_internal (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

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

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