IndisputableMonolith.NumberTheory.EffectivePrimePhaseInput

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.SubsetProductPhase
   3import IndisputableMonolith.NumberTheory.PrimePhaseDistribution
   4
   5/-!
   6# Effective Prime Phase Input
   7
   8This module states the exact prime-distribution input needed for the residual
   9Erdős-Straus proof and proves that it implies `PrimePhaseBoxDistribution`.
  10
  11It deliberately avoids importing the currently bit-rotted
  12`PrimeDistributionBridge.lean`; that file is an upstream source candidate, not
  13a dependency of this interface.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace PrimePhaseInput
  19
  20open ErdosStrausRotationHierarchy
  21open ErdosStrausBoxPhase
  22open SubsetProductPhase
  23open PrimePhaseDistribution
  24
  25/-- Effective prime phase input: for every trapped ledger, bounded prime
  26phase supply produces an actual subset-product phase hit. -/
  27structure EffectivePrimePhaseInput where
  28  bound : ℕ → ℕ
  29  supplies_generators :
  30    ∀ n : ℕ, ResidualTrap n →
  31      ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c)
  32
  33/-- Effective prime phase supply gives the exact distribution statement
  34required by the residual Erdős-Straus chain. -/
  35def primePhaseBoxDistribution_of_effectivePrimePhaseInput
  36    (input : EffectivePrimePhaseInput) :
  37    PrimePhaseBoxDistribution where
  38  bound := input.bound
  39  hits := by
  40    intro n hn
  41    rcases input.supplies_generators n hn with ⟨c, hcbound, hc, ⟨hit⟩⟩
  42    exact ⟨c, hcbound, hc, generated_phase_hit_gives_HitsBalancedPhase hit⟩
  43
  44/-- Effective prime phase supply gives bounded balanced search. -/
  45def boundedBalancedSearch_of_effectivePrimePhaseInput
  46    (input : EffectivePrimePhaseInput) :
  47    BoundedBalancedSearchEngine :=
  48  boundedBalancedSearch_of_primePhaseBoxDistribution
  49    (primePhaseBoxDistribution_of_effectivePrimePhaseInput input)
  50
  51/-- Effective prime phase supply solves the residual trapped class. -/
  52theorem erdos_straus_residual_from_effectivePrimePhaseInput
  53    (input : EffectivePrimePhaseInput)
  54    {n : ℕ} (hn : ResidualTrap n) :
  55    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  56  erdos_straus_residual_from_prime_phase_box_distribution
  57    (primePhaseBoxDistribution_of_effectivePrimePhaseInput input) hn
  58
  59/-- The intended RS source theorem.  This is the final remaining input:
  60derive `EffectivePrimePhaseInput` from the RCL prime-ledger machinery. -/
  61structure RSPrimePhaseEquidistribution where
  62  effective_input : EffectivePrimePhaseInput
  63  /-- Marker: this theorem is meant to be sourced from RCL/J-cost prime-ledger
  64  phase distribution, not from finite search. -/
  65  from_rcl_prime_ledger : True
  66
  67def effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution
  68    (rs : RSPrimePhaseEquidistribution) :
  69    EffectivePrimePhaseInput :=
  70  rs.effective_input
  71
  72theorem erdos_straus_residual_from_rsPrimePhaseEquidistribution
  73    (rs : RSPrimePhaseEquidistribution)
  74    {n : ℕ} (hn : ResidualTrap n) :
  75    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  76  erdos_straus_residual_from_effectivePrimePhaseInput
  77    (effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution rs) hn
  78
  79end PrimePhaseInput
  80end NumberTheory
  81end IndisputableMonolith
  82