t5_holds
plain-language theorem explainer
The Recognition Composition Law plus reciprocity, normalization, calibration, and continuity force a unique cost on the positive reals: J(x) = (x + 1/x)/2 - 1. Anyone citing the T5 step of the unified forcing chain, or the complete-inevitability root theorems, needs this package. The proof fills the T5 structure from CostUniqueness facts for the canonical J-cost and routes uniqueness through the Aczél-packaged law-of-logic theorem, so callers never see ODE bootstrap hypotheses.
Claim. The T5 uniqueness package holds: the canonical cost $J(x)=\frac12(x+x^{-1})-1$ is reciprocal, normalized at $1$, satisfies the Recognition Composition Law, is log-calibrated, and is continuous on $(0,\infty)$; and any continuous $F:(0,\infty)\to\mathbb{R}$ obeying reciprocity $F(x)=F(1/x)$, normalization $F(1)=0$, the RCL $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$, and calibration, under Aczél smoothness of continuous d'Alembert solutions, equals $J$ identically.
background
The Unified Forcing Chain module proves that T0–T8 are forced from the cost foundation (Recognition Composition Law), not merely compatible with it. T5 is the uniqueness rung: RCL together with reciprocity, normalization, and calibration pin the cost functional on the positive reals.
The RCL is $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Reciprocity is the double-entry identity $J(x)=J(1/x)$. Normalization is $J(1)=0$; calibration fixes the log-coordinate second derivative at the identity so the curvature scale is one. The Aczél smoothness package states that every continuous solution of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^\infty$ (Aczél 1966), closing regularity without exposing ODE bootstrap to callers.
Upstream, the law-of-logic cost theorem is the authoritative uniqueness result: any reciprocal, normalized, composition-law, calibrated, continuous $F$ equals the canonical J-cost once that Aczél package is in scope.
proof idea
Term-mode inhabitant of the T5 structure. The five property fields are filled directly by the CostUniqueness lemmas for the canonical J-cost: reciprocal symmetry, normalization at 1, satisfaction of the composition law, log-coordinate calibration, and continuity on the positive reals.
The uniqueness field is a lambda over an arbitrary $F$ carrying an Aczél-smoothness hypothesis plus the five analytic hypotheses. The proof promotes the Aczél hypothesis to a typeclass instance, then applies the law-of-logic forces J-cost theorem, which returns pointwise equality with the canonical cost. No fresh analysis is performed here; this is a packaging bridge onto the explicit RCL theorem surface.
why it matters
T5 is the J-uniqueness landmark in the forcing chain (primer T5: $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$). It is required by the complete-inevitability root theorems (ultimate inevitability and its canonical and extended surfaces), by constants-from-phi (via the spine-to-extras bridge with T0 and T6), by the classical-negation-plus-unique-minimizer bridge, and by the gravity master theorem's T0–T8 package.
Without unique $J$, the self-similar fixed point $\varphi$ (T6) and the derived constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ have no forced cost substrate. The producer-bridge doc records that the RCL surface is now available, so the complete chain no longer populates T5 as a free sibling of the T4-to-T5 realization bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.