tau_values
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 in Recognition Science
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.
scope and limits
- Does not prove physical correctness of the assigned rungs.
- Does not extend tau beyond the three listed arguments.
- Does not derive tau from the J-function or Recognition Composition Law.
- Does not assert numerical match to measured lepton masses.
formal statement (Lean)
139theorem tau_values : tau 0 = 0 ∧ tau 1 = 11 ∧ tau 2 = 17 := by
proof body
Term-mode proof.
140 simp only [tau, Anchor.E_passive, Anchor.W, passive_field_edges, cube_edges,
141 active_edges_per_tick, D, wallpaper_groups]
142 norm_num
143
144/-- Rung integers for charged leptons.
145 e: 2 (baseline), mu: 2 + tau(1) = 13, tau: 2 + tau(2) = 19 -/