pith. machine review for the scientific record. sign in
def definition def or abbrev high

deltaStructural

show as:
view Lean formalization →

The definition supplies the dimension correction Δ(D) as the ratio of face count to face-vertex count in a D-dimensional hypercube. Researchers deriving lepton generation steps from first principles would cite it to fix the μ→τ correction at D=3 without fitting. It is realized as the direct quotient of the two geometric counts faceCount and faceVertexCount.

claimLet $F(D)=2D$ denote the number of $(D-1)$-faces of the $D$-cube and let $V(D)=2^{D-1}$ denote the number of vertices on each such face. The structural correction is then defined by $Δ(D) := F(D)/V(D)$.

background

The module derives the dimension-dependent correction Δ(D) from hypercube geometry without calibration to observed masses. Face count is defined as twice the dimension while vertex count per face is the power of two for the lower-dimensional cube. The upstream theorem from PrimitiveDistinction supplies the seven axioms that reduce to four structural conditions plus three definitional facts.

proof idea

The definition is a one-line wrapper that applies the quotient of faceCount D and faceVertexCount D after casting both to reals.

why it matters in Recognition Science

It supplies the geometric input to the main theorem delta_D3_derived, which equates the structural and axis-additive expressions at D=3 and confirms Δ(3)=3/2 follows from cube geometry alone. This closes the facet-mediated step in the lepton ladder and aligns with the eight-tick octave and D=3 forced by the unified forcing chain.

scope and limits

formal statement (Lean)

 121noncomputable def deltaStructural (D : ℕ) : ℝ :=

proof body

Definition body.

 122  (faceCount D : ℝ) / (faceVertexCount D : ℝ)
 123
 124/-- The axis-additive formula (from exclusivity proof). -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.