gapMinusOne_factor
plain-language theorem explainer
The declaration establishes that the integration gap minus one equals 44 at the forced dimension D=3. A researcher closing the combinatorial structure of the recognition cycle would cite this when verifying the explicit count after the parity and configuration steps. The proof is a direct native computation of the integer expression.
Claim. For the forced spatial dimension $D=3$, the quantity $D^2(D+2)-1$ equals 44.
background
The integration gap is the integer $D^2(D+2)$, which equals 45 at D=3 and is termed the consciousness gap in companion modeling. gapMinusOne subtracts one from this value, yielding 44. D is the spatial dimension fixed to 3 by the linking argument in Foundation.DimensionForcing. The module records that gcd(2^D, D^2(D+2))=1 precisely when D is odd, restricting the dimension among odd candidates. Upstream constants supply the tick as the fundamental RS time quantum with one octave equal to eight ticks.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete integer expression for D=3.
why it matters
This equality supplies the explicit numerical value for the integration gap at the dimension selected by the forcing chain (T8). It supports the coprimality result that forces D odd and ultimately selects D=3 among consistent dimensions. The module doc states that the result combines with the linking argument in Foundation.DimensionForcing to restrict the dimension. No downstream uses are recorded, leaving the combinatorial closure open for later application in the recognition period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.