module module moderate

`IndisputableMonolith.Constants.CurvatureSpaceDerivation`

CurvatureSpaceDerivation module sets the configuration space dimension for the Recognition ledger as the effective dimension for curvature integration. Researchers deriving spatial dimensions via the RS forcing chain would cite its decomposition results. The module structures its content as definitions and lemmas that apply upstream results on the time quantum and cubic ledger geometry.

claim$\dim(\mathcal{C}) = 5$ for the configuration space of the Recognition ledger, which forces the spatial dimension $D = 3$ for curvature integration.

background

The module imports IndisputableMonolith.Constants, which defines the fundamental RS time quantum as $\tau_0 = 1$ tick, and IndisputableMonolith.Constants.AlphaDerivation. The latter states: "This module provides a complete, constructive derivation of the fine-structure constant $\alpha^{-1}$ from the geometry of the cubic ledger" with 4$\pi$ from Gauss-Bonnet via vertex deficits of $Q_3$.

It introduces the configuration space dimension as "the effective dimension for curvature integration" per its doc-comment. Sibling declarations establish config_space_is_5D, spatial_dims_eq_3, temporal_dim_forced, and balance_dim_forced.

The setting is the Recognition Science derivation of dimensions from the J-uniqueness fixed point and eight-tick octave in the forcing chain.

proof idea

This module contains no single proof but a collection of definitions and lemmas. It defines configSpaceDim, then proves the 5D decomposition and dimension forcing via conservation and balance using results imported from Constants and AlphaDerivation.

why it matters in Recognition Science

The module supplies the curvature space dimension that supports T8 in the UnifiedForcingChain, where the eight-tick octave forces $D = 3$ spatial dimensions. It provides the geometric setting for curvature integration in the ledger as part of the constants derivation.

scope and limits

Does not derive numerical values of constants.
Does not address the J-function or Recognition Composition Law.
Does not treat mass formulas or the phi-ladder.

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