dreamGeneratorCount_pos
plain-language theorem explainer
The theorem establishes that the number of DREAM virtue generators is strictly positive. Researchers extending Recognition Science ethics models would cite it to confirm the basis size for σ-preserving moves at D=3. The proof is a one-line wrapper that rewrites the count via its equality theorem and normalizes the resulting numerical inequality.
Claim. The cardinality of the DREAM virtue generator set is positive: $0 < 14$.
background
In the Virtue Generators from J-Cost module the DREAM generators are the 14 bidirectional moves in the vector space F₂³. Their count is given by 2 × (2^D - 1) evaluated at D=3, which equals 14. The upstream theorem dreamGeneratorCount_eq records this equality by reflexivity and notes that each generator corresponds to a bidirectional F₂³ move.
proof idea
The proof is a one-line wrapper. It applies the rewrite tactic to the equality theorem dreamGeneratorCount_eq, reducing the goal to 0 < 14, then invokes norm_num to discharge the numerical fact.
why it matters
This positivity result is bundled into the VirtueGeneratorsCert definition alongside the count equality, the Count Law derivation, and perfect cost. It upgrades the scaffold tag in the pre-Big-Bang paper §virtues to a structural theorem, confirming the 14-generator basis at D=3 from the forcing chain. The conjecture that these generators span every σ-preserving transformation remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.