fundamentalZFCount
plain-language theorem explainer
The theorem establishes that the inductive type enumerating the five core Zermelo-Fraenkel axioms retained in Recognition Science has cardinality five. Foundation researchers cite it when confirming that the selected axioms align with the framework's dimensional parameter. The proof is a one-line decision procedure that exploits the Fintype instance derived from the inductive definition.
Claim. The cardinality of the type of fundamental Zermelo-Fraenkel axioms (extensionality, pairing, union, power set, infinity) equals five: $|F| = 5$ where $F$ is the finite type with those five constructors.
background
In the Set Theory from RS module, Zermelo-Fraenkel axioms supply the mathematical foundation while the recognition lattice Q₃ supplies the structured set. The inductive type FundamentalZFAxiom lists exactly the five canonical axioms: extensionality, pairing, union, power set, and infinity. The module states these five are the most fundamental subset and correspond to configDim D. Upstream results on spectral emergence define Q₃ as simultaneously forcing the gauge group SU(3) × SU(2) × U(1), three generations, and 24 chiral fermions, thereby giving Q₃ the set-theoretic structure required for the axiom enumeration.
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 automatically derived from the inductive definition of FundamentalZFAxiom and its five constructors.
why it matters
This result populates the five_axioms field inside the setTheoryCert definition, which also records the power-set cardinality 256 and the structure match to 2_2D. It supplies the set-theoretic foundation step that reduces the nine ZF axioms to the five retained in RS, linking the count to the recognition lattice Q₃. The mapping of the remaining four axioms remains an open question in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.