naturalPhaseFailureCost_two_below_one
plain-language theorem explainer
The result shows that the natural phase failure cost evaluates to a value strictly below one when the gate size is two. Researchers studying residual gaps in mismatch models would cite it to demonstrate that positivity of the cost function alone cannot enforce a uniform unit floor. The proof reduces the claim by unfolding the cost definition and normalizing the resulting numerical expression using the J-cost relation.
Claim. Let $C(n)$ denote the natural phase failure cost for gate size $n$. Then $C(2) < 1$.
background
The Honest Residual Gap module records the honest obstruction that natural finite-phase mismatch costs decrease with gate size and therefore cannot justify a uniform KTheta floor from the mismatch model. The J-cost function supplies the recognition cost $J(x) = (x + x^{-1})/2 - 1$ that appears in the normalization step. Upstream results include the eight-tick phase definition giving periodic values $k pi / 4$ for $k = 0$ to $7$ and the magnitude-of-mismatch structure that forces symmetry on any carrier and cost type.
proof idea
The proof is a term-mode reduction that unfolds the natural phase failure cost definition and applies norm_num with the Jcost lemma to evaluate the concrete numerical inequality.
why it matters
The declaration supplies a concrete cost value below the unit floor, reinforcing the module's statement that the natural mismatch model cannot itself produce a uniform floor. It highlights the need for a prime or divisor distribution theorem capable of producing actual phase hits rather than relying on cost positivity. This sits inside the eight-tick octave of the forcing chain where phase periodicity governs the residual gap analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.