gapMinusOne
plain-language theorem explainer
Defines the integer D squared times (D plus 2) minus 1 for any natural number d. Researchers working on the Recognition Science integration gap at the forced dimension 3 cite this to obtain the value 44 that enters the phi-power balance. It is a one-line definition that subtracts 1 from the upstream integrationGap computation.
Claim. For a natural number $d$, $gapMinusOne(d) := d^2(d+2)-1$. At $d=3$ this equals 44.
background
The module establishes combinatorial facts about the integer $D^2(D+2)$, termed the integration gap. This quantity factors as the product of the parity count $D^2$ and the configuration dimension $D+2$. The upstream definition integrationGap $d$ computes parityCount $d$ times configDim $d$, which equals $d^2(d+2)$ for any natural $d$. D itself is the spatial dimension fixed at 3 by the linking argument in DimensionForcing. At this value the integration gap equals 45, so the present definition yields 44.
proof idea
One-line definition that subtracts 1 from the output of integrationGap $d$.
why it matters
This definition supplies the integer 44 required by the IntegrationGapCert structure for the phi-power balance identity phi^(A - gap) * phi^gap = phi at D=3. It is used directly in gapMinusOne_at_D3 and gapMinusOne_factor to establish the numerical value and its factorization 4*11. In the Recognition framework this closes the gap between the integration gap of 45 and the exponent -44 in the matter-balance bridge, consistent with the eight-tick octave and phi-ladder mass scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.