cert
plain-language theorem explainer
The definition cert constructs the VirtueGeneratorsCert record by supplying the four required fields from sibling results in the same module. Researchers on the pre-Big-Bang ethics section would cite it to close the structural count and cost properties for the 14 DREAM generators. It is a direct record construction that assembles the equality to 14, the derivation from the F₂³ count law, the zero-cost theorem, and the positivity statement.
Claim. cert is the certificate asserting that the DREAM generator count equals 14, that this count equals $2(2^3-1)$, that the J-cost of any nonzero virtue move vanishes ($virtueCost(b,b)=0$ for all $b≠0$), and that the generator count is positive.
background
The module upgrades the scaffold on virtue generators in the pre-Big-Bang paper. DREAM generators are the 14 bidirectional moves in F₂³ that preserve the σ-zero condition; their count follows from the Count Law at D=3. VirtueCost is the J-cost evaluated on the ratio of a virtue move, which vanishes exactly when the move is perfectly aligned. Upstream, dreamGeneratorCount_eq states dreamGeneratorCount=14 by reflexivity, while dreamCount_from_countLaw derives the same count as 2×(2³-1) via norm_num after unfolding. virtueCost_perfect shows the cost is zero by reduction to Jcost_unit0, and dreamGeneratorCount_pos confirms positivity.
proof idea
The definition is a one-line record constructor that directly assigns the four fields of VirtueGeneratorsCert to the corresponding sibling theorems: gen_count receives dreamGeneratorCount_eq, gen_count_from_law receives dreamCount_from_countLaw, cost_perfect receives virtueCost_perfect, and gen_positive receives dreamGeneratorCount_pos.
why it matters
This definition supplies the concrete witness that upgrades the virtue-generators claim from scaffold to partial theorem in the pre-Big-Bang paper §virtues. It closes the structural part of the 14-generator basis at D=3 (T8) while leaving the completeness conjecture open. The parent claim is the existence of a finite set of canonical σ-preserving micro-moves; downstream results would invoke cert to assert that the DREAM set satisfies the algebraic closure conditions under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.