synchronization_selection_principle
plain-language theorem explainer
The theorem establishes that the synchronization period, given by the least common multiple of 2 to the power D and 45, attains its minimum uniquely at dimension 3 for all dimensions at least 3. Authors of the Recognition Science draft paper cite this result when reducing the spatial dimension constraint to an arithmetic minimization condition. The tactic proof first reduces both sides to the explicit form 2^D times 45 using an auxiliary equality lemma, then applies additive decomposition of the dimension together with monotonicity of exponenti
Claim. For every natural number $D$ with $D$ at least 3, if $P(D)$ denotes the least common multiple of $2^D$ and 45, then $P(3)$ is at most $P(D)$ and equality holds only when $D$ equals 3.
background
The synchronization period is introduced in the RS native units module as the least common multiple of 8 and 45, which evaluates to 360; an auxiliary result extends the definition to arbitrary dimension by showing that the period equals 2 raised to D multiplied by 45. This declaration appears in the Draft V1 module, whose module documentation explains that it mirrors theorem statements from the accompanying LaTeX draft to keep the certified surface aligned with the paper. It depends on basic arithmetic properties such as associativity of addition in the LogicNat structure and the successor operation.
proof idea
The proof opens with the constructor tactic to handle the two conjuncts separately. In the first conjunct it invokes the closed-form lemma to replace both periods by their explicit expressions 2^3 times 45 and 2^D times 45. It then uses the existence lemma for additive decomposition to write D as 3 plus some k, proves the power inequality 2^3 less than or equal to 2 to the 3 plus k by scaling the trivial inequality 1 less than or equal to 2^k, and finally multiplies through by 45 while rearranging factors with commutativity and associativity. The second conjunct assumes equality and repeats the decomposition; for positive k it derives a strict power inequality, scales it by 45 to obtain a strict period inequality, and reaches a contradiction with the equality hypothesis.
why it matters
This theorem provides the key arithmetic fact underlying the synchronization minimization claim in the draft paper. It is applied in constraintS_forces_D3 to deduce that any dimension satisfying the S-constraint must equal 3, and in the resource-functional minimization theorem to bound the linear combination of period and dimension. Within the Recognition Science framework the result realizes the T7 eight-tick octave step, where the period 2^3 combines with the 45-tick gap to select D equals 3 as the unique minimizer of the synchronization resource. The statement is fully proved and introduces no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.