t5_delta_forced
plain-language theorem explainer
On the φ-ladder the doubled cost J_n = φⁿ + φ⁻ⁿ − 2 is normalized, calibrated by J_1 = √5 − 2, reciprocal-symmetric, and obeys the discrete Recognition Composition Law; it is the unique such sequence. Cite this for the choice-free (sigma0) T5 cost-uniqueness node restricted to the ledger's discrete carrier. The proof is a single pair constructor packaging four elementary properties with the discrete uniqueness theorem.
Claim. Let $J_n = \varphi^n + \varphi^{-n} - 2$ on $\mathbb{Z}$ (values in $\mathbb{Z}[\varphi]$). Then $J_0 = 0$, $J_1 = \sqrt{5}-2$, $J_{-n} = J_n$ for all $n$, and $J$ satisfies the discrete RCL $J_{m+n} + J_{m-n} = J_m J_n + 2 J_m + 2 J_n$. Moreover any $G:\mathbb{Z}\to\mathbb{Z}[\varphi]$ with $G(0)=0$, $G(1)=\sqrt{5}-2$, and the same discrete RCL equals $J$ at every integer.
background
Recognition Science forces the cost functional by the Recognition Composition Law (RCL). The continuum T5 node proves that any reciprocal-symmetric, normalized, calibrated continuous $F$ obeying RCL equals $J(x)=(x+x^{-1})/2-1$, but that argument uses Classical.choice (sigma1) to exclude pathological real interpolants.
This module re-derives T5 on the domain the ledger actually inhabits: the φ-ladder ${\varphi^n:n\in\mathbb{Z}}$ forced by T6 self-similarity, carried in the ring GoldenInt = $\mathbb{Z}[\varphi]$. Negative powers are exact ring elements via $\varphi^{-1}=\varphi-1$; no division or field is required. The doubled cost is $J_n=\mathrm{trace}_n-2$ where $\mathrm{trace}_n=\varphi^n+\varphi^{-n}$ is the exact algebraic stand-in for $2\cosh(n\log\varphi)$.
The discrete RCL is the exact specialization of the continuum composition law at $x=\varphi^m$, $y=\varphi^n$, written in the doubled normalization $G=2F$ so all values stay inside the ring: $G(m+n)+G(m-n)=G(m)G(n)+2G(m)+2G(n)$. Upstream, d'Alembert uniqueness for the shifted sequence pins every integer value from two initial data by two-step induction; symmetry is derived, not assumed.
proof idea
Term-mode pair constructor. The left conjunct assembles four already-proved facts about the doubled cost: normalization at 0, calibration at 1 (equals $\sqrt{5}-2$), reciprocal symmetry, and satisfaction of the discrete RCL. The right conjunct is the uniqueness theorem: any integer sequence into GoldenInt that is normalized, calibrated the same way, and obeys discrete RCL equals the doubled cost pointwise. That uniqueness shifts by 2 into the d'Alembert frame and invokes trace uniqueness by strong induction. No further tactics; the declaration is pure packaging of those five lemmas.
why it matters
This is the T5 node of the forcing chain (T0–T8), restated as a delta-forced sigma0 fact on the φ-ladder. The continuum law_of_logic_forces_jcost remains the sigma1 residue quarantined in Cost.FunctionalEquation; here continuity, reciprocity-as-hypothesis, and Classical.choice are all eliminated. Reciprocal symmetry becomes a theorem of the discrete law, and the two-step recurrence plus two initial values replace the cosh ODE argument.
Framework landmarks: T5 J-uniqueness with $J(x)=\cosh(\log x)-1$, T6 φ as self-similar fixed point supplying the ladder carrier, and the RCL itself in doubled discrete form. The result closes the choice-free re-derivation promised by the module: the algebraic skeleton of T5 lives entirely inside $\mathbb{Z}[\varphi]$ with axiom footprint ${propext, Quot.sound}$. Downstream use sites are not yet wired in this graph snapshot, but the declaration is the citation target for any later spine step that needs discrete cost uniqueness without continuum hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.