FundamentalZFAxiom
plain-language theorem explainer
The inductive definition enumerates the five core Zermelo-Fraenkel axioms adopted inside Recognition Science. Foundations researchers who reconstruct mathematics from the recognition lattice Q3 cite this list when they verify axiom counts or assemble structural certificates. The definition proceeds by direct enumeration of the five constructors together with automatic derivation of decidability and finiteness.
Claim. An inductive type whose constructors are extensionality, pairing, union, power set, and infinity.
background
Zermelo-Fraenkel axioms supply the standard foundation for mathematics. In Recognition Science the recognition lattice Q3 carries set-like structure, and the module isolates the five canonical axioms extensionality, pairing, union, power set, and infinity. These five correspond to configDim D times one out of the full nine ZF axioms. The power set of Q3 has cardinality 2^8 = 256.
proof idea
The declaration is introduced as a direct inductive definition that lists the five constructors. No lemmas are invoked; the deriving clauses for DecidableEq, Repr, BEq, and Fintype are supplied automatically by the type checker.
why it matters
This supplies the axiom enumeration required by the theorem that proves the cardinality equals five and by the structure that certifies the match to the power set cardinality 256. It anchors the set-theoretic foundation step in the Recognition Science derivation, linking to the eight-tick octave through the exponent 2^3 = 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.