naturalPhaseFailureCost_pos
plain-language theorem explainer
Natural phase failure cost is strictly positive for every natural number c. Researchers on residual gap bounds in Recognition Science cite this to show that finite-phase mismatch costs decrease with gate size and cannot enforce a uniform floor. The proof unfolds the definition, applies the positivity tactic to confirm the argument exceeds 1, then invokes the J-cost positivity lemma.
Claim. For every natural number $c$, the natural phase failure cost satisfies $0 < J(1 + 1/(c+1))$, where $J$ denotes the J-cost function.
background
The module records the honest obstruction in phase matching: natural finite-phase mismatch cost decreases with gate size and cannot justify a uniform KTheta floor. J-cost is the function satisfying J(x) > 0 whenever x > 0 and x ≠ 1, as stated in the upstream lemma Jcost_pos_of_ne_one. The eight-tick phase structure supplies the periodic phases kπ/4 for k = 0 to 7 that underlie the mismatch model.
proof idea
The tactic proof unfolds naturalPhaseFailureCost to expose the argument 1 + 1/(c+1). Positivity tactic yields 0 < 1 + 1/(c+1) and the strict inequality to 1. The lemma Jcost_pos_of_ne_one is then applied directly to the unfolded expression.
why it matters
The result sharpens the module's obstruction statement that natural mismatch costs alone cannot produce a fixed floor, directing attention to the required prime/divisor distribution theorem for actual phase hits. It rests on J-cost positivity and the eight-tick phase definition, closing one algebraic path while leaving the divisor-theoretic gap open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.