T5_J_Unique
plain-language theorem explainer
T5 packages the claim that recognition cost is unique: reciprocity, normalization, the Recognition Composition Law, calibration, and continuity force J(x)=(x+1/x)/2-1 on (0,∞). Anyone citing the forcing chain's unique-J step uses this Prop bundle. It is a claim interface (structure), not a proved inhabitant; uniqueness is stated via the Aczél-packaged RCL surface so callers avoid ODE bootstrap hypotheses.
Claim. The recognition cost $J(x)=\frac12(x+x^{-1})-1$ is reciprocal, normalized, satisfies the Recognition Composition Law, is canonically calibrated, and is continuous on $(0,\infty)$. Moreover, for every $F:\mathbb{R}\to\mathbb{R}$, if the Aczél smoothness package holds and $F$ is reciprocal, normalized, composition-law compliant, calibrated, and continuous on $(0,\infty)$, then $F(x)=J(x)$ for all $x>0$.
background
In the Unified Forcing Chain, every step from the absolute floor through T8 is meant to be forced from the cost foundation. T5 is the unique-J rung: after ledger and recognition (T3–T4), the cost functional itself is pinned.
The native cost is $J(x)=\frac12(x+x^{-1})-1$ on positive reals (equivalently $\cosh(\log x)-1$). Reciprocal symmetry $J(x)=J(x^{-1})$ is the algebraic double-entry law. Normalization and calibration fix the scale at the identity (classically $J(1)=0$ and a second-derivative/log-coordinate normalization). The Recognition Composition Law is the functional equation $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
Upstream algebra records reciprocity for this $J$ and packages Aczél-style regularity so uniqueness can be stated without exposing ODE bootstrap data to chain callers. The module's key insight is that RCL plus normalization plus calibration force the rest of the chain once the claim surfaces are assembled.
proof idea
No proof body: this declaration is a Prop structure, the T5 claim interface. Fields assert that the concrete cost satisfies reciprocity, normalization, composition, calibration, and continuity on $(0,\infty)$, plus a quantified uniqueness clause.
The uniqueness field is the explicit RCL theorem surface: any competitor $F$ meeting the same algebraic hypotheses, the Aczél smoothness package, and continuity equals $J$ pointwise for $x>0$. The adjacent module note records that inhabitants are meant to come from the Aczél-packaged law_of_logic_forces_jcost surface rather than raw ODE hypotheses. Downstream bridges simply project .uniqueness and the property fields.
why it matters
T5 is the primer landmark "J-uniqueness": $J(x)=\frac12(x+x^{-1})-1$. It is the hinge between cost algebra and self-similarity. Downstream, t5_to_t6_bridge_holds and T5_To_T6_Forced_Bridge consume a T5_J_Unique hypothesis to force $\varphi$ (T6); CompleteForcingChain / CompleteForcingChainT8 re-export it in the full T−1..T8 record.
The bridge audit note is sharp: the T5 record is proved from cost-uniqueness lemmas about this $J$ and the Aczél-packaged law-of-logic surface; it does not consume the T−1..T4 floor beyond re-exporting an RCL surface field. Deleting the floor would not break a T5 proof. The open structural point is therefore not uniqueness of $J$, but whether the floor's own cost can satisfy the same hypotheses that force this $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.