T5_J_Unique
plain-language theorem explainer
T5 packages uniqueness of the recognition cost J(x)=(x+x^{-1})/2-1 among continuous reciprocal normalized calibrated solutions of the composition law. Anyone citing the forcing spine into T6 (φ) or the full T-1..T8 chain needs this record. As a Prop structure it is a definitional interface; its fields are discharged by CostUniqueness and functional-equation lemmas, not by a local proof body.
Claim. The T5 package asserts that $J(x)=(x+x^{-1})/2-1$ is reciprocal ($J(x)=J(x^{-1})$), normalized, satisfies the recognition composition law, is calibrated ($G''(0)=1$ for $G(t)=J(e^t)$), and continuous on $(0,\infty)$; and that any $F:\mathbb{R}\to\mathbb{R}$ meeting the same conditions under the Aczél smoothness package equals $J$ at every $x>0$.
background
The module exposes the public T-1 through T8 forcing spine. T5 is the step that pins the canonical reciprocal cost: once a cost functional is forced to be reciprocal, normalized, continuous, calibrated, and to obey the composition law, it must be $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$).
Upstream, $J$ is defined as that closed form. Reciprocity is the algebraic double-entry identity $J(x)=J(x^{-1})$. Normalization and calibration fix the zero and the quadratic scale near the identity (calibration is $G''(0)=1$ for $G(t)=F(e^t)$). The composition law is the Recognition Composition Law on positive ratios. Aczél smoothness packages the classical fact that continuous d'Alembert solutions are $C^\infty$, so uniqueness arguments may differentiate freely.
Locally this structure only records those properties for $J$ plus the universal uniqueness quantifier; it does not itself derive them from the T-1..T4 floor.
proof idea
No proof body: this is a Prop structure (definitional interface). Its six fields name the properties that constitute T5 uniqueness. Reciprocity, normalization, composition, calibration, and continuity of $J$ are expected to be filled by existing Cost / FunctionalEquation / CostUniqueness lemmas (and related reciprocity theorems for $J$). The uniqueness field is the standard Aczél-class uniqueness statement: any $F$ that is reciprocal, normalized, composition-law, calibrated, continuous on $(0,\infty)$, and lives under the Aczél smoothness package, agrees with $J$ on positives. Downstream bridges treat an inhabitant of this structure as a hypothesis bundle rather than re-proving uniqueness in place.
why it matters
T5 is the J-uniqueness landmark in the forcing chain (primer T5). It is the hinge from cost form to self-similar hierarchy: downstream T5_To_T6_SelfSimilarity_Bridge, T5_To_T6_Forced_Bridge, and t5_to_t6_bridge_holds / t5_to_t6_forced_bridge_holds consume the uniqueness field to force φ as the self-similar fixed point (T6). CompleteForcingChainT8 and UnifiedForcingChain.CompleteForcingChain include this record on the public spine.
The module honesty note is important: the T5 content is proved from CostUniqueness lemmas about Jcost and from law_of_logic_forces_jcost; it does not consume the T-1..T4 floor beyond re-exporting an RCL surface. Deleting T-1..T4 would not break T5 proofs. The open structural gap is that the floor's own cost cannot yet be shown to satisfy the full T5 package, so the arrow T4→T5 remains a bridge interface rather than a derivation from distinguishability alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.