IndisputableMonolith.Verification.JcostConvexityCert
Verification certificate module for strict convexity of the Recognition cost J. Anyone auditing T5 (J-uniqueness) or needing a machine-checked convexity fact in the verification graph lands here. It imports Cost.Convexity and surfaces those results under a Verification name. Packaging is thin re-export style, not a fresh analytic proof.
claimCertificate that $J_{\log}(t)=\cosh t-1$ is strictly convex on $\mathbb{R}$ and that $J(x)=\frac12(x+x^{-1})-1$ is strictly convex on $\mathbb{R}_{>0}$.
background
Recognition Science forces a unique cost via the Recognition Composition Law and the forcing chain. Landmark T5 identifies that cost as $J(x)=\frac12(x+x^{-1})-1$ on $\mathbb{R}{>0}$, equivalently $J{\log}(t)=\cosh t-1$ after $t=\log x$.
Upstream Cost.Convexity proves both presentations are strictly convex: "$J_{\log}(t)=\cosh t-1$ is strictly convex on $\mathbb{R}$" and "$J_{\mathrm{cost}}(x)=\frac12(x+x^{-1})-1$ is strictly convex on $\mathbb{R}_{+}$", and states these facts are foundational for T5.
This module lives in the Verification domain. It does not redefine J; it packages the convexity theorems so verification consumers can depend on a single certificate node rather than the full Cost development.
proof idea
Import-and-certify structure, not a new analytic argument. The second-derivative (or equivalent) work establishing strict convexity of $\cosh t-1$ and the change-of-variables transfer to $J$ on $\mathbb{R}_{>0}$ lives in IndisputableMonolith.Cost.Convexity. This module re-exports or wraps that content under Verification.JcostConvexityCert so the verification dependency graph has a stable named certificate.
why it matters in Recognition Science
Strict convexity is the analytic lever behind T5 J-uniqueness in the forcing chain (J forced to $(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$). Downstream verification audits of cost minimality, RCL consequences, or uniqueness arguments can point at this certificate without opening Cost.Convexity directly. The current graph records no used_by edges, so the module is a leaf packaging node ready for verification consumers rather than an interior proof step.
scope and limits
- Does not reprove convexity; defers entirely to Cost.Convexity.
- Does not prove J-uniqueness (T5) or the Recognition Composition Law.
- Does not treat discrete phi-ladder convexity or mass-formula bounds.
- Does not address behavior at the boundary x=0 or non-strict convexity claims.