rsPrimitive_count
plain-language theorem explainer
The declaration establishes that the finite set of recognition primitives has cardinality five. Workers on cross-domain theorems in Recognition Science cite this cardinality when establishing independence conditions for tagged axes. The proof reduces to a decision procedure that evaluates the Fintype instance derived from the five-constructor inductive type.
Claim. The finite set of RS primitives has cardinality five: $|RSPrimitive| = 5$.
background
The module supplies infrastructure for cross-domain combination theorems. Two finite axes of equal cardinality count as independent only when tagged by distinct members of the set RSPrimitive. This set is introduced as an inductive type whose five constructors are jCost, phiLadder, sigmaCharge, q3Lattice and gap45, each carrying a distinct recognition meaning.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes the cardinality directly from the Fintype instance that is derived automatically from the inductive definition of RSPrimitive.
why it matters
The result fixes the number of available tags for domain axes and thereby supports the independence statements for triples and disjoint sums that appear as sibling declarations. It anchors the coupled-axis layer of the Recognition Science framework, ensuring that the five primitives suffice to label the fundamental axes without overlap, consistent with the eight-tick octave and the derivation of D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.