Strict-majority circuits -- proof internals

theorem Complexity.CircuitCode.strictMajorityThreshold_le_internal (inputCount : ℕ) [NeZero inputCount] : strictMajorityThreshold inputCount ≤ inputCount

theorem Complexity.CircuitCode.length_strictMajorityRawCircuit_internal (inputCount : ℕ) : List.length (strictMajorityRawCircuit inputCount) = 3 + 2 * inputCount * strictMajorityThreshold inputCount

theorem Complexity.CircuitCode.strictMajorityRawCircuit_wellFormed_internal (inputCount : ℕ) [NeZero inputCount] : RawCircuit.WellFormed inputCount (strictMajorityRawCircuit inputCount)

theorem Complexity.CircuitCode.eval?_strictMajorityRawCircuit_internal (inputCount : ℕ) [NeZero inputCount] (input : BitString inputCount) : (strictMajorityRawCircuit inputCount).eval? input.toList = some (decide (strictMajorityThreshold inputCount ≤ Fin.countP input))