IndisputableMonolith.Verification.CoshStrictConvexCert
Verification certificate that the log-domain cost J_log(t)=cosh(t)-1 is strictly convex on the reals. Analysts and anyone citing the T5 J-uniqueness step use it as a machine-checked convexity witness. The module imports the Cost.Convexity development and packages its strict-convexity theorems for the verification layer.
claimThe module certifies that $J_{\log}(t)=\cosh t-1$ is strictly convex on $\mathbb{R}$, and thereby that $J(x)=\frac12(x+x^{-1})-1$ is strictly convex on $\mathbb{R}_{>0}$.
background
Recognition Science forces the cost functional through the Recognition Composition Law and uniqueness (forcing step T5). The unique solution is $J(x)=(x+x^{-1})/2-1$, equivalently $J_{\log}(t)=\cosh t-1$ after $t=\log x$.
Strict convexity of this $J$ is the analytic engine behind uniqueness: a strictly convex functional cannot admit two distinct minimizers with the same boundary data. The upstream module Cost.Convexity states exactly that: "$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 marks both results as foundational for T5.
This verification module sits one layer above that development. It does not re-prove convexity from scratch; it exposes a certificate object consumable by the broader Verification hierarchy.
proof idea
The module is a thin verification wrapper. It imports Mathlib and IndisputableMonolith.Cost.Convexity, then packages the already-proved strict-convexity theorems for $J_{\log}$ (second derivative $\cosh t>0$, or equivalent first-derivative monotonicity) into a named certificate CoshStrictConvexCert. No independent analytic argument lives here; the substance is upstream.
why it matters in Recognition Science
T5 (J-uniqueness) in the forcing chain requires a strictly convex cost so that the functional equation plus normalization pins $J(x)=\cosh(\log x)-1$ uniquely. Without a checked convexity witness, the uniqueness step is only a paper claim.
This module supplies that witness to the Verification domain. Downstream consumers that assemble end-to-end certificates for the forcing chain (T0–T8) can point at a single certificate rather than reaching into the Cost library. It does not itself prove T5; it freezes the convexity lemma that T5 depends on.
scope and limits
- Does not prove T5 J-uniqueness; only certifies the convexity input to that step.
- Does not re-derive strict convexity; relies entirely on Cost.Convexity.
- Does not address discrete or lattice convexity, only the real/positive-real continuum statements.
- Does not certify the Recognition Composition Law or any other forcing step.