gapMinusOne_at_D3
plain-language theorem explainer
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.
Claim. When 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.