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