tau_values
plain-language theorem explainer
The theorem fixes the initial values of the tau sequence at 0, 11, and 17. These supply the additive rung corrections for the charged leptons on the phi-ladder, with electron at baseline 2, muon at 13, and tau at 19. The result is required by the mass formulas in the Anchor module. The proof is a one-line term wrapper that unfolds tau together with the cube-geometry constants and evaluates the arithmetic by norm_num.
Claim. $tau(0) = 0 land tau(1) = 11 land tau(2) = 17$, where $tau$ encodes the passive-edge and wallpaper-group offsets that shift the baseline rung 2 for the charged leptons in the Recognition mass ladder.
background
The Masses.Anchor module derives all sector constants from D=3 cube geometry. Total edges equal cube_edges(3) = 3 * 2^(3-1) = 12. Passive field edges are then defined as cube_edges(d) minus active_edges_per_tick, yielding E_passive = 11. The crystallographic constant W is wallpaper_groups = 17. The function tau returns these values at the first three arguments to set the lepton rung integers.
proof idea
The proof is a term-mode one-liner. It applies simp only to the definitions tau, E_passive, W, passive_field_edges, cube_edges, active_edges_per_tick, D, and wallpaper_groups, then discharges the resulting numeric goals with norm_num.
why it matters
This supplies the concrete rung offsets required by the lepton mass formulas that sit downstream of the D=3 forcing step (T8) and the eight-tick octave. It closes the derivation of the charged-lepton rungs that enter the phi-ladder mass expression yardstick * phi^(rung - 8 + gap(Z)). The module anchors every constant to cube_edges and wallpaper_groups without external parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.