deficit_angle_flat
plain-language theorem explainer
The definition sets the deficit angle for an edge in a flat cubic lattice to 2π minus four times the cube dihedral angle. Researchers in Regge calculus and discrete gravity cite it as the zero-curvature reference case on Z^3. It is realized as a direct arithmetic expression using the lattice coordination number 4 and the right dihedral angle π/2.
Claim. The deficit angle at an edge of the flat cubic lattice is $2π - 4 · (π/2)$.
background
In the DiscreteCurvature module the deficit angle at an edge is δ_e = 2π minus the sum of dihedral angles around that edge. On the flat lattice Z^3 exactly four cubes meet at each edge and each contributes the right dihedral angle π/2, so the sum exactly equals 2π. The upstream constants establish cube_dihedral as π/2 and cubes_per_edge as 4. The module follows Regge calculus, concentrating curvature on edges via these deficits, and treats the flat case as the baseline before metric perturbations deform the angles.
proof idea
The definition is a one-line arithmetic expression that subtracts the product of cubes_per_edge and cube_dihedral from 2π. No additional lemmas or tactics are required beyond the constant definitions of those two quantities.
why it matters
This definition supplies the flat_zero field inside the DiscreteCurvatureCert structure, which also records the Gauss-Bonnet relation 8 · vertex_deficit_cube = 4π and the Euler characteristic 2 for S^2. It anchors the Regge-style discretization of curvature before deformations are introduced, providing the zero reference that later theorems use to show deficits proportional to second derivatives of the metric perturbation. The construction supports the quadratic limit in which J-cost strain recovers sectional curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.