cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single certificate for the deep recognition-curvature bundle: the cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Gravity and curvature modules cite this as the inhabited witness that the cost geometry is well-posed. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There exists a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
The module develops the deep (v3) recognition-bundle curvature story: Chern numbers $c_1=1/45$, $c_2=1/2025$ from a $U(1)\sigma\times U(1)\Theta$ structure, with curvature form $F=dA+A\wedge A$ identified in RS units as $F=J(\phi),\omega_{\mathrm{recognition}}$ on the recognition manifold.
The certificate structure packages three cost-geometry axioms used by that story. Domain cost is the local cost functional on pairs of positive reals (mass/energy-like arguments); it is required to vanish when the two arguments coincide and to stay nonnegative when both are positive. The canonical threshold is a fixed positive scale against which curvature or recognition events are compared.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: the cost of any recognition event is non-negative, via $J$-cost nonnegativity). The three field proofs are sibling lemmas in this same module.
proof idea
One-line structure inhabitant. Each field of RecogCurvature3DeepCert is filled by the corresponding already-proved sibling: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No extra tactics or algebraic work.
why it matters
Gives a single named witness that the cost side of the deep recognition-curvature package is inhabited and consistent. The module presents this layer as a structural theorem (zero sorry, zero axiom) supporting the identification $F=J(\phi),\omega_{\mathrm{recognition}}$ and the reported Chern numbers. In the broader RS chain this sits on the gravity side of the $J$-cost geometry forced at T5, with $\phi$ the self-similar scale from T6. No downstream consumers are recorded yet; the immediate sibling cert_inhabited simply records that the type is nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.