IndisputableMonolith.Gravity.GravitationalLensingRS3FromJCost
Module packaging Recognition Science gravitational lensing (RS3) as a J-cost domain statement: a nonnegative domain cost, a positive canonical threshold, and an inhabited certificate bundle. Gravity theorists cite it when linking weak-lensing observables to the unique J-cost rather than a phenomenological deflection potential. Content is mostly definitions and elementary positivity/equality lemmas, not a full ray-trace derivation.
claimOn the RS gravity side one introduces a domain cost $C$ built from the J-cost $J(x)=(x+x^{-1})/2-1$, proves $C\ge 0$ and an evaluation identity, fixes a positive canonical threshold $\theta_*>0$, and packages these into an inhabited gravitational-lensing RS3 certificate.
background
Recognition Science forces a unique nonnegative cost $J$ on ratios (T5): $J(x)=\cosh(\log x)-1$. Gravity modules import that cost together with the RS tick constant $\tau_0$ and ask which geometric observables are controlled by $J$ rather than by an independent Newtonian potential.
This module sits in the Gravity domain. It defines a domain-level cost (domainCost) evaluated on lensing configurations, records that the cost is nonnegative, and isolates a positive canonical threshold against which lensing strength is compared. The certificate type GravLensRS3Cert bundles those facts so downstream gravity claims can assume a single inhabited witness rather than re-proving positivity each time.
Upstream material is thin: Constants supplies the RS time quantum; Cost supplies $J$ and its elementary algebraic properties. No full optical scalar or null-geodesic machinery is imported here.
proof idea
Definition-heavy module. domainCost is introduced from the J-cost; domainCost_at_eq is an evaluation identity; domainCost_nonneg is nonnegativity inherited from $J\ge 0$. canonicalThreshold is a fixed positive real; canonicalThreshold_pos is the positivity lemma. GravLensRS3Cert packages the above; cert and cert_inhabited supply a concrete inhabited instance. No deep tactic proof of a lensing equation appears; the argument structure is 'define cost, record positivity and threshold, inhabit the certificate'.
why it matters in Recognition Science
Gives the Gravity domain a reusable RS3 lensing certificate tied directly to J-cost uniqueness (forcing chain T5) rather than to a free deflection kernel. Downstream used_by edges are empty in the current graph, so the module is a leaf packaging layer: later weak-lensing or rotation-curve claims can import cert_inhabited instead of rebuilding domainCost_nonneg. It does not yet close a paper proposition on observed Einstein radii; it only standardizes the cost-side hypotheses those propositions will need. Framework landmarks touched: J-uniqueness and the cost composition law as the sole source of the domain cost.
scope and limits
- Does not derive the thin-lens deflection angle or magnification matrix from Einstein equations.
- Does not prove observational bounds on Einstein radii or shear spectra.
- Does not connect domainCost to the RS mass ladder or $\phi$-rungs.
- Does not treat strong-lensing time delays or multi-image parity.
- Does not claim a numerical match to measured $H_0$ or $\Omega_m$ from lensing.