gapMinusOne_factor
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the integration gap formula D^2(D+2).
- Does not prove coprimality with 2^D.
- Does not hold or apply for dimensions other than D=3.
- Does not connect the count to spectra, constants, or physical units.
formal statement (Lean)
98theorem gapMinusOne_factor : gapMinusOne D = 4 * 11 := by native_decide
proof body
Term-mode proof.
99
100/-! ## φ-power identity (matter-balance bridge) -/
101
102noncomputable section
103
104/-- The active edge count per fundamental tick. -/