active_edges_per_tick
plain-language theorem explainer
Active edges per atomic tick is fixed at the constant 1, counting the single edge transition that occurs in each recognition event on the D=3 cubic ledger. Derivations of the fine-structure constant and mass-ladder constructions cite this value when subtracting from total cube edges to isolate the 11 passive field edges. The definition is a direct constant assignment that implements the T2 forcing step without further computation.
Claim. The active edge count per atomic tick is defined by the constant $A = 1$, where this counts the single transition edge traversed during one atomic tick on the cubic ledger in three dimensions.
background
The Alpha Derivation module constructs α⁻¹ from the geometry of the cubic ledger forced by the Meta-Principle on Z³. The unit cell is the cube Q₃ whose edge count is given by D · 2^(D-1). One atomic tick traverses exactly one edge; the remainder dress the vacuum interaction. MODULE_DOC states: “Active edges per tick: 1 (the transition)” and “Passive (field) edges: 12 - 1 = 11”. Upstream results supply the lattice summation operator total from DiscreteVorticity and the phi-ladder hypothesis structure from PhiLadderLattice.
proof idea
Direct definition that assigns the natural number 1. No lemmas or tactics are invoked; the declaration serves as the base constant referenced by all subsequent edge-counting identities.
why it matters
The definition supplies the active-edge term that appears in alpha_ingredients_from_D3_cube, passive_field_edges, eleven_is_passive_edges, and the mass-anchor theorems A, B_pow_Electroweak_eq. It realizes the T2 step of the unified forcing chain by fixing one transition per tick, thereby producing the factor 11 that multiplies the solid angle to seed α⁻¹. It also anchors the D = 3 cube counting used throughout the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.