deficit_angle_flat
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute deficit angles on deformed lattices.
- Does not derive proportionality to second derivatives of the metric perturbation.
- Does not evaluate the Regge action or its continuum limit.
- Does not invoke J-cost, phi-ladder, or Recognition Composition Law.
Lean usage
theorem flat_deficit_zero : deficit_angle_flat = 0 := by unfold deficit_angle_flat cubes_per_edge cube_dihedral; simp; ringformal statement (Lean)
63noncomputable def deficit_angle_flat : ℝ := 2 * Real.pi - cubes_per_edge * cube_dihedral
proof body
Definition body.
64