Conditional anti-checker counter circuits -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterOutputWidth_pos_internal (beta : PositiveRationalScale) (arity : ℕ) : 0 < counterOutputWidth beta arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterSizeBound_pos_internal (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) : 0 < counterSizeBound overhead beta arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterCircuit.estimate_lt_two_pow_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (input : BitString ((prefixLength + 1) * (arity + 1))) : counter.estimate input < 2 ^ counterOutputWidth beta arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterCircuit.outputWidth_le_sizeBound_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : counterOutputWidth beta arity ≤ counterSizeBound overhead beta arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterCircuit.approximates_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} {counter : ApproximateCounterCircuit overhead beta arity prefixLength} (hcorrect : counter.IsCorrect) (input : BitString ((prefixLength + 1) * (arity + 1))) : AntiChecker.IsRelativeApproximation (roundPrecision arity) (candidateLabeledSurvivorCount arity (smallThreshold beta arity) (unpackLabeledSamples input)) (counter.estimate input)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterFamily.counter_isCorrect_internal {overhead arity : ℕ} {beta : PositiveRationalScale} {family : ApproximateCounterFamily overhead beta arity} (hcorrect : family.IsCorrect) (prefixLength : Fin (requiredRoundCount beta arity)) : (family.counter prefixLength).IsCorrect