powerSetQ3_eq_256
plain-language theorem explainer
The equality establishes that the power set cardinality of the recognition lattice Q3 is exactly 256. Set theorists embedding ZF axioms into Recognition Science would cite this to confirm the power set axiom implementation matches the expected 2^(2^D) for three dimensions. The proof succeeds through direct numerical decision in the Lean kernel.
Claim. The cardinality of the power set of the recognition lattice $Q_3$ equals 256.
background
The module SetTheoryFromRS embeds Zermelo-Fraenkel set theory into Recognition Science by identifying the recognition lattice Q3 as the base set with structure. Five canonical ZF axioms are mapped to configDim D. The upstream definition powerSetQ3 computes the power set size directly as 2^8.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the numerical equality 2^8 = 256.
why it matters
This theorem supplies the power_set_256 field in the setTheoryCert definition, which certifies the set theory embedding from RS. It realizes the equality |F(F2^3)| = 2^8 = 256 stated in the module documentation, consistent with the eight-tick octave and D = 3 from the forcing chain. No open questions remain for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.