constraintS
constraintS packages the verified certificate for constraint (S) asserting that D=3 uniquely minimizes the synchronization period lcm(2^D, T(D^2)) among odd dimensions D >= 3. Researchers modeling dimensional rigidity cite this certificate when grounding the selection of the 45-unit phase. The definition is a structure constructor that assembles pre-verified numerical facts via native_decide together with direct references to coprimality and monotonicity lemmas.
claimLet ConstraintS_Cert be the structure with fields phasePeriod(3) = 45, syncPeriod(3) = 360, Nat.Coprime(8, phasePeriod(3)), failure of coprimality for even D in {2,4,6,8,10}, strict inequality syncPeriod(3) < syncPeriod(D) for odd D with 3 <= D <= 11 and D != 3, and the chain of strict inequalities syncPeriod(3) < syncPeriod(5) < syncPeriod(7) < syncPeriod(9) < syncPeriod(11).
background
The module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D >= 3, D=3 uniquely minimizes the synchronization period lcm(2^D, T(D^2)). Here phasePeriod(D) denotes the triangular number T(D^2) and syncPeriod(D) denotes lcm(2^D, phasePeriod(D)). The eight-tick octave of the forcing chain supplies the factor 2^D while the parity matrix of the D-dimensional hypercube supplies the D^2 entries whose cumulative phase is T(D^2).
proof idea
The definition constructs the ConstraintS_Cert record by assigning phase_at_D3 and sync_at_D3 via native_decide, coprime_at_D3 via native_decide, even_D_fails to the theorem even_D_not_coprime, D3_minimizes to D3_unique_minimizer, and monotone_odd to sync_strictly_increasing_odd.
why it matters in Recognition Science
This supplies the concrete certificate for constraint (S) that selects the 45-unit phase at D=3, confirming the minimal synchronization cost among odd dimensions. It directly supports the eight-tick octave (period 2^3) and the forcing of D=3 in the unified chain T0-T8. The certificate grounds the dimensional selection used in downstream Recognition Science arguments for the alpha band and mass ladder.
scope and limits
- Does not prove minimization for odd D > 11.
- Does not derive the definitions of phasePeriod or syncPeriod.
- Does not address coprimality for even D outside the finite set {2,4,6,8,10}.
- Does not supply a general analytic proof independent of native_decide.
formal statement (Lean)
170def constraintS : ConstraintS_Cert where
171 phase_at_D3 := by native_decide
proof body
Definition body.
172 sync_at_D3 := by native_decide
173 coprime_at_D3 := by native_decide
174 even_D_fails := even_D_not_coprime
175 D3_minimizes := D3_unique_minimizer
176 monotone_odd := sync_strictly_increasing_odd
177
178end SyncMinimization
179end Gap45
180end IndisputableMonolith