pith. machine review for the scientific record. sign in
theorem proved term proof high

deltaStructural_eq_half_D3

show as:
view Lean formalization →

The structural correction for the tau lepton generation step equals 3/2 when spatial dimension is fixed at three. Lepton mass derivations on the Recognition Science phi-ladder cite this to fix the facet-mediated term without empirical fitting. The proof is a one-line wrapper applying the general deltaStructural_D3 result to the D = 3 case.

claimIn three spatial dimensions the structural correction for the tau step satisfies $Δ_{struct}(3) = 3/2$.

background

Recognition Science derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses. The function deltaStructural encodes the facet-vertex ratio: F = 2D faces each contribute 1/V where V = 2^{D-1} is the discrete vertex count per facet, so Δ(D) = F/V. The module contrasts this facet-mediated μ→τ step with the edge-mediated e→μ step that uses the continuous solid angle 4π. Upstream results include the voxel definition as the fundamental length quantum and the Physical structure requiring positive c, ħ, G in RS-native units.

proof idea

The proof is a one-line wrapper that applies the general deltaStructural_D3 theorem directly to the D = 3 case.

why it matters in Recognition Science

This theorem specializes the general structural delta to D = 3, confirming Δ(3) = 3/2 as required by the tau step derivation. It supports the module claim that the correction follows from face geometry without calibration and aligns with the forced D = 3 in the unified forcing chain (T8). No downstream uses appear yet.

scope and limits

formal statement (Lean)

 165theorem deltaStructural_eq_half_D3 : deltaStructural 3 = (3 : ℝ) / 2 := deltaStructural_D3

proof body

Term-mode proof.

 166
 167/-! ## The Face-Vertex Interpretation
 168
 169**Physical interpretation of the derivation**:
 170
 171The tau transition is mediated by the faces of the cubic voxel.
 172Each face is a 2D object (square in D=3) with V = 4 vertices.
 173
 174The radiative correction receives a contribution from each face,
 175but the contribution is "spread" over the face's vertices.
 176
 177Contribution per face-vertex pair: 1
 178Total contribution: F faces × 1 / V vertices per face = F/V = D/2
 179
 180This is NOT a fit — it follows from the face geometry.
 181-/
 182
 183/-- The face-vertex ratio F/V equals D/2 when V = 4 (the 2D case).
 184    Verified specifically for D = 3. -/

depends on (23)

Lean names referenced from this declaration's body.