sync_resource_functional_minimized
plain-language theorem explainer
The resource functional F(D) = α ⋅ ℓ(D) + β ⋅ D with α > 0, β ≥ 0 and ℓ(n) = lcm(2^n, 45) is minimized at D = 3 among natural numbers D ≥ 3. Draft paper authors cite it to justify the dimensional preference in the synchronization model. The proof applies the synchronization selection principle for monotonicity of ℓ, then uses monotonicity of multiplication by nonnegative scalars before a linear arithmetic step.
Claim. Let α > 0, β ≥ 0 and let D be a natural number with D ≥ 3. Then α ⋅ ℓ(3) + β ⋅ 3 ≤ α ⋅ ℓ(D) + β ⋅ D, where ℓ(n) := lcm(2^n, 45).
background
The Papers.DraftV1 module mirrors theorem statements from Draft_v1.tex, mapping them to available results in the Recognition Science repository while using hypothesis interfaces for external mathematics. The resource functional combines a synchronization cost α ⋅ ℓ(D) with a linear dimension penalty β ⋅ D. The synchronization selection principle supplies the monotonicity ℓ(3) ≤ ℓ(D) for D ≥ 3 that drives the comparison.
proof idea
The tactic proof first applies the synchronization selection principle to obtain ℓ(3) ≤ ℓ(D) as a natural-number inequality. It casts both this and 3 ≤ D to reals, applies mul_le_mul_of_nonneg_left to each weighted term using the sign hypotheses on α and β, then closes with linarith.
why it matters
The result supports the forcing-chain step T8 that selects D = 3 by exhibiting an explicit minimization of the resource functional at that value. It appears in the draft module to certify the algebraic core of the synchronization argument in Draft_v1.tex. No downstream uses are recorded, so the declaration functions as a terminal justification for the dimensional choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.