Pith. sign in
module module moderate

IndisputableMonolith.Verification.CalibrationCert

show as:
view Lean formalization →

Verification certificate packaging the unit-normalization of the Recognition cost: the second derivative of J_log at the origin equals 1 (axiom A4). Audit and forcing-chain consumers cite it to discharge scale-fixing without opening the Cost.Calibration development. The module re-exports the calibrated identity proved upstream.

claimCertificate that $J_{\log}''(0)=1$, i.e. the unit-normalization axiom (A4) for the Recognition cost $J$, fixing its overall scale at the identity.

background

Recognition Science characterizes the cost $J$ by a short axiom list. Axiom A4 requires that the logarithmic form $J_{\log}$ satisfy $J_{\log}''(0)=1$. That single normalization pins the scale of $J$ and, together with the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, forces the unique closed form $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$).

The upstream module Cost.Calibration carries the analytic proof that the second derivative at zero equals 1, "establishing the unit normalization axiom (A4)" and thereby "fix[ing] the scale uniquely and complet[ing] the characterization of $J$." Verification.CalibrationCert lives in the verification layer: it imports that development and exposes the calibrated identity as a stable certificate for audit consumers.

proof idea

Thin verification certificate module, not an independent analytic development. It imports Cost.Calibration and packages the already-proved identity $J_{\log}''(0)=1$ under a certificate name. No new second-derivative computation occurs here; the argument is the upstream calibration proof.

why it matters in Recognition Science

Unit normalization (A4) is required to finish T5 J-uniqueness in the forcing chain: without a fixed second derivative at the identity, the scale of $J$ remains free and RS-native constants (including $\hbar=\varphi^{-5}$) cannot lock. This module supplies the verification-facing certificate so audit surfaces need not depend directly on Cost.Calibration. Supplied used_by edges are empty, so it functions as a leaf certificate in the verification domain rather than an intermediate lemma in a longer proof chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)