zeroDeficitCert

formal source

  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
  62
  63structure FreudenthalCert where
  64  cube_data : cubeVertices = 8 ∧ cubeEdges = 12 ∧ cubeFaces = 6
  65  tet_count : freudenthalTetCount = 6
  66  new_hinges : newHinges = 13
  67  body_angle : 6 * (1 : ℚ) / 6 = 1
  68  zero_deficit : ZeroDeficitCert
  69
  70def freudenthalCert : FreudenthalCert where
  71  cube_data := ⟨rfl, rfl, rfl⟩
  72  tet_count := freudenthal_count
  73  new_hinges := rfl
  74  body_angle := body_diagonal_full_angle
  75  zero_deficit := zeroDeficitCert
  76
  77end IndisputableMonolith.Foundation.FreudenthalTriangulationCert