def
definition
faceCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation on GitHub at line 103.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
100/-! ## Cube Geometry -/
101
102/-- Face count of D-hypercube: F = 2D. -/
103def faceCount (D : ℕ) : ℕ := 2 * D
104
105/-- Vertex count of a (D-1)-hypercube (the face of a D-cube). -/
106def faceVertexCount (D : ℕ) : ℕ := 2^(D - 1)
107
108/-- In D=3, each face is a 2D square with 4 vertices. -/
109theorem faceVertexCount_D3 : faceVertexCount 3 = 4 := by native_decide
110
111/-- In D=3, there are 6 faces. -/
112theorem faceCount_D3 : faceCount 3 = 6 := by native_decide
113
114/-! ## The Structural Derivation -/
115
116/-- The structurally derived dimension correction.
117 Formula: Δ(D) = F(D) / V(D) = 2D / 2^{D-1} = D / 2^{D-2}
118
119 This is derived from: each face contributes, normalized by
120 the number of vertices of that face. -/
121noncomputable def deltaStructural (D : ℕ) : ℝ :=
122 (faceCount D : ℝ) / (faceVertexCount D : ℝ)
123
124/-- The axis-additive formula (from exclusivity proof). -/
125noncomputable def deltaAxisAdditive (D : ℕ) : ℝ := (D : ℝ) / 2
126
127/-! ## Key Theorem: The Two Formulas Agree at D = 3 -/
128
129/-- The structural formula equals 3/2 at D = 3. -/
130theorem deltaStructural_D3 : deltaStructural 3 = 3 / 2 := by
131 unfold deltaStructural faceCount faceVertexCount
132 norm_num
133