module module high

`IndisputableMonolith.Gravity.DiscreteCurvature`

DiscreteCurvature supplies the geometric primitives for lattice curvature in Recognition Science gravity by fixing the cube dihedral angle at π/2 and defining deficit angles that vanish on flat space. Lattice gravity researchers cite these objects when constructing discrete Ricci scalars from local geometry. The module delivers its content through direct definitions of dihedral and deficit quantities together with zero-argument lemmas establishing flat-space identities.

claim$\theta_{\rm cube}=\pi/2$, with deficit angle $\delta=\pi/2-\theta$ for a deformed cube and curvature extracted via $\kappa=\delta/a^2$ or summed vertex deficits.

background

The module belongs to the Gravity domain and imports Constants, where the RS time quantum satisfies $\tau_0=1$ tick. It introduces the cube dihedral angle fixed at $\pi/2$ (right angle) and deficit angles that quantify local deviation from flat geometry on a cubic lattice. These objects prepare the discrete setting for linearized curvature measures that later converge to continuum Ricci scalars.

proof idea

This is a definition module, no proofs. Sibling declarations supply direct definitions (cube_dihedral, deficit_angle_flat, curvature_from_deficit) and simple algebraic lemmas (flat_deficit_zero, deficit_zero_when_flat) that verify identities by substitution.

why it matters in Recognition Science

The deficit-angle machinery feeds the LatticeRicci module, which defines the lattice Ricci scalar from these deficits and proves convergence to the continuum Ricci scalar in the linearized weak-field regime. The downstream documentation identifies this as Step 4 of the lattice Ricci construction.

scope and limits

Does not treat non-cubic polyhedra or irregular lattices.
Does not address strong-field or nonlinear regimes.
Does not derive the continuum limit or global topology.

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