Cost Calibration Boundary Continuous Extension Log Line Gap Least Constant

The least gap constant

In mathematics, a continuous extension takes a function defined on a sparse set, such as the prime numbers, and fills in the gaps so that the result is continuous on the whole real line. The question is how much the values at the primes can move when you perturb the function slightly at the point 2. The Recognition Science framework's machine-checked library of formal theorems proves an exact answer: the least constant that works is 1.

Formally, the theorem states that for any real K, the following are equivalent: for any two positive continuous extensions α and β of prime-weight functions, if their values at 2 differ by at most ε, then for every prime p, the difference |α(p) − β(p)| is bounded by (K·ε / log 2)·log(p). This holds for all ε ≥ 0 exactly when K ≥ 1. In other words, the bound with K = 1 is the tightest possible; any smaller constant fails for some pair of extensions.

The constant 1 is not arbitrary. It emerges from the logarithmic scaling of the bound: the factor 1/log 2 normalizes the gap at the prime 2, and the growth with log(p) matches the natural spacing of primes. The theorem pins down this least constant as a structural fact about continuous extensions, not a fitted parameter.

In Recognition Science, this result belongs to the calibration boundary: the boundary between admissible and inadmissible cost functions. The theorem does not itself derive any physical constant or prove any property of the cost function J. It establishes a precise analytic fact about how continuous extensions behave near the prime weights, which the framework uses as a technical lemma in its broader forcing chain.

What the theorem does not claim: it does not say that any particular physical quantity equals 1, nor does it assert that the bound is sharp for every pair of extensions. It only says that K = 1 is the least constant that makes the bound hold universally. The theorem also does not address extensions that are not positive or not continuous; those cases lie outside its scope.

theorem continuousExtension_logLine_primeWeight_gap_least_constant
    (K : ℝ) :
    (∀ (α β : RealPrimeWeights) (eps : ℝ),
        0 ≤ eps →
        ContinuousRCLPositiveExtension α →
        ContinuousRCLPositiveExtension β →
        |α 2 - β 2| ≤ eps →
        ∀ p : ℕ, Nat.Prime p →
          |α p - β p| ≤ (K * eps / Real.log 2) * Real.log (p : ℝ))
      ↔
    (1 : ℝ) ≤ K := by
  constructor
  · intro hbound
    have hlog2pos : 0 < Real.log (2 : ℝ) := Real.log_pos (by norm_num)
    let α : RealPrimeWeights := fun _ => 0
    let β : RealPrimeWeights := fun p => Real.log (p : ℝ)
    let eps : ℝ := Real.log (2 : ℝ)
    have heps : 0 ≤ eps := le_of_lt hlog2pos
    have hα : ContinuousRCLPositiveExtension α :=
      (continuousExtension_iff_weightsOnLogLine α).mpr ⟨0, by
        intro p hp
        simp [α]⟩
    have hβ : ContinuousRCLPositiveExtension β :=
      (continuousExtension_iff_weightsOnLogLine β).mpr ⟨1, by
        intro p hp
        simp [β]⟩
    have hcal : |α 2 - β 2| ≤ eps := by
      simp [α, β, eps, abs_of_pos hlog2pos]
    have hle := hbound α β eps heps hα hβ hcal 2 Nat.prime_two
    have hleft : |α 2 - β 2| = Real.log (2 : ℝ) := by
      simp [α, β, abs_of_pos hlog2pos]
    have hright :
        (K * eps / Real.log (2 : ℝ)) * Real.log (2 : ℝ) =
          K * Real.log (2 : ℝ) := by
      have hcancel :
          (K * eps / Real.log (2 : ℝ)) * Real.log (2 : ℝ) = K * eps :=
        div_mul_cancel₀ (K * eps) (ne_of_gt hlog2pos)
      simpa [eps] using hcancel
    have : Real.log (2 : ℝ) ≤ K * Real.log (2 : ℝ) := by
      simpa [hleft, hright] using hle
    exact (le_mul_iff_one_le_left hlog2pos).mp this
  · intro hK α β eps heps hα hβ hcal p hp
    have hparent :=
      continuousExtension_logLine_primeWeight_gap α β eps heps hα hβ hcal p hp
    have hlog2pos : 0 < Real.log (2 : ℝ) := Real.log_pos (by norm_num)
    have hplog : 0 < Real.log (p : ℝ) :=
      Real.log_pos (Nat.one_lt_cast.mpr hp.one_lt)
    have hscale :
        (eps / Real.log (2 : ℝ)) * Real.log (p : ℝ) ≤
          (K * eps / Real.log (2 : ℝ)) * Real.log (p : ℝ) := by
      have hnonneg : 0 ≤ eps / Real.log (2 : ℝ) :=
        div_nonneg heps (le_of_lt hlog2pos)
      have hgain :
          eps / Real.log (2 : ℝ) ≤ K * (eps / Real.log (2 : ℝ)) := by
        calc
          eps / Real.log (2 : ℝ)
              = (1 : ℝ) * (eps / Real.log (2 : ℝ)) := (one_mul _).symm
          _ ≤ K * (eps / Real.log (2 : ℝ)) :=
            mul_le_mul_of_nonneg_right hK hnonneg
      have hrew :
          K * (eps / Real.log (2 : ℝ)) = K * eps / Real.log (2 : ℝ) := by
        ring
      rw [← hrew]
      exact mul_le_mul_of_nonneg_right hgain (le_of_lt hplog)
    exact hparent.trans hscale

What this page does not claim

This theorem does not derive any physical constant such as the fine-structure constant. It does not prove that the bound is sharp for any particular pair of extensions. It does not address extensions that are not positive or not continuous.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/CalibrationBoundary/ContinuousExtensionLogLineGapLeastConstant.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: