Az_eq
plain-language theorem explainer
Az equals 1 because it is defined directly as the active edges per atomic tick, fixed at unity by the T2 rule. Mass sector derivations cite this normalization to anchor B_pow and r0 calculations without free parameters. The proof is a one-line simplification that unfolds the definition and substitutes the constant value.
Claim. $A_z = 1$, where $A_z$ is the integer count of active edges per atomic tick.
background
The module verifies sector constants derived from first principles using D = 3 spatial dimensions and cube edge counting. Cube edges total 12, so passive field edges are 11 and active edges per tick are fixed at 1. Upstream, active_edges_per_tick is defined as the natural number 1 with the note that it records one edge transition per tick by T2. Az is the sibling definition that casts this count to an integer for use in anchor formulas.
proof idea
One-line wrapper that applies simp to unfold Az as active_edges_per_tick and substitute the constant value 1.
why it matters
This equality closes the normalization step for the anchor derivation of sector yardsticks B_pow and r0. It supports the parameter-free chain from D = 3 and cube combinatorics to explicit values such as B_pow = -22 for leptons. The module documentation states that all sector constants trace back to these counts with no fitting to mass data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.