ledger_fraction
plain-language theorem explainer
The ledger_fraction definition supplies the rational (W + E_total) / (4 E_passive) that enters the base shift for the electron mass topology. Mass topology researchers cite it when closing the denominator coefficient in the refined shift expression. It is a direct abbreviation of the geometric counts from the cubic ledger Q3 with no additional lemmas required.
Claim. The base topological fraction is defined as $ (W + E_{total}) / (4 E_{passive}) $, where $W$ is the wallpaper group count, $E_{total}$ the total edges of the 3-cube, and $E_{passive}$ the passive field edges.
background
In the T9 topology module the refined ledger fraction is introduced to derive the topological shift δ for the electron mass. The module constructs δ from the geometry of the cubic ledger Q3, with W = 17 for wallpaper groups (face symmetries), E_total = 12 for total edges, and E_passive = 11 for passive edges. Upstream results from the Anchor module supply the counts: E_passive as passive_field_edges D (D = 3), E_total as cube_edges D, and W as wallpaper_groups.
proof idea
This is a one-line definition that directly computes the rational (W + E_total) / (4 * E_passive) from the imported constants. No tactics or lemmas are applied beyond the arithmetic division.
why it matters
This definition anchors the base shift in the JCostPerturbation theorems, where it is used to prove that the denominator must be 4 and to obtain base_shift = 34 + 29/44. It fills the geometric part of the T9 refined shift formula in the Recognition Science chain, connecting the cubic ledger topology to the mass ladder. Downstream results invoke it to close the forcing of the shift parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.