LensingRegime
plain-language theorem explainer
Recognition Science enumerates five gravitational lensing regimes as an inductive type to support uniform certification of deflection angles that scale by phi on the ladder. Cosmologists working within the RS framework cite this enumeration when proving that all regimes share the same phi-ratio property and positive deflection. The declaration is a direct inductive construction that automatically derives a Fintype instance whose cardinality equals five.
Claim. Let $R$ be the finite set of gravitational lensing regimes consisting of the five elements weak lensing, strong lensing, microlensing, cluster lensing, and time-delay lensing, equipped with decidable equality and a Fintype structure.
background
The module Gravitational Lensing from RS sets the local theoretical setting by introducing five canonical lensing regimes that correspond to configDim D = 5. Each regime carries a characteristic deflection angle placed on the phi-ladder of Recognition Science, where angles obey the self-similar scaling fixed by the forcing chain. The module documentation states: 'Five canonical lensing regimes (= configDim D = 5): weak lensing, strong lensing, microlensing, cluster lensing, time-delay. Each regime has a characteristic deflection angle on the φ-ladder.'
proof idea
The declaration is a direct inductive definition that enumerates the five regimes and derives the DecidableEq, Repr, BEq, and Fintype instances automatically. No lemmas are invoked; the finite cardinality follows immediately from the enumeration of five constructors.
why it matters
This definition supplies the type required by GravitationalLensingCert, which asserts Fintype.card LensingRegime = 5 together with the phi-ratio property for consecutive deflection angles and positivity of all angles. It also feeds the theorem lensingRegime_count that discharges the cardinality claim by decision. In the Recognition framework the enumeration closes the setup for cosmology depth, linking the five regimes to the phi-ladder scaling that originates in T5 J-uniqueness and T6 phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.