pith. sign in
module module high

IndisputableMonolith.Gravity.DiscreteCurvature

show as:
view Lean formalization →

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

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)