Az
plain-language theorem explainer
Az supplies the integer value of active edges per atomic tick for sector mass derivations in Recognition Science. Researchers building alternative formulas for B_pow and r0 cite it when expressing sector-specific constants from cube combinatorics. The definition performs a direct type cast of the upstream natural number to ℤ.
Claim. Let $A_z$ be the integer equal to the number of active edges per atomic tick.
background
In the Masses.AnchorDerivation module, sector constants are verified as derived from first principles without free parameters. The derivation chain starts from D = 3, yielding cube_edges = 12, active_edges_per_tick = 1 by T2, passive_field_edges = 11, and wallpaper_groups = 17. The upstream definition states that active_edges_per_tick is the natural number 1, corresponding to one edge transition per atomic tick.
proof idea
The definition is a one-line cast of active_edges_per_tick to ℤ.
why it matters
This definition feeds the integer A_z into the alternative formulas B_pow_alt and r0_alt for all sectors, and into the verification theorems Az_eq, B_pow_eq_alt, and r0_eq_alt. It instantiates the T2 step of the forcing chain by setting the active edge count to 1, supporting the claim that all mass yardsticks follow from the Recognition Composition Law and the eight-tick octave without external parameters. The module confirms consistency with the main Anchor definitions for B_pow and r0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.