generation_ordering_general
plain-language theorem explainer
The theorem shows that for every natural number d at least 2 the passive field edge count E_pass(d) is strictly positive and strictly less than the endogenous wallpaper count W_endo(d). Mass-baseline derivations in Recognition Science cite it to confirm the general generation ordering before specializing to D=3. The proof is a short tactic script that unfolds the hypercube definitions and dispatches both sides of the conjunction with omega after a brief Nat inequality.
Claim. For every natural number $d$ with $dgeq 2$, let $E_{rm pass}(d)=dcdot2^{d-1}-1$ be the number of passive field edges and let $W(d)=E_{rm pass}(d)+2d$ be the endogenous wallpaper count. Then $0<E_{rm pass}(d)<W(d)$.
background
The BaselineDerivation module upgrades several boundary assumptions about rung integers to derived statements by counting features of the D-hypercube. Passive field edges are defined as cube_edges(d) minus the single active edge per tick, where cube_edges(d) equals d times 2 to the power d-1. Cube faces equal 2d. The endogenous wallpaper count W_endo(d) is then their sum. The module documentation states that every integer here traces to the single input D=3 and lists generation ordering (B-14) as 0 less than E_pass less than W, with the concrete D=3 value 0 less than 11 less than 17.
proof idea
The tactic proof opens with constructor to split the conjunction. The left conjunct unfolds passive_field_edges, cube_edges and active_edges_per_tick, then proves d times 2 to the d-1 is at least 2 for d at least 2 by a Nat.mul_le_mul step followed by norm_num and omega. The right conjunct unfolds cube_faces and finishes immediately with omega.
why it matters
The result supplies the general form of B-14 in the cube-geometry table, ensuring the inequality 0 less than E_pass less than W holds for all d at least 2 before the framework specializes to three spatial dimensions. It thereby supports the subsequent mass-ladder and lepton-generation constructions that rely on this ordering. Although no downstream theorems yet invoke it, the declaration closes one of the listed scaffolding items in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.