module module high

`IndisputableMonolith.Constants.CurvatureSpaceDerivation`

CurvatureSpaceDerivation module defines the configuration space dimension for the Recognition ledger as the effective dimension for curvature integration. Researchers deriving RS constants from ledger geometry would cite it to anchor spatial structure. The module organizes its case through imports from Constants and AlphaDerivation followed by a chain of sibling declarations on decomposition and dimensional forcing.

claimThe configuration space dimension for curvature integration satisfies $\dim(\mathcal{C}) = 5$, which forces spatial dimensions $D = 3$ and temporal dimension via the eight-tick structure.

background

The module sits inside the Constants domain. It imports the base Constants module defining the RS time quantum $\tau_0 = 1$ tick and the AlphaDerivation module, whose main result is the derivation of $\alpha^{-1}$ from cubic ledger geometry together with the structural extraction of $4\pi$ from Gauss-Bonnet on vertex deficits of $Q_3$.

Key objects introduced are configSpaceDim (effective dimension for curvature integration), ConfigSpaceDecomposition, and canonicalDecomposition. Sibling results then force config_space_is_5D, spatial_dims_eq_3, temporal_dim_forced via eight_tick_forces_temporal, and balance_dim_forced from conservation.

proof idea

This is a definition module, no proofs. The argument is organized as a sequence of declarations: first the dimensional objects and their decompositions, then the forcing theorems that extract five-dimensional configuration space, three spatial dimensions, and the temporal constraint from the imported time quantum and alpha geometry.

why it matters in Recognition Science

The module supplies the spatial configuration required for curvature integration and thereby supports the constant derivations that rest on ledger geometry. It realizes the T8 step of the forcing chain by establishing $D = 3$ and connects directly to the eight-tick octave. No downstream theorems are listed, yet it underpins the dimensional scaffolding used by the parent Constants module.

scope and limits

Does not compute explicit curvature integrals or numerical values.
Does not prove uniqueness of the five-dimensional choice.
Does not address mass formulas or phi-ladder rungs.
Does not extend to time evolution or dynamical equations.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (33)

def configSpaceDim L64
structure ConfigSpaceDecomposition L67
def canonicalDecomposition L74
theorem config_space_is_5D L77
def spatial_dims_forced L86
theorem spatial_dims_eq_3 L88
def temporal_dim_forced L95
theorem eight_tick_forces_temporal L98
def balance_dim_forced L106
theorem balance_from_conservation L109
def angular_contribution_per_dim L134
def total_angular_factor L137
theorem total_angular_is_pi5 L139
def seam_ratio L153
theorem seam_ratio_from_topology L155
def curvature_correction_derived L168
theorem curvature_correction_eq_formula L171
theorem curvature_matches_alpha_derivation L178
theorem pi3_incomplete L187
theorem pi4_incomplete L202
theorem pi6_excess L215
theorem pi_power_eq_pi5_iff L228
theorem curvature_power_family_eq_canonical_iff L244
theorem curvature_power_family_matches_derived_iff L271
theorem curvature_denominator_at_pi5_eq_canonical_iff L281
theorem curvature_numerator_at_pi5_eq_canonical_iff L318
theorem curvature_tuple_uniqueness_bundle L339
theorem curvature_tuple_uniqueness_bundle_vs_derived L352
theorem pi5_uniquely_forced L380
theorem curvature_term_complete_derivation L390
def dual_balance_codimension L417
theorem balance_constraint_codim_1 L419
theorem config_space_complete L423