IndisputableMonolith.Gravity.GravitationalLens3FromJCost
Packages the RS link from the unique J-cost to a three-dimensional gravitational-lensing certificate. Gravity workers cite the domain cost, the canonical positive threshold, and the inhabited GravLens3Cert bundle. The module is mostly definitions and elementary nonnegativity/positivity facts over Constants and Cost, not a long derivation.
claimOn the RS cost $J(x)=(x+x^{-1})/2-1$, the module defines a domain cost for gravitational lensing, proves it is nonnegative and agrees with $J$ at the evaluation point, introduces a strictly positive canonical threshold, and packages an inhabited certificate $\mathrm{GravLens3Cert}$ asserting the three-dimensional lensing claim from that cost data.
background
Recognition Science forces a unique nonnegative cost $J$ on ratios (T5): $J(x)=\cosh(\log x)-1$, equivalently $(x+x^{-1})/2-1$, obeying the Recognition Composition Law. Gravity modules import that cost together with the RS constants (including the tick $\tau_0$) and specialize it to lensing observables.
This file sits in the Gravity domain. Sibling definitions introduce a domain-level cost functional built from $J$, record that it matches $J$ at the natural evaluation point, and prove nonnegativity. A canonical threshold is fixed and shown positive, giving a sharp numerical gate for the lensing certificate.
The three-dimensional character is intentional: the forcing chain already selects $D=3$ spatial dimensions (T8), so the lensing certificate is stated in that ambient dimension rather than as a free parameter.
proof idea
Definition module with short supporting lemmas, not a multi-step derivation. domainCost is introduced from the imported Cost layer; domainCost_at_eq and domainCost_nonneg are elementary rewrites and nonnegativity transfers from $J$. canonicalThreshold is a closed RS-native expression; canonicalThreshold_pos is a positivity check. GravLens3Cert bundles the cost/threshold data into a certificate type, with cert and cert_inhabited supplying a concrete inhabitant so downstream code can assume the 3D lensing package is available.
why it matters in Recognition Science
Closes a Gravity-side packaging step: lensing is not postulated geometrically but tied to the same $J$ that the foundation forces uniquely. The inhabited GravLens3Cert is the handoff object for any later theorem that needs "3D gravitational lensing from J-cost" as a hypothesis or export. It aligns with T5 (J-uniqueness) and T8 ($D=3$), and with the RS-native constants imported from Constants. No downstream used_by edges are recorded yet; the module is an export surface for the gravity stack rather than an internal lemma in a longer proved chain.
scope and limits
- Does not derive Einstein lensing equations or GR deflection angles from scratch.
- Does not prove uniqueness of the threshold beyond the chosen canonical expression.
- Does not treat $D\neq 3$ or variable-dimension lensing.
- Does not supply observational fits or numerical ray-tracing.
- Does not expand the full forcing chain T0–T8 inside this file.