IndisputableMonolith.Verification.CoshPropertiesCert
Verification module packaging certified algebraic identities for hyperbolic cosine that underwrite the T5 uniqueness of the recognition cost J. Anyone citing the closed form J(x)=cosh(log x)-1, or the Recognition Composition Law reductions that use it, lands here. The module is a thin certificate layer over Mathlib and the FunctionalEquation helpers; it does not reprove T5 itself.
claimCertificate bundle for the identities linking $J(x)=\frac{x+x^{-1}}{2}-1$ to $\cosh(\log x)-1$, including evenness, positivity for $x>0$, $x\neq 1$, the fixed-point relation at the golden ratio scale, and the composition identities needed by the T5 cost-uniqueness argument.
background
Recognition Science forces a unique nonnegative cost $J$ on ratios via the Recognition Composition Law and normalization. Landmark T5 identifies that cost as $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$ for $x>0$. The upstream module Cost.FunctionalEquation supplies the functional-equation lemmas used in that uniqueness proof.
This verification module sits one layer above those helpers. It collects the concrete cosh (and log-cosh) facts that must hold for the closed form to be admissible: evenness in the multiplicative variable, strict positivity off the identity, and the algebraic reductions that turn RCL instances into hyperbolic identities. Notation and units follow the RS-native convention $c=1$ with the $\varphi$-ladder elsewhere; nothing here depends on dimension or the eight-tick clock.
proof idea
Definition and certificate module, not a single theorem proof. It imports Mathlib analysis facts on $\cosh$ and the FunctionalEquation helper lemmas for T5, then packages the needed identities (rewrites of $J$ into cosh form, basic inequalities, and composition corollaries) as named certificate objects. No independent forcing argument is run here; discharge is by direct appeal to Mathlib plus the upstream functional-equation API.
why it matters in Recognition Science
T5 J-uniqueness is the hinge that turns the abstract cost functional equation into the concrete generator used by the rest of the forcing chain (T6 $\varphi$ fixed point, mass ladder, coupling constants). Without a clean cosh certificate, every downstream citation of $J(x)=\cosh(\log x)-1$ would re-open elementary hyperbolic algebra. This module isolates that bookkeeping so the FunctionalEquation lemmas and any later verification reports can treat the cosh form as a black-box fact. No direct used-by edges are recorded; the consumer is the T5 uniqueness development and any audit that checks the closed form against RCL.
scope and limits
- Does not prove T5 uniqueness; only certifies cosh identities used by it.
- Does not derive the Recognition Composition Law or force $\varphi$.
- Does not address spatial dimension, eight-tick period, or mass-ladder rungs.
- Does not supply numerical bounds on $\alpha$ or other RS constants.
- Does not replace Mathlib analysis; assumes standard real $\cosh$ facts.