cubes_per_edge
plain-language theorem explainer
In the cubic lattice Z^3 exactly four cubes meet at each edge. This supplies the multiplicity for deficit-angle sums in flat discrete geometries and is cited in Regge-calculus derivations of zero curvature. The definition is a direct constant assignment of the natural number 4 with no lemmas or computation.
Claim. In the integer lattice $Z^3$, the number of unit cubes incident to each edge is $4$.
background
The module formalizes Regge-style discrete curvature on lattices. On a flat Z^3 lattice each cube has right dihedral angles of pi/2; the deficit at an edge is 2 pi minus the sum of those angles. Upstream DihedralAngle.deficit computes 2 pi minus sum of thetas for a list of dihedral data, while Schlaefli.deficit applies the same to a simplicial hinge. The local setting is the connection between lattice strain (encoded by J-cost of ledger entries) and curvature concentrated on edges, with the flat case serving as the zero-curvature baseline.
proof idea
Direct constant definition. It assigns the integer 4 with no tactics, lemmas, or reduction steps.
why it matters
This supplies the geometric multiplicity required by deficit_angle_flat (which computes 2 pi minus cubes_per_edge times cube_dihedral) and by the theorem flat_deficit_zero that proves the result is zero. It anchors the Regge action to the Einstein-Hilbert limit in the undeformed case, consistent with the framework's forcing of D equals 3 spatial dimensions and the eight-tick octave. The definition closes the flat-lattice case before metric perturbations are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.