module module high

`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)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.LatticeRicci module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (17)

def cube_dihedral L56
def cubes_per_edge L59
def deficit_angle_flat L63
theorem flat_deficit_zero L65
def deficit_angle_deformed L75
theorem deficit_zero_when_flat L79
theorem deficit_scales_with_a_squared L83
def curvature_from_deficit L92
theorem curvature_equals_d2h L98
def linearized_ricci_from_deficits L113
theorem ricci_is_sum_of_curvatures L116
def vertex_deficit_cube L133
theorem vertex_deficit_value L135
theorem gauss_bonnet_cube L138
theorem euler_characteristic_from_deficit L143
structure DiscreteCurvatureCert L151
theorem discrete_curvature_cert L158