gapMinusOne_at_D3
gapMinusOne at the forced dimension D equals 44. Researchers working on the integration gap in Recognition Science cite this to fix the numerical value of the gap minus one at three spatial dimensions. The proof is a direct native_decide evaluation of the arithmetic expression from the definition gapMinusOne d := integrationGap d - 1.
claimWhen the spatial dimension is $D = 3$, the quantity $D^2(D + 2) - 1$ equals 44.
background
The module defines the integration gap as the integer $D^2(D + 2)$, which equals 45 at D = 3. D is the spatial dimension fixed at 3 by the linking argument in Foundation.DimensionForcing. gapMinusOne is defined as integrationGap d minus 1, so the value at D = 3 is 44. The local setting also requires that gcd(2^D, D^2(D + 2)) = 1 precisely when D is odd, which holds at D = 3 and restricts dimensions among those consistent with non-trivial linking.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the arithmetic expression for gapMinusOne at D = 3 directly from its definition.
why it matters in Recognition Science
This result supplies the gap_minus_one field inside the IntegrationGapCert theorem, which bundles configuration dimension, parity count, gap value, and coprimality at D = 3. It supports the framework's selection of D = 3 among odd dimensions where the recognition period 2^D remains coprime to the gap. The placement aligns with T8 forcing of three spatial dimensions and the coprimality condition that keeps the recognition cycle orderly.
scope and limits
- Does not compute gapMinusOne for any dimension other than 3.
- Does not derive the integration gap formula from first principles.
- Does not connect the value 44 to any physical observable or constant.
- Does not address consciousness modeling interpretations noted in the module documentation.
formal statement (Lean)
96theorem gapMinusOne_at_D3 : gapMinusOne D = 44 := by native_decide
proof body
97