RSPrimitive
plain-language theorem explainer
RSPrimitive enumerates the five recognition primitives that tag finite domain axes to enforce independence in cross-domain combinations. Researchers building coupled-axis theorems cite it to distinguish axes by primitive rather than shared cardinality. The declaration is a direct inductive type with five constructors that derives decidable equality, representation, and finite-type instances.
Claim. The recognition primitives form the inductive type with constructors J-cost, phi-ladder, sigma-charge, q3-lattice, and gap-45.
background
The RS-Coupled Axes module supplies infrastructure for cross-domain combination theorems. Two finite axes of equal cardinality count as independent only when they carry distinct recognition-primitive tags. CoupledAxis packages a finite type Ix of cardinality n together with one such tag. The upstream jCost definition supplies the J-cost proxy, the real number of lives lost under a trolley choice.
proof idea
This is an inductive definition introducing exactly five constructors. The deriving clause installs DecidableEq, Repr, and Fintype instances automatically.
why it matters
RSPrimitive supplies the tags required by CoupledAxis and thereby enables the concrete axis definitions atmosphereAxis (phi-ladder), earthAxis (J-cost), and oceanAxis (sigma-charge). It also feeds the rsPrimitive_count theorem that fixes the total at five. The tagging rule directly implements the module's independence condition for cross-domain theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.