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

faceCount_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)

 112theorem faceCount_D3 : faceCount 3 = 6 := by native_decide

proof body

Term-mode proof.

 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. -/

depends on (20)

Lean names referenced from this declaration's body.