base_shift
plain-language theorem explainer
The base shift assembles the zeroth-order geometric term for the electron mass shift as twice the wallpaper group count plus the cubic ledger fraction. Researchers deriving particle masses from Recognition Science topology cite this when separating the dual sector symmetry cover from radiative corrections. It is introduced as a direct definition that combines W with the ratio (W + E_total) over 4 E_passive.
Claim. The base shift is given by $2W + (W + E_0)/(4 E_p)$, where $W$ counts wallpaper groups, $E_0$ is the total edge count of the cubic ledger $Q_3$, and $E_p$ is the passive edge count.
background
The module derives the refined ledger fraction for the electron mass shift under T9 topology from the geometry of the cubic ledger $Q_3$. It fixes $E_0 = 12$ total edges and $E_p = 11$ passive edges, with $W$ defined as the wallpaper group count supplying face symmetries and set to 17. The base shift isolates the leading geometric contribution before the module adds the radiative terms $α^2$ and $E_0 α^3$ as stated in the module documentation.
proof idea
This is a direct definition that sets the base shift equal to the sum of twice the wallpaper group count and the precomputed ledger fraction. No lemmas or tactics are applied; it functions as a one-line assembly point referenced by downstream forcing theorems via unfolding or simplification.
why it matters
This supplies the base geometric term that JCostPerturbation theorems invoke to force the denominator scale $k=4$ and recover the explicit form 34 + 29/44. It realizes the base topology component of the T9 refined shift formula, which matches empirical mass ratios to $2×10^{-7}$. The construction ties into D = 3 spatial dimensions through the cubic ledger and the phi-ladder mass formula but leaves open full integration with higher-order J-cost perturbations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.