r0_eq_alt
plain-language theorem explainer
The theorem shows that the sector radius r0(s) for each of the four Anchor sectors equals its alternative expression built from cube edge counts and the 17 wallpaper groups. Mass ladder researchers in Recognition Science cite it to confirm that sector yardsticks carry no free parameters. The proof runs by case split on the sector, followed by definitional simplification against the geometric constants and numerical normalization.
Claim. For every sector $s$, the radius function $r_0(s)$ equals the alternative geometric expression $r0_{alt}(s)$ obtained from $D=3$ hypercube combinatorics and the crystallographic count of 17 wallpaper groups.
background
Anchor.Sector is the inductive type with four constructors corresponding to Lepton, UpQuark, DownQuark and Electroweak. The function r0 computes the sector yardstick from total edges W, while r0_alt supplies the explicit formula derived in the same module. Cube edges are given by $d·2^{d-1}$, passive field edges subtract the single active edge per tick, and wallpaper groups is the fixed crystallographic constant 17. The module AnchorDerivation supplies these alternative formulas to verify that the constants in Anchor.lean arise solely from $D=3$ and the listed geometric inputs.
proof idea
The term proof begins with exhaustive case analysis on the four sectors. Each case applies simp to unfold Anchor.r0, r0_alt, W, E_total, A together with the constants wallpaper_groups, cube_edges, active_edges_per_tick and the sector-specific values Wz, Etz, Az. The resulting numerical expressions are discharged by norm_num.
why it matters
The result completes the verification chain that sector constants trace to T8 ($D=3$), cube_edges and wallpaper_groups without external parameters, directly supporting the mass formula yardstick · phi^(rung-8+gap(Z)). It supplies the final link between the geometric derivations in AlphaDerivation and the Anchor definitions used for mass ladder placement. No downstream theorems yet depend on it, leaving open its integration into explicit mass computations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.