ledger_fraction_exact
plain-language theorem explainer
The lemma establishes that the ledger fraction in the electron mass derivation equals exactly 29/44. Researchers deriving forced particle masses from T8 ledger quantization in Recognition Science would cite this rational value to fix subsequent bounds. The proof is a one-line term reduction that unfolds the geometric edge counts and wallpaper groups then normalizes the resulting arithmetic.
Claim. The ledger fraction in the electron mass ledger quantization equals exactly $29/44$.
background
The module proves the electron mass formula is forced from T8 ledger quantization together with geometric constants. Key upstream definitions are active edges per tick equal to 1, cube edges for dimension d given by d times 2 to the power d-1, passive field edges as cube edges minus the active count (11 for d=3), and wallpaper groups fixed at 17. E_passive is the passive edge count of 11 and W is the anchor total in the mass formula.
proof idea
The term proof applies a single simp that unfolds ledger_fraction together with W, E_total, E_passive, wallpaper_groups, cube_edges, passive_field_edges, and active_edges_per_tick, then invokes norm_num to confirm the rational identity.
why it matters
This exact equality is invoked by the downstream base_shift_bounds lemma to obtain numerical bounds on the base shift. It completes a step in the T9 necessity argument that the electron mass is determined by the Recognition Science chain from T0 through T8, incorporating D=3 and the 17 wallpaper groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.