sync_resource_functional_minimized
plain-language theorem explainer
The theorem shows that the resource functional F(D) = α * syncPeriod(D) + β * D attains its minimum at D=3 for natural numbers D at least 3 whenever α is positive and β is nonnegative. Researchers citing the Recognition Science draft paper would use this to justify the dimensional choice in the synchronization model. The proof applies the synchronization selection principle to obtain monotonicity of syncPeriod, derives the companion inequality for the dimension term, multiplies each by the appropriate coefficient, and concludes with linarith.
Claim. Let $s(n)$ denote the synchronization period function. If $α > 0$, $β ≥ 0$, and $D ≥ 3$ is a natural number, then $α · s(3) + β · 3 ≤ α · s(D) + β · D$.
background
The module Papers.DraftV1 re-exports proved theorems under names matching statements in Draft_v1.tex, mapping them to existing repository results while using hypothesis interfaces for external mathematics such as Alexander duality. The resource functional is the linear combination α times the synchronization period at dimension D plus β times D, where the period function satisfies syncPeriod(3) = 360 in RS-native units and is nondecreasing for D ≥ 3 by the synchronization selection principle. Upstream results include the definition of syncPeriod as the lcm-based period and the Constraint inductive type from the SAT module, which supplies the algebraic setting for the minimization.
proof idea
The tactic proof first applies synchronization_selection_principle to obtain the natural-number inequality syncPeriod 3 ≤ syncPeriod D, then casts both this and the hypothesis 3 ≤ D to reals. It invokes mul_le_mul_of_nonneg_left twice, once for each term using the sign conditions on α and β. The resulting pair of inequalities is discharged by linarith.
why it matters
The result fills the algebraic core for the resource minimization step in Draft_v1.tex, supporting the framework's selection of D=3 as the spatial dimension (T8) via the eight-tick octave (T7). It relies on the synchronization selection principle and the RS-native syncPeriod definition to close the minimization claim for the functional appearing in the paper's Kepler non-precession section. No downstream uses are recorded yet, leaving its integration into larger cosmology or complexity arguments open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.