IndisputableMonolith.NumberTheory.ResidualGapHonest

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.NumberTheory.BoundedPhaseVisibility
   4
   5/-!
   6# Honest Residual Gap
   7
   8This module records the honest obstruction: the natural finite-phase mismatch
   9cost decreases with the gate size, so it cannot itself justify a uniform
  10`KTheta` floor.
  11
  12The missing theorem is therefore not an algebraic floor theorem, but a
  13prime/divisor distribution theorem strong enough to produce an actual phase
  14hit.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace NumberTheory
  19namespace ResidualGapHonest
  20
  21open Cost
  22open BoundedPhaseVisibility
  23
  24/-- Natural phase mismatch cost at one residue step for gate `c`.
  25We use `1 + 1/(c+1)` to keep the ratio positive and defined at `c=0`. -/
  26noncomputable def naturalPhaseFailureCost (c : ℕ) : ℝ :=
  27  Jcost (1 + (1 : ℝ) / (c + 1 : ℝ))
  28
  29theorem naturalPhaseFailureCost_pos (c : ℕ) :
  30    0 < naturalPhaseFailureCost c := by
  31  unfold naturalPhaseFailureCost
  32  have hden : (0 : ℝ) < (c + 1 : ℝ) := by positivity
  33  have hr : 0 < 1 + (1 : ℝ) / (c + 1 : ℝ) := by positivity
  34  have hne : 1 + (1 : ℝ) / (c + 1 : ℝ) ≠ 1 := by
  35    have hfrac : (0 : ℝ) < (1 : ℝ) / (c + 1 : ℝ) := by positivity
  36    linarith
  37  exact Jcost_pos_of_ne_one _ hr hne
  38
  39/-- A concrete value showing the natural phase cost is below a unit floor.
  40This already rules out deriving an arbitrary fixed floor from mere positivity
  41of the natural mismatch model. -/
  42theorem naturalPhaseFailureCost_two_below_one :
  43    naturalPhaseFailureCost 2 < 1 := by
  44  unfold naturalPhaseFailureCost
  45  norm_num [Jcost]
  46
  47/-- The final missing theorem, stated honestly.
  48
  49The phase-hit condition is the **two-sided** one: both `d` and the
  50complementary divisor `e = N^2 / d` must lie in residue `-N mod c`.
  51
  52The one-sided condition `d ≡ -N mod c` alone is **not** sufficient
  53unless `gcd(N, c) = 1`.  Counterexample at `n = 49`, `c = 7`,
  54`N = 686`: the divisor `d = 7^6 = 117649` divides `N^2` and satisfies
  55`d ≡ 0 ≡ -N mod 7`, but the complementary divisor
  56`e = N^2 / d = 4` satisfies `e ≡ 4 ≢ 0 mod 7`.
  57
  58Therefore the correct target is either:
  59
  60* the two-sided condition above, or
  61* the coprime condition `gcd(n, c) = 1`, which forces `gcd(N, c) = 1`
  62  and lets the complementary residue follow automatically from
  63  `d e = N^2` and `d ≡ -N mod c` via `e ≡ -N mod c`.
  64-/
  65structure DivisorCharacterSumBound : Prop where
  66  /-- The desired output: every residual trap has a bounded finite quotient
  67  with a square-budget phase hit (two-sided). -/
  68  supplies_visibility :
  69    ∀ n : ℕ, ErdosStrausRotationHierarchy.ResidualTrap n →
  70      ∃ c : ℕ, ErdosStrausRotationHierarchy.AdmissibleHardGate c ∧
  71        ErdosStrausBoxPhase.HitsBalancedPhase n c
  72
  73end ResidualGapHonest
  74end NumberTheory
  75end IndisputableMonolith
  76