naturalPhaseFailureCost
plain-language theorem explainer
The natural phase failure cost for gate size c is defined as the J-cost of the positive ratio 1 + 1/(c+1). Researchers examining honest obstructions in residual gap calculations cite this to quantify the finite-phase mismatch that decreases with larger gates. The definition is a direct one-line application of the Jcost function chosen to remain defined at c=0.
Claim. For each natural number gate size $c$, the natural phase failure cost is $J(1 + 1/(c+1))$, where $J$ denotes the J-cost function.
background
This definition sits in the Honest Residual Gap module, whose module documentation states that the natural finite-phase mismatch cost decreases with gate size and therefore cannot justify a uniform KTheta floor. The module imports the Cost module (supplying Jcost) and BoundedPhaseVisibility. Jcost measures phase mismatch via the Recognition Composition Law and is applied here to the ratio 1 + 1/(c+1) to keep the argument positive and defined at zero.
proof idea
One-line definition that applies Jcost directly to the expression 1 + 1/(c + 1).
why it matters
The definition supplies the concrete mismatch model used by the downstream theorems naturalPhaseFailureCost_pos (which proves strict positivity) and naturalPhaseFailureCost_two_below_one (which shows the value at c=2 is already less than 1). The latter rules out deriving an arbitrary fixed floor from mere positivity, forcing the search for a prime/divisor distribution theorem instead. It records the honest obstruction step in the residual gap analysis within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.