Geometry Dihedral Angle Cubic Lattice Deficit Zero

The flat cubic hinge

A dihedral angle is the angle between two faces that meet along an edge. For a cube, every such angle is a right angle, 90 degrees, since adjacent faces are perpendicular. The declaration cubic_lattice_deficit_zero is a formal, machine-checked statement that four of these right angles, the four cubes that meet around any edge of the standard cubic lattice, sum to exactly 360 degrees, or 2π radians. This is the classical fact that the Z³ lattice is flat: no curvature is concentrated along its edges.

The result is proved in the framework's machine-checked library of formal theorems. It builds on a definition of a dihedral angle from Cayley-Menger data, the distances between points that determine a simplex's geometry. The proof first establishes that a cube's dihedral angle is π/2 exactly, then shows that four copies of this angle sum to 2π, and finally concludes that the deficit, defined as 2π minus the sum, is zero. The chain of reasoning is explicit and leaves no gap for an unstated assumption.

This flatness statement is a piece of the framework's program to discharge a hypothesis about Regge calculus, a discrete approach to general relativity where spacetime is built from flat simplices and curvature lives at hinges. In that setting, a zero deficit at a hinge means no curvature there. The cubic lattice result is the baseline identity for the simplest case: a flat, regular grid in three dimensions. It is a necessary check that the framework's definitions reproduce a known geometric fact before they are applied to curved spaces.

What the declaration does not claim is broader. It does not say that the cubic lattice is the only flat structure, nor that any physical space is actually a cubic lattice. It does not address curvature at vertices or along higher-dimensional faces. It is a statement about one specific configuration of four cubes around an edge, not a theorem about all of three-dimensional geometry. The proof is a foundation stone, not a cathedral.

/-- The deficit at a flat cubic hinge is zero (the baseline identity
    already present in `ReggeCalculus.cubic_lattice_flat` for the
    π/2 × 4 = 2π case, now lifted to the `DihedralAngle` API). -/
theorem cubic_lattice_deficit_zero :
    deficit [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] = 0 :=
  deficit_eq_zero_of_flat _ cubic_lattice_flatSum

/-- The cube dihedral is `π / 2` exactly. -/
theorem cube_dihedral_theta : cube_dihedral.theta = Real.pi / 2 := by
  unfold DihedralAngleData.theta cube_dihedral
  simp only
  exact Real.arccos_zero

/-- Four cube-dihedral angles (`π/2 + π/2 + π/2 + π/2 = 2π`) sum to `2π`:
    the classical "Z³ lattice is flat" statement. -/
theorem cubic_lattice_flatSum :
    FlatSumCondition [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] := by
  unfold FlatSumCondition sumThetas
  simp only [List.map, List.sum_cons, List.sum_nil, cube_dihedral_theta]
  ring

/-- At a flat hinge, the deficit is zero. -/
theorem deficit_eq_zero_of_flat (ds : List DihedralAngleData)
    (h : FlatSumCondition ds) : deficit ds = 0 := by
  unfold deficit
  rw [h]; ring

What this page does not claim

The cubic lattice is not claimed to be the only flat structure in three dimensions. No claim is made about the physical geometry of actual space being a cubic lattice. The result does not address curvature at vertices or along faces of dimension greater than one.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/DihedralAngle.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: