Pith. sign in
module module moderate

IndisputableMonolith.Verification.JcostCoshIdentityCert

show as:
view Lean formalization →

Verification certificate that the Recognition cost equals its hyperbolic form: J(x) = cosh(log x) - 1. Cited by anyone auditing T5 J-uniqueness or the closed-form cost used on the phi-ladder. The module packages that elementary identity against the FunctionalEquation helpers rather than re-proving uniqueness.

claimCertificate that the Recognition cost satisfies $J(x)=\cosh(\log x)-1$ for $x>0$, equivalently $J(x)=\frac{x+x^{-1}}{2}-1$.

background

Recognition Science forces a unique nonnegative cost $J$ on ratios via the Recognition Composition Law and the T5 uniqueness step. The closed form is $J(x)=(x+x^{-1})/2-1$, which is identical to $\cosh(\log x)-1$ once one works in logarithmic coordinates.

The imported Cost.FunctionalEquation module supplies the lemmas used in the T5 cost-uniqueness argument. This verification module sits one layer above that: it does not re-derive uniqueness, but records the cosh identity as a named, checkable certificate in the Verification domain.

proof idea

Certificate/verification module, not a standalone uniqueness proof. It wires the elementary identity $$(x+x^{-1})/2-1=\cosh(\log x)-1$$ to the cost API exposed by FunctionalEquation, so audits can point at one object rather than unfold hyperbolic trig by hand.

why it matters in Recognition Science

Pins the T5 landmark form of $J$ used throughout the forcing chain and mass ladder. Downstream verification surfaces that need a machine-checkable witness that the cost in RS-native units is the same $J$ as $\cosh(\log x)-1$ cite this certificate. No parent used_by edges are recorded; the module is an audit artifact in Verification, not a step inside UnifiedForcingChain itself.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)