configDim_at_D3
plain-language theorem explainer
The declaration establishes that the configuration dimension evaluates to 5 when the spatial dimension is the forced value D = 3. Workers on the integration gap and related consciousness modeling cite this to anchor the D = 3 case in the framework. The proof reduces immediately to native_decide, which computes the result from the definition configDim d := d + 2.
Claim. For the forced spatial dimension $D = 3$, the configuration dimension satisfies $configDim(D) = 5$.
background
The module defines the integration gap as the integer $D^2(D+2)$, which at $D=3$ equals 45. D is the spatial dimension forced by linking in Foundation.DimensionForcing. The configuration dimension is defined locally as configDim d := d + 2, representing D spatial degrees of freedom plus one temporal and one ledger balance.
proof idea
This is a one-line wrapper that applies the native_decide tactic to evaluate the equality configDim D = 5 directly from the definition with D fixed at 3.
why it matters
This result supplies the config_dim field in the IntegrationGapCert theorem, which certifies the full integration gap structure at D = 3 including the gap value 45 and coprimality. It aligns with the framework's selection of D = 3 from the eight-tick octave and linking arguments. The parent theorem integrationGapCert uses this to establish the gap value 45 and coprimality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.