IndisputableMonolith.NumberTheory.PrimePhaseDistribution

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase
   3import IndisputableMonolith.NumberTheory.PrimeCostSpectrum
   4
   5/-!
   6# Prime Phase Distribution Interface for Erdős-Straus
   7
   8The RCL algebra and finite square-budget closure are now theorem-grade.  The
   9global remaining step is a prime phase distribution theorem strong enough to
  10hit the required square-budget phase.
  11
  12This module names that distribution statement exactly and proves that it
  13instantiates the existing `BoundedBalancedSearchEngine`.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace PrimePhaseDistribution
  19
  20open ErdosStrausRotationHierarchy
  21open ErdosStrausBoxPhase
  22
  23/-- Prime phase distribution over square-budget divisor boxes.
  24
  25For every residual trapped `n`, a bounded admissible gate `c` has a divisor
  26box point hitting the required balanced phase. -/
  27structure PrimePhaseBoxDistribution where
  28  bound : ℕ → ℕ
  29  hits :
  30    ∀ n : ℕ, ResidualTrap n →
  31      ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ HitsBalancedPhase n c
  32
  33/-- The exact finite-combinatorial conversion:
  34prime phase box distribution gives the bounded balanced search engine. -/
  35def boundedBalancedSearch_of_primePhaseBoxDistribution
  36    (dist : PrimePhaseBoxDistribution) :
  37    BoundedBalancedSearchEngine where
  38  bound := dist.bound
  39  bound_ok := by
  40    intro n hn
  41    rcases dist.hits n hn with ⟨c, hcbound, hc, hhit⟩
  42    exact ⟨c, hcbound, hc, box_phase_hit_gives_balanced_pair hhit⟩
  43
  44/-- If the prime phase box distribution theorem is supplied, the residual
  45Erdős-Straus class follows. -/
  46theorem erdos_straus_residual_from_prime_phase_box_distribution
  47    (dist : PrimePhaseBoxDistribution)
  48    {n : ℕ} (hn : ResidualTrap n) :
  49    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  50  bounded_balanced_search_solved
  51    (boundedBalancedSearch_of_primePhaseBoxDistribution dist) hn
  52
  53/-! ## Existing RS prime-distribution surface
  54
  55The imported prime modules currently provide:
  56
  57* prime ledger cost additivity (`PrimeCostSpectrum`);
  58* an RH/frustration-spectrum bridge to aggregate prime distribution
  59  (`PrimeDistributionBridge`, currently an upstream repair target under
  60  the active Lean toolchain).
  61
  62They do not yet prove the square-budget residue-box hit required above.
  63The following structure records the exact extra theorem needed from the
  64RS prime-distribution program. -/
  65
  66/-- The missing first-principles bridge from the RS prime ledger to
  67Erdős-Straus square-budget phase hits. -/
  68structure RSPrimePhaseBoxTheorem : Type where
  69  distribution : PrimePhaseBoxDistribution
  70  /-- Marker that the theorem is intended to be derived from RCL/J-cost prime
  71  ledger machinery rather than inserted as an arithmetic oracle. -/
  72  from_rcl_prime_ledger : True
  73
  74/-- Once the RS prime phase box theorem is derived, it supplies the desired
  75bounded balanced search engine. -/
  76def boundedBalancedSearch_of_rsPrimePhaseBoxTheorem
  77    (rs : RSPrimePhaseBoxTheorem) :
  78    BoundedBalancedSearchEngine :=
  79  boundedBalancedSearch_of_primePhaseBoxDistribution rs.distribution
  80
  81/-- Final conditional form, with the remaining theorem named explicitly. -/
  82theorem erdos_straus_residual_from_rs_prime_phase_box
  83    (rs : RSPrimePhaseBoxTheorem)
  84    {n : ℕ} (hn : ResidualTrap n) :
  85    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  86  bounded_balanced_search_solved
  87    (boundedBalancedSearch_of_rsPrimePhaseBoxTheorem rs) hn
  88
  89end PrimePhaseDistribution
  90end NumberTheory
  91end IndisputableMonolith
  92