lensingRegime_count
plain-language theorem explainer
The theorem establishes that the Recognition Science cosmology enumerates exactly five gravitational lensing regimes. Researchers modeling light deflection would cite the count to organize regime-specific predictions on the phi-ladder. The proof is a one-line decision procedure that counts the constructors of the inductive regime enumeration.
Claim. The set of gravitational lensing regimes has cardinality five: $ |$ {weak lensing, strong lensing, microlensing, cluster lensing, time-delay lensing} $ | = 5 $.
background
The Gravitational Lensing from RS module introduces five canonical regimes that correspond to a configuration dimension of 5. These regimes are weak lensing, strong lensing, microlensing, cluster lensing, and time-delay lensing, each tied to a deflection angle on the phi-ladder. This provides the local theoretical setting for certifying lensing effects within the broader Recognition Science framework derived from the forcing chain. The upstream inductive definition supplies the explicit list of regimes whose finite cardinality is asserted here.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes the Fintype cardinality by inspecting the five constructors of the regime inductive type and verifies equality to 5.
why it matters
This declaration populates the five_regimes field of gravitationalLensingCert, which certifies the lensing framework in the cosmology module. It directly implements the module statement of five regimes each with a characteristic deflection angle on the phi-ladder. In the Recognition Science context, it extends the phi-ladder structure to cosmological applications, consistent with the eight-tick octave and dimension assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.