pith. machine review for the scientific record. sign in
theorem proved term proof

cost_spectrum_certificate

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 318theorem cost_spectrum_certificate :
 319    -- (1) Prime cost is strictly positive.
 320    (∀ {p : ℕ}, Nat.Prime p → 0 < primeCost p) ∧
 321    -- (2) Prime cost is strictly monotonic in p.
 322    (∀ {p q : ℕ}, Nat.Prime p → Nat.Prime q → p < q →
 323      primeCost p < primeCost q) ∧
 324    -- (3) Cost is zero exactly at n = 1 (within positive integers).
 325    (costSpectrumValue 1 = 0) ∧
 326    -- (4) Cost is positive for n ≥ 2.
 327    (∀ {n : ℕ}, 2 ≤ n → 0 < costSpectrumValue n) ∧
 328    -- (5) Cost is completely additive over positive integers.
 329    (∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 →
 330      costSpectrumValue (m * n) = costSpectrumValue m + costSpectrumValue n) ∧
 331    -- (6) Cost on a prime equals its prime cost.
 332    (∀ {p : ℕ}, Nat.Prime p → costSpectrumValue p = primeCost p) ∧
 333    -- (7) Cost on a power: c(n^k) = k · c(n).
 334    (∀ {n : ℕ} (_ : n ≠ 0) (k : ℕ),
 335      costSpectrumValue (n ^ k) = (k : ℝ) * costSpectrumValue n) ∧
 336    -- (8) Cost is bounded above by Ω(n) · J(n).
 337    (∀ {n : ℕ}, 2 ≤ n →
 338      costSpectrumValue n ≤ (Omega n : ℝ) * Jcost (n : ℝ)) :=

proof body

Term-mode proof.

 339  ⟨@primeCost_pos,
 340   @primeCost_strictMono,
 341   costSpectrumValue_one,
 342   @costSpectrumValue_pos,
 343   @costSpectrumValue_mul,
 344   @costSpectrumValue_prime,
 345   @costSpectrumValue_pow_general,
 346   @costSpectrumValue_le_omega_mul_jcost⟩
 347
 348end
 349
 350end PrimeCostSpectrum
 351end NumberTheory
 352end IndisputableMonolith

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.