RecogGeodesic3DeepCert
plain-language theorem explainer
A certificate packing three analytic facts used by recognition geodesics: diagonal domain cost vanishes off zero, domain cost is nonnegative for positive arguments, and the canonical threshold is positive. Gravity and geodesic constructions cite it as the structural bundle of J-cost properties. It is a plain structure type; inhabitants are assembled from sibling lemmas.
Claim. A recognition-geodesic deep certificate is a record of three statements: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats geodesics on the recognition manifold as curves that minimize $\int J(r(t)),dt$. Vanishing $J$ marks the recognition ground-state orbit; the first departure from a straight trajectory sits at $J=J(\varphi)$. Domain cost is the local cost functional on pairs of positive scale parameters that underlies that variational problem; the canonical threshold is the positive cutoff used to mark the first nontrivial departure.
Upstream, the foundation layer already knows that every recognition event has nonnegative cost, via $J$-cost nonnegativity on positive states. The present structure simply packages the concrete real-analytic consequences needed for the geodesic story: diagonal vanishing, nonnegativity on the positive quadrant, and positivity of the threshold.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields; this declaration only names the bundle.
proof idea
No proof body: this is a structure definition. The three fields are Prop-valued requirements. Downstream, cert fills them by assigning domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; cert_inhabited then wraps that inhabitant to show the type is nonempty.
why it matters
In the Recognition gravity stack, geodesics are defined by minimizing integrated $J$-cost. This certificate is the structural interface that freezes the three analytic facts those constructions need, without re-proving them at every use site. Downstream, cert and cert_inhabited produce a concrete, sorry-free inhabitant, matching the module claim of a structural theorem with zero sorry and zero axiom.
Framework-wise it sits under the $J$-uniqueness and $\varphi$ landmarks (T5–T6): diagonal vanishing is the ground-state orbit at $J=0$, and the positive canonical threshold is the scale at which trajectories first leave the straight-line regime near $J(\varphi)$. Parent consumers are the local certificate and nonempty proof in the same module; nothing beyond that bundle is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.