cert
plain-language theorem explainer
Packages a gravitational-lensing certificate: the domain cost vanishes on the diagonal for every nonzero scale, and the canonical threshold is strictly positive. Astrophysicists working the RS lensing stack cite it as the inhabited witness for the module's certification structure. Construction is a one-line structure instance wiring two already-proved sibling facts.
Claim. There exists a certificate asserting (i) for every real $r \neq 0$, the gravitational-lensing domain cost satisfies $C(r,r)=0$, and (ii) the canonical threshold $T$ obeys $T>0$.
background
In the Recognition Science astrophysics layer, gravitational lensing is treated through a domain cost $C$ (here domainCost) built from the global J-cost of the Cost module. The diagonal condition $C(r,r)=0$ for $r\neq 0$ says that a pure self-comparison at fixed scale carries no excess recognition cost, matching the fixed-point behaviour of $J$ under the Recognition Composition Law.
The companion datum is a canonical threshold (a positive real cut used to separate detectable lensing deflections from noise). The module imports only Mathlib, Constants, and Cost, so the threshold is an RS-native positive constant rather than an empirical fit.
GravitationalLensing_v2Cert is the structure that bundles exactly these two propositions. The present definition supplies one concrete inhabitant of that structure.
proof idea
One-line structure instance. The field cost_at_eq is filled by the sibling lemma domainCost_at_eq; the field threshold_pos is filled by the sibling lemma canonicalThreshold_pos. No further tactic work occurs.
why it matters
Gives the module an explicit, named certificate value that downstream astrophysics developments can require as a hypothesis or can inhabit via cert_inhabited. In the broader RS stack this sits under the astrophysics domain rather than the T0–T8 forcing chain; it does not itself force $\phi$, the eight-tick octave, or $D=3$, but it keeps lensing costs aligned with the same J-cost that those landmarks determine. With zero used_by edges at present, its main role is to close the local certification interface so later lensing theorems can assume a single packaged witness instead of two separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.