IndisputableMonolith.Gravity.DiscreteCurvature
DiscreteCurvature module defines deficit angles and curvature extraction on a cubic lattice for Recognition Science gravity. Lattice gravity researchers cite these primitives when building discrete Ricci scalars. The module consists of definitions and elementary lemmas with no complex proofs.
claimThe dihedral angle of a cube equals $pi/2$. Deficit angles vanish on flat lattices and scale as $a^2$ under deformation parameter $a$. Curvature equals the sum of deficit angles at each vertex.
background
Recognition Science discretizes gravity on a cubic lattice using the time quantum tau_0 = 1 tick imported from Constants. The module introduces the cube dihedral angle pi/2 and defines deficit angles for flat and deformed cases, along with curvature extracted from those deficits. It supplies the geometric building blocks referenced by the downstream LatticeRicci construction of the lattice Ricci scalar.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
Supplies the discrete curvature primitives that LatticeRicci uses to define the lattice Ricci scalar from deficit angles and prove convergence to the continuum Ricci scalar in the linearized regime. It fills the geometric foundation for Step 4 in the lattice gravity development.
scope and limits
- Does not derive Einstein equations on the lattice.
- Does not treat non-cubic lattices or higher-order terms.
- Does not include quantum corrections to curvature.
used by (1)
depends on (1)
declarations in this module (17)
-
def
cube_dihedral -
def
cubes_per_edge -
def
deficit_angle_flat -
theorem
flat_deficit_zero -
def
deficit_angle_deformed -
theorem
deficit_zero_when_flat -
theorem
deficit_scales_with_a_squared -
def
curvature_from_deficit -
theorem
curvature_equals_d2h -
def
linearized_ricci_from_deficits -
theorem
ricci_is_sum_of_curvatures -
def
vertex_deficit_cube -
theorem
vertex_deficit_value -
theorem
gauss_bonnet_cube -
theorem
euler_characteristic_from_deficit -
structure
DiscreteCurvatureCert -
theorem
discrete_curvature_cert