module module high

`IndisputableMonolith.Gravity.DiscreteCurvature`

This module supplies the discrete geometry primitives for curvature on a cubic lattice in Recognition Science gravity. It fixes the cube dihedral angle at pi over 2 and defines deficit angles together with their scaling under deformation. Lattice gravity researchers cite these definitions when assembling the Ricci scalar in the LatticeRicci module. The module consists entirely of definitions and elementary lemmas that establish zero deficit in the flat case and quadratic scaling with deformation amplitude.

claimThe dihedral angle of a cube satisfies $θ = π/2$. The flat deficit angle vanishes identically. For a deformed lattice the deficit angle $δ$ scales as $a^2$ where $a$ is the deformation parameter; the discrete curvature is recovered from the deficit via $κ = δ / A$ with $A$ the local area element.

background

In Recognition Science the gravitational sector is discretized on a cubic lattice whose edges are measured in the fundamental time quantum τ₀ = 1 tick supplied by the Constants module. The dihedral angle between adjacent faces of each cube is fixed at π/2 in the flat metric. Deficit angles quantify the angular defect at vertices when the lattice is deformed, furnishing a discrete proxy for sectional curvature.

proof idea

This is a definition module, no proofs. It introduces the named constants cube_dihedral, cubes_per_edge and the functions deficit_angle_flat, deficit_angle_deformed, curvature_from_deficit together with their immediate algebraic properties.

why it matters in Recognition Science

These definitions are imported by the LatticeRicci module, which assembles them into the lattice Ricci scalar and proves convergence to the continuum Ricci scalar in the linearized weak-field regime. The module thereby supplies the discrete geometric foundation for the gravity sector, consistent with the spatial dimension D = 3 fixed by the forcing chain.

scope and limits

Does not treat non-cubic or irregular lattices.
Does not include time-dependent or dynamical curvature.
Does not compute numerical values for physical constants.
Does not address higher-order curvature corrections.

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