powerSetQ3
plain-language theorem explainer
The definition assigns the power set cardinality of the recognition lattice Q₃ to 256. Researchers formalizing ZF axioms inside the Recognition Science framework cite it to fix the numerical anchor for the five fundamental axioms. The assignment is a direct constant that later theorems reduce to 2 raised to the power of eight.
Claim. The power set of the recognition lattice $Q_3$ has cardinality $2^8 = 256$.
background
The module embeds five canonical ZF axioms (extensionality, pairing, union, power set, infinity) into Recognition Science as configDim D. The recognition lattice Q₃ is the base set whose power set is denoted |ℱ(F₂³)|. Module documentation states the key relation |ℱ(F₂³)| = 2^8 = 256, linking the lattice directly to the eight-tick octave.
proof idea
The definition is a one-line constant assignment that evaluates 2^8. No lemmas or tactics are invoked; the value is supplied as a primitive for downstream use.
why it matters
This definition supplies the power_set_256 field of the SetTheoryCert structure and is invoked by the theorems powerSetQ3_eq_256 and powerSetQ3_2_2D. It realizes the framework step that equates the power set of Q₃ with 2^(2^D) for D = 3, closing the link to the eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.