cert
plain-language theorem explainer
Packages the three structural facts needed for the RS gravitational-lensing certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the RS3 lensing coefficient from J-cost will pull this bundle. The definition is a pure structure inhabitant wiring three already-proved sibling lemmas.
Claim. There is 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_*$ is strictly positive.
background
The module develops the Recognition Science gravitational-lensing coefficient from the J-cost. In GR the light-deflection angle is $\alpha=4GM/(c^2 b)$. RS specializes impact parameters on the $\varphi$-ladder: at $b=r_{\mathrm{Sch}}\varphi$ one obtains $\alpha=4J(\varphi)\approx 0.472$ rad, and at $b=r_{\mathrm{Sch}}\varphi^5$ one obtains $\alpha=4/\varphi^4\approx 0.94$ arcsec.
The domain cost is the local cost functional on mass/energy (or radius) pairs used to state the structural side-conditions of that derivation. The certificate structure GravLensRS3Cert simply collects three elementary properties of that cost and of the canonical threshold: diagonal vanishing, nonnegativity, and positivity of the threshold. Upstream, nonnegativity of recognition cost is already known from ObserverForcing (cost_nonneg: the cost of any recognition event is non-negative), which underwrites the domain-cost nonnegativity lemma wired here.
proof idea
One-line structure inhabitant. The three fields of GravLensRS3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional reasoning occurs at this declaration.
why it matters
This is the named certificate object for the RS3 gravitational-lensing module (status: structural theorem, 0 sorry, 0 axiom). It freezes the three side-conditions that any downstream consumer of the J-cost lensing coefficient must assume: cost vanishes when the two arguments coincide, cost is a nonnegative defect, and the canonical threshold used to mark the $\varphi$-ladder impact parameters is positive.
In the broader framework it sits under the gravity domain and ties the classical Einstein deflection formula to the T5 J-uniqueness cost $J(x)=(x+x^{-1})/2-1$ and the T6 golden-ratio fixed point $\varphi$. The numerical specializations $\alpha=4J(\varphi)$ and $\alpha=4/\varphi^4$ are the concrete RS predictions the certificate underwrites. No downstream theorems currently depend on it in the graph, so it functions as the module's exportable proof package rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.