Physics Lepton Generations Tau Step Exclusivity

The Tau Step Coefficient

The tau generation step is a formula in the Recognition Science framework that relates the muon and tau lepton generations. The step is written as step_μ→τ = F − (W + D/2) · α, where F, W, and α are framework quantities and D is the spatial dimension. The term (W + D/2) is the α-correction coefficient. The question the module answers is why this coefficient is (W + D/2) and not one of several alternatives that all give the same numerical value in three dimensions.

In three dimensions, the alternatives W + F/4, W + E/8, W + D(D−1)/4, and W + D²/6 all evaluate to W + 3/2, the same as W + D/2. The module separates these into two categories. The first is algebraically equivalent: F/4 equals D/2 because the hypercube face count F is 2D by definition, so W + F/4 is the same formula in different notation. The second category is numerically coincident but algebraically distinct: E/8, D(D−1)/4, and D²/6 differ from D/2 in dimensions other than three.

The exclusivity result comes from two principles. The first, axis additivity, requires that a correction term built from independent per-axis contributions satisfy f(0) = 0 and f(a+b) = f(a) + f(b), making the correction linear in D with no cross-axis interaction terms. The second is calibration at D=3: the tau step requires the dimension correction to be 3/2 when D=3. Under these two conditions, the dimension correction is uniquely D/2. The alternatives E/8, D(D−1)/4, and D²/6 fail axis additivity, while F/4 is identical to D/2.

The machine-checked library of formal theorems proves this uniqueness. The theorem admissible_unique states that any function f from natural numbers to reals satisfying the admissible correction structure, which bundles axis additivity with the D=3 calibration, must equal f(d) = d/2 for all d. A companion theorem, tau_correction_unique_admissible, restates this as the correction being exactly correction_D_half. The library also proves the negative results: E_eighth_not_axisAdditive, D_quad1_not_axisAdditive, and D_quad2_not_axisAdditive each show the corresponding alternative fails the additivity condition.

What this establishes in plain language is a uniqueness claim with a precise scope. The coefficient (W + D/2) is not chosen because it matches data at D=3; it is forced once the two structural rules are accepted. The alternatives that agree numerically at D=3 are ruled out by a principle that has content in other dimensions. The framework's contribution is not the numerical agreement but the proof that the agreement is not a coincidence under the stated axioms.

/-- Uniqueness: any admissible correction is exactly D/2. -/
theorem admissible_unique (f : ℕ → ℝ) (h : AdmissibleCorrection f) :
    ∀ d : ℕ, f d = (d : ℝ) / 2 := by
  have hlin := axisAdditive_linear f h.axisAdditive
  -- use calibration at d=3 to solve for f(1)
  have h3 : f 3 = (3 : ℝ) * f 1 := hlin 3
  have hf1 : f 1 = (1 : ℝ) / 2 := by
    -- from f3 = 3/2 = 3*f1
    have : (3 : ℝ) * f 1 = (3 : ℝ) / 2 := by
      -- rewrite h3 using calib
      rw [← h3, h.calib_D3]
    -- divide by 3
    have h3ne : (3 : ℝ) ≠ 0 := by norm_num
    -- f1 = (3/2)/3 = 1/2
    field_simp [h3ne] at this
    -- `this` is now: 3 * (2 * f1) = 3  (or equivalent); solve
    nlinarith
  intro d
  have : f d = (d : ℝ) * f 1 := hlin d
  -- substitute f1 = 1/2
  rw [this, hf1]
  ring

/-- E/8 is not axis-additive (witness: 2+2). -/
theorem E_eighth_not_axisAdditive : ¬ AxisAdditive correction_E_eighth := by
  intro h
  rcases h with ⟨h0, hadd⟩
  have h22 : correction_E_eighth (2 + 2) = correction_E_eighth 2 + correction_E_eighth 2 := hadd 2 2
  -- compute both sides
  unfold correction_E_eighth at h22
  simp [cube_edges] at h22
  -- LHS = 4, RHS = 1
  norm_num at h22

/-- D(D-1)/4 is not axis-additive (witness: 1+1). -/
theorem D_quad1_not_axisAdditive : ¬ AxisAdditive correction_D_quad1 := by
  intro h
  rcases h with ⟨h0, hadd⟩
  have h11 : correction_D_quad1 (1 + 1) = correction_D_quad1 1 + correction_D_quad1 1 := hadd 1 1
  unfold correction_D_quad1 at h11
  norm_num at h11

/-- D²/6 is not axis-additive (witness: 1+1). -/
theorem D_quad2_not_axisAdditive : ¬ AxisAdditive correction_D_quad2 := by
  intro h
  rcases h with ⟨h0, hadd⟩
  have h11 : correction_D_quad2 (1 + 1) = correction_D_quad2 1 + correction_D_quad2 1 := hadd 1 1
  unfold correction_D_quad2 at h11
  norm_num at h11

/-- **Key Identity**: F/4 = D/2 for ALL dimensions.
    This is not numerical coincidence—it's algebraic identity. -/
theorem F_quarter_eq_D_half : ∀ d : ℕ, correction_F_quarter d = correction_D_half d := by
  intro d
  unfold correction_F_quarter correction_D_half
  -- (2*d)/4 = d/2
  simp [cube_faces]
  ring

What this page does not claim

The module does not derive the tau generation step formula itself, only the uniqueness of one coefficient within it. The numerical agreement at D=3 is not evidence for the framework; the exclusivity proof is the claim. The framework does not claim the tau step coefficient is measured or empirically confirmed.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/LeptonGenerations/TauStepExclusivity.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: