`cubeEdges_eq`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.FreudenthalTriangulationCert on GitHub at line 31.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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
  57
  58def zeroDeficitCert : ZeroDeficitCert where
  59  body_diagonal_deficit_zero := trivial
  60  face_diagonal_deficit_zero := trivial
  61  new_hinge_count := rfl

papers checked against this theorem

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