cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single gravitational-lensing certificate. Anyone citing the structural Einstein-ring claim in this module will pull this bundle rather than the three lemmas separately. The construction is a pure structure instance: each field is filled by an already-proved sibling lemma.
Claim. There exists a certificate recording that (i) the domain cost vanishes on the diagonal ($C(r,r)=0$ for all $r\neq 0$), (ii) the domain cost is nonnegative for positive mass and distance parameters, and (iii) the canonical threshold is strictly positive.
background
The module treats strong gravitational lensing on the Recognition Science phi-ladder. The classical Einstein ring radius is $\theta_E=\sqrt{4GM/c^2\cdot D_{LS}/(D_L D_S)}$; under RS, distances of the form $D=\phi^k D_{\mathrm{Sch}}$ rescale the angle by $\phi^{k/2}$. The development is marked structural (zero sorry, zero axiom).
The certificate structure GravLens3Cert collects three positivity and normalization facts about a domain cost $C(m,e)$ used to compare mass and distance scales in the lensing geometry: vanishing on the diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold. Upstream, the foundation result that every recognition-event cost is nonnegative (via $J$-cost nonnegativity) supplies the conceptual template for the domain-cost nonnegativity field.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas that already establish diagonal vanishing of the domain cost, its nonnegativity on the positive orthant, and positivity of the canonical threshold. No additional reasoning occurs at this declaration.
why it matters
This is the inhabited certificate that the module's structural lensing claim is allowed to depend on. It closes the local interface between the $J$-cost / domain-cost layer and the Einstein-ring scaling $\theta_E\propto\phi^{k/2}$ at ladder distances $D=\phi^k D_{\mathrm{Sch}}$. No downstream consumers are recorded yet; the immediate sibling cert_inhabited is the natural next reference. In the broader framework it sits under the gravity domain rather than the T0–T8 forcing chain, but it inherits the nonnegativity discipline of the recognition cost $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.