mass_topology_counts
plain-language theorem explainer
The theorem fixes the three-dimensional mass topology constants at twelve total cube edges, eleven passive edges, and seventeen wallpaper groups. Researchers deriving lepton mass corrections and J-cost perturbations cite these values to anchor ledger fractions and base shifts. The proof evaluates the underlying topology definitions directly via successive constructor splits and native decision procedures.
Claim. In three spatial dimensions the total number of cube edges is $E_ {total}=12$, the number of passive field edges is $E_{passive}=11$, and the number of wallpaper groups is $W=17$.
background
The module supplies the O4 perturbative closure for J-cost perturbations in the lepton correction path, tying geometric constants to canonical lepton-step definitions. E_total is defined as the edge count of a three-dimensional cube, E_passive as the passive subset obtained by subtracting one from the total, and W as the count of wallpaper groups that encode the two-dimensional face symmetries. These originate from the Anchor and MassTopology modules as direct evaluations of cube_edges 3, passive_field_edges 3, and wallpaper_groups, with the spatial dimension fixed at three by the upstream forcing chain.
proof idea
The term-mode proof opens the conjunction with constructor, then applies native_decide to each of the three resulting goals to confirm equality against the precomputed topology constants.
why it matters
This supplies the exact numerical inputs required by the downstream theorems that derive base_shift = 34 + 29/44 and force ledger-fraction denominators to equal four in the normalized geometric family. It closes the zeroth-order geometric part of the refined shift in the J-cost(1+α) channel, linking to the eight-tick octave and D=3 in the unified forcing chain. The constants appear explicitly in the alpha-band matching calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.