JcostCoshFormCert
plain-language theorem explainer
Certificate packaging that the recognition cost J, in log-coordinates, equals cosh(t)−1 and obeys the cosh-add identity. Verification auditors and anyone citing T5 J-uniqueness use it as a single Prop bundle. Discharge is a two-line constructor applying the pointwise cosh identity and the functional identity lemmas.
Claim. A unit certificate whose verification predicate asserts two facts about the recognition cost $J(x)=(x+x^{-1})/2-1$: (i) $G_J(t):=J(e^t)=\cosh t-1$ for every real $t$; (ii) $G_J$ satisfies the cosh-add identity $G(t+u)+G(t-u)=2G(t)G(u)+2(G(t)+G(u))$. The top-level theorem states that every such certificate verifies.
background
The module packages the log-coordinate form of the Recognition Science cost. The cost is $J(x)=(x+x^{-1})/2-1$ for $x>0$ (the unique nonnegative cost vanishing only at ratio one). Passing to log-coordinates via $G(t)=J(e^t)$ converts the algebraic expression into hyperbolic form: $G_J(t)=(\mathrm{e}^t+\mathrm{e}^{-t})/2-1=\cosh t-1$.
The second conjunct is the cosh-type functional identity CoshAddIdentity: $G(t+u)+G(t-u)=2G(t)G(u)+2(G(t)+G(u))$. It is the d'Alembert equation shifted by the constant $-1$; the extra linear terms come from that shift. Module docs stress that these two facts feed T5 cost uniqueness: cosh representation plus ODE uniqueness $H''=H\Rightarrow H=\cosh$, together with d'Alembert symmetry, pin $J$ as the unique admissible cost.
Upstream, Cost.Jcost and the cosmology aliases supply the same algebraic definition; CoshAddIdentity is the named functional-equation interface imported from Cost.FunctionalEquation.
proof idea
The structure itself is an empty marker (deriving Repr only). The content lives in the simp predicate verified, which is the conjunction of the pointwise identity and CoshAddIdentity Cost.Jcost.
The discharge theorem verified_any is a one-step constructor: the left conjunct is closed by Jcost_G_eq_cosh_sub_one (the explicit $G_J=\cosh-1$ lemma), and the right conjunct by Jcost_cosh_add_identity. No further rewriting or case analysis is required.
why it matters
This certificate is a verification-layer packaging of the T5 landmark: J-uniqueness with $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. The module doc states the identities are foundational for T5: the cosh representation ties $J$ to hyperbolic geometry, and the functional identity shows the cost structure is fixed by algebraic constraints rather than free choice.
In the forcing chain, T5 sits between the Recognition Composition Law (RCL) and the later forcing of $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). Having a single verified Prop lets downstream certificate aggregators assert the cosh form without reopening the functional-equation development. No used_by edges are recorded yet; the natural consumers are higher verification bundles that assemble the full T5 uniqueness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.