IndisputableMonolith.Cosmology.GravitationalLensingFromRS
The module develops the mathematical objects needed to express gravitational lensing within Recognition Science cosmology. Researchers deriving light deflection from the J-function and phi-ladder would cite the regime and angle definitions. It consists entirely of type and function definitions with no theorems or proofs.
claimIntroduces LensingRegime as a classification of lensing conditions, deflectionAngle as the computed light deflection, deflection_ratio and deflection_pos as auxiliary quantities, and GravitationalLensingCert as a certification structure, all in RS-native units with τ₀ = 1 tick.
background
This module belongs to the Cosmology domain. It imports IndisputableMonolith.Constants, whose doc-comment identifies the fundamental RS time quantum as τ₀ = 1 tick. Sibling definitions include LensingRegime, lensingRegime_count, deflectionAngle, deflection_ratio, deflection_pos, GravitationalLensingCert, and gravitationalLensingCert.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The definitions supply building blocks for gravitational lensing calculations in RS cosmology. No immediate parent theorems appear in the used_by edges, indicating the module serves as an interface layer for future derivations that connect to the forcing chain T0-T8 and the D = 3 spatial dimensions.
scope and limits
- Does not derive explicit formulas linking deflection to mass distributions.
- Does not verify consistency with observed lensing data.
- Does not extend to strong lensing or multiple images.