continuum_gauge_exceeds_native_gauge
plain-language theorem explainer
On the continuum every positive real scale yields a reciprocal, normalized, RCL-satisfying continuous cost via the cosh-log family; on the discrete carrier every even-power native cost fails the structural ledger without anchor. Anyone comparing continuum gauge freedom to native PRC uniqueness cites this. The proof is a pair of existing lemmas, one for each conjunct.
Claim. For every $l > 0$, the continuum cost $F_l(x) = \tfrac12(x^l + x^{-l}) - 1$ is reciprocal, normalized ($F_l(1)=0$), satisfies the Recognition Composition Law, and is continuous on $(0,\infty)$. Simultaneously, for every natural $k$, the even-power native cost generated by $k$ fails the structural native-cost hypotheses with the anchor removed (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace).
background
Recognition Composition Law (RCL) is the functional equation $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ on positives. A reciprocal cost obeys $F(x)=F(1/x)$; normalized means $F(1)=0$. The continuum gauge family is $\mathrm{costLambda},c,x = \tfrac12(x^c+x^{-c})-1$, equivalently $\cosh(c\log x)-1$; the $c=1$ member is the unique $J$ of the forcing chain (T5).
The native side works on ratio orbits rather than $\mathbb{R}_{>0}$. The structural ledger without anchor packages four discrete constraints: base hypotheses minus two-calibration, sign-reversal, monotonicity, and zero-calibration of the doubled trace. Even-power generated native costs are the discrete analogues of even continuum exponents.
This module records how continuum gauge freedom fails to transport onto the carrier: the continuum admits a full positive scale family under RCL, while even powers are refuted on the structural ledger.
proof idea
Term-mode pair. The first conjunct is the lambda fun l hl => composition_law_admits_full_scale_family l hl, which already proves that every positive scale of costLambda is reciprocal, normalized, RCL-compliant, and continuous on $(0,\infty)$. The second conjunct is the existing lemma evenPowerGeneratedNativeCost_not_sansAnchor, which shows no even-power native cost satisfies the structural hypotheses with the anchor removed. No further rewriting.
why it matters
Feeds structuralStratificationCertificate_holds, which assembles uniqueness, slim contraction, positivity, and the refutation that the sans-anchor uniqueness target is inhabited. The doc-comment frames the claim as: the continuum scale family does not transport; part of what calibration collapses is freedom that exists only after completion to the line.
In the RS forcing picture this separates T5 $J$-uniqueness and RCL on $\mathbb{R}_{>0}$ from the discrete carrier orbit. Odd powers remain present (gauge_orbit_contains_every_odd_power); whether anything beyond that orbit exists is the named transcendence wall. The result is a stratification certificate ingredient, not a cardinality comparison of orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.