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

deltaAxisAdditive_D3

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 135theorem deltaAxisAdditive_D3 : deltaAxisAdditive 3 = 3 / 2 := by

proof body

Term-mode proof.

 136  unfold deltaAxisAdditive
 137  norm_num
 138
 139/-- **MAIN THEOREM**: At the physical dimension D = 3, the structural
 140    derivation and the axis-additive formula give the same result.
 141
 142    This means Δ(3) = 3/2 is derived from cube geometry, not calibrated. -/

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.