`cubeEdges`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.FreudenthalTriangulationCert
domain: Foundation
line: 26 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.FreudenthalTriangulationCert on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  23/-- Unit cube vertex count. -/
  24def cubeVertices : ℕ := 8
  25/-- Unit cube edge count. -/
  26def cubeEdges : ℕ := 12
  27/-- Unit cube face count. -/
  28def cubeFaces : ℕ := 6
  29
  30theorem cubeVertices_eq : cubeVertices = 8 := rfl
  31theorem cubeEdges_eq : cubeEdges = 12 := rfl
  32theorem cubeFaces_eq : cubeFaces = 6 := rfl
  33
  34/-- Freudenthal decomposition: 6 tetrahedra. -/
  35def freudenthalTetCount : ℕ := 6
  36theorem freudenthal_count : freudenthalTetCount = 6 := rfl
  37
  38/-- Body diagonal shared by all 6 tetrahedra. -/
  39def bodyDiagonalTetrahedra : ℕ := 6
  40
  41/-- Sum of 6 × (1/6) = 1 (symbolic angle check). -/
  42theorem body_diagonal_full_angle : 6 * (1 : ℚ) / 6 = 1 := by norm_num
  43
  44/-- New hinges added by Freudenthal: 12 face diagonals + 1 body diagonal. -/
  45def newHinges : ℕ := 13
  46theorem newHinges_decomp : newHinges = 12 + 1 := rfl
  47
  48/-- Total hinges in simplicial refinement. -/
  49def totalHingesSimp : ℕ := cubeEdges + newHinges
  50theorem totalHinges_eq : totalHingesSimp = 25 := by decide
  51
  52/-- New hinges have zero deficit (key claim). -/
  53structure ZeroDeficitCert where
  54  body_diagonal_deficit_zero : True  -- all 6 angles sum to 2π
  55  face_diagonal_deficit_zero : True  -- all 4 angles sum to 2π
  56  new_hinge_count : newHinges = 13

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.