generation_ordering_general
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of E_pass or W at any specific d.
- Does not derive the mass formula or rung integers themselves.
- Does not address physical interpretation beyond the combinatorial count.
- Does not extend the ordering to non-integer dimensions.
formal statement (Lean)
215theorem generation_ordering_general (d : ℕ) (hd : 2 ≤ d) :
216 0 < passive_field_edges d ∧
217 passive_field_edges d < passive_field_edges d + cube_faces d := by
proof body
Tactic-mode proof.
218 constructor
219 · unfold passive_field_edges cube_edges active_edges_per_tick
220 have : d * 2 ^ (d - 1) ≥ 2 := by
221 have hd1 : 1 ≤ d - 1 + 1 := by omega
222 calc d * 2 ^ (d - 1) ≥ 2 * 2 ^ (2 - 1) := by
223 apply Nat.mul_le_mul hd (Nat.pow_le_pow_right (by norm_num) (by omega))
224 _ = 4 := by norm_num
225 _ ≥ 2 := by norm_num
226 omega
227 · unfold cube_faces
228 omega
229
230/-- W_endo(D) = E_pass(D) + F(D) — the endogenous wallpaper count. -/