A
plain-language theorem explainer
The declaration sets the constant A to one active edge transition per fundamental tick. Mass derivations cite this value when building sector yardsticks from cube geometry at D=3. It is realized as a direct abbreviation to the upstream active-edges definition.
Claim. Let $A$ denote the number of active edges per atomic tick. Then $A = 1$.
background
The Masses.Anchor module centralizes parameter-free constants derived from cube geometry in three spatial dimensions. Total edges equal twelve, passive edges eleven, wallpaper groups seventeen, and A supplies the single active edge per tick. This A aliases the definition active_edges_per_tick, documented as one edge transition per tick by T2. Upstream results include parallel A definitions in IntegrationGap (the active edge count per fundamental tick) and Actualization (the operator that maps configurations to their realized states), but the present abbreviation specifically imports the edge-count constant for mass formulas.
proof idea
One-line abbreviation that directly references the active_edges_per_tick definition from the AlphaDerivation module.
why it matters
This supplies the active-edge count used to construct B_pow and r0 values for lepton, up-quark, down-quark, and electroweak sectors in the module table. It feeds downstream results including EnergyConservationDomainCert.applied, Noether spaceShift and timeShift, EulerLagrange.christoffel, and NarrativeGeodesic.BookerPlotFamily. The definition completes the cube-geometry step of the derivation chain at D=3, consistent with the eight-tick octave and phi-ladder landmarks. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.