Geometry Dihedral Angle Cubic Lattice Flat Sum

The flat cubic hinge

A dihedral angle is the angle between two faces that share an edge. In a cube, every such angle is a right angle, 90 degrees. At any edge of the cubic lattice, four cubes meet, and their four right angles add to 360 degrees, a full turn. This is the flatness of the cubic lattice: no curvature accumulates along the edge. The declaration cubic_lattice_flatSum records exactly this fact as a theorem in the framework's machine-checked library of formal theorems.

The theorem states that the sum of the dihedral angles around a cubic lattice edge equals 2π. It is a direct consequence of the cube's right angle being π/2, established separately, and the arithmetic that four times π/2 is 2π. The proof is a simple computation. The library also derives that the deficit, defined as 2π minus the sum of angles, is zero at such a flat hinge. This matches the classical Regge calculus notion that zero deficit means zero curvature.

In Recognition Science, this theorem is part of a larger program. The framework models spacetime as a simplicial complex, a mesh of flat pieces, and uses dihedral angles to measure how the pieces fit together. The flat-sum condition is the piecewise-flat analog of saying a region has no curvature. This particular theorem verifies the baseline case for the cubic lattice, a necessary check before the framework can address more complex simplicial structures in its program to discharge the Regge deficit linearization hypothesis.

The theorem does not claim that the cubic lattice is the only flat structure, nor does it address curvature in curved spaces. It does not prove anything about the physical universe or about how the cubic lattice arises from recognition events. It is a statement about a specific geometric configuration, verified within the framework's formal system.

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

/-- 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 data of a dihedral angle: a cosine value in `[-1, 1]`. -/
structure DihedralAngleData where
  cosine : ℝ
  cosine_lb : -1 ≤ cosine
  cosine_ub : cosine ≤ 1

What this page does not claim

The theorem does not claim the cubic lattice is the only flat structure. It does not address curvature in non-flat or curved spaces. It does not make any claim about the physical universe or how the cubic lattice arises from recognition events.

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: