curvature_cancels_in_dimensionless
plain-language theorem explainer
Dimensionless outputs are independent of the curvature-normalization gauge: if two real values agree for every positive scale factor, they agree outright. Cited when arguing that F''(0)=1 is a unit choice, not a physical constraint in the T5 uniqueness story. Proof is a one-line instantiation of the hypothesis at scale 1.
Claim. Let $\alpha_1,\alpha_2\in\mathbb{R}$. If $\alpha_1=\alpha_2$ holds for every curvature scale $c>0$, then $\alpha_1=\alpha_2$.
background
This module closes Gap 4 in the T5 cost-uniqueness critique: the symmetry and normalization constraints on the cost $F$ are not free assumptions. Reciprocal symmetry $F(x)=F(1/x)$ and unit normalization $F(1)=0$ are forced from the double-entry ledger (T3). The third classical constraint, curvature normalization $F''(0)=1$, is treated differently.
Per the module resolution, curvature normalization is a gauge choice (a unit definition). Any rescaling $F\mapsto cF$ with $c>0$ leaves the physics unchanged because observables enter as ratios. The sibling claim that curvature is gauge normalization records that status; the present theorem records the consequence for dimensionless outputs: they cannot depend on the chosen scale $c$.
No external lemmas are required. The argument lives entirely inside the T5 constraint-forcing layer that feeds J-uniqueness (forcing-chain step T5).
proof idea
Term-mode one-liner. The hypothesis already asserts $\alpha_1=\alpha_2$ for every positive real $c$. Instantiate at $c=1$, using the Mathlib fact that $1>0$. The goal $\alpha_1=\alpha_2$ is immediate. No algebraic rewriting and no appeal to the cost functional itself.
why it matters
In the Recognition forcing chain, T5 asserts uniqueness of the cost $J(x)=(x+x^{-1})/2-1$ once symmetry and normalization are fixed. Critics object that those constraints look chosen. This theorem is the thin formal witness that the curvature piece is pure gauge: dimensionless quantities (the only physical outputs) cancel any rescaling of $F$.
Together with the ledger-forced reciprocal and unit constraints, it completes the answer to "who chose the T5 hypotheses": two are forced by double-entry structure; one is a harmless unit convention. Downstream uniqueness of $J$, and later landmarks that rest on it (self-similar $\phi$, eight-tick period, $D=3$), inherit a cleaner justification. No used_by edges are recorded yet; the declaration is local scaffolding for the gauge half of the Gap-4 resolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.