IndisputableMonolith.NumberTheory.MinimalVisibilityEngine

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.VisibilityFromFloorBudget
   3import IndisputableMonolith.NumberTheory.PhaseBudgetEngineFromRS
   4
   5/-!
   6# Minimal Visibility Engine
   7
   8Repackages the bounded visibility engine without the visibility field.
   9That field is now a theorem (`hits_balanced_phase_of_floor_and_budget`), so
  10only the explicit RS-physical inputs (stable budget, uniform `KTheta` floor)
  11are required.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace NumberTheory
  16namespace MinimalVisibilityEngine
  17
  18open BoundedPhaseVisibility
  19open VisibilityFromFloorBudget
  20open PhaseBudgetEngineFromRS
  21open ErdosStrausRotationHierarchy
  22open SubsetProductPhase
  23open ErdosStrausBoxPhase
  24open T1PhaseBudgetBound
  25open scoped Classical
  26
  27/-- A minimal visibility engine carries only KTheta floor hypothesis and stable budget.  No
  28visibility field. -/
  29structure MinimalEngine where
  30  costOf : ℕ → ℕ → ℝ
  31  stable :
  32    ∀ n : ℕ, NonIdentityReciprocal n → StableIntegerLedgerBudget n (costOf n)
  33  floor :
  34    ∀ n : ℕ, NonIdentityReciprocal n → KThetaFailureFloorHypothesis n (costOf n)
  35
  36/-- A minimal engine yields a successful admissible gate for every
  37nonidentity reciprocal ledger. -/
  38theorem hits_admissible_gate (engine : MinimalEngine)
  39    {n : ℕ} (hn : NonIdentityReciprocal n) :
  40    ∃ c : ℕ, AdmissibleHardGate c ∧ HitsBalancedPhase n c :=
  41  hits_balanced_phase_of_floor_and_budget hn (engine.stable n hn) (engine.floor n hn)
  42
  43/-- A successful admissible gate gives a `SubsetProductPhaseHit` witness. -/
  44theorem subset_product_hit_of_minimal (engine : MinimalEngine)
  45    {n : ℕ} (hn : NonIdentityReciprocal n) :
  46    ∃ c : ℕ, AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c) := by
  47  classical
  48  rcases hits_admissible_gate engine hn with ⟨c, hc, hhit⟩
  49  exact ⟨c, hc, subsetProductPhaseHit_of_hitsBalancedPhase hhit⟩
  50
  51/-- A minimal visibility engine (KTheta floor hypothesis + stable budget) supplies the
  52`PhaseBudgetEngine` directly.  The bound field receives the gate witness
  53itself, so the membership check is satisfied by reflexivity. -/
  54noncomputable def phaseBudgetEngine (engine : MinimalEngine) :
  55    PhaseBudgetToErdosStraus.PhaseBudgetEngine where
  56  bound := fun n =>
  57    if h : ResidualTrap n then
  58      Classical.choose (subset_product_hit_of_minimal engine
  59        (nonIdentityReciprocal_of_residualTrap h))
  60    else 0
  61  supplies_hit := by
  62    intro n hntrap
  63    have hn : NonIdentityReciprocal n :=
  64      nonIdentityReciprocal_of_residualTrap hntrap
  65    have hex := subset_product_hit_of_minimal engine hn
  66    refine ⟨Classical.choose hex, ?_, ?_, ?_⟩
  67    · simp [hntrap]
  68    · exact (Classical.choose_spec hex).1
  69    · exact (Classical.choose_spec hex).2
  70
  71/-- Final closure: a minimal visibility engine solves the residual class. -/
  72theorem erdos_straus_residual_from_minimal_engine
  73    (engine : MinimalEngine)
  74    {n : ℕ} (hn : ResidualTrap n) :
  75    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  76  PhaseBudgetToErdosStraus.erdos_straus_residual_from_phaseBudget
  77    (phaseBudgetEngine engine) hn
  78
  79end MinimalVisibilityEngine
  80end NumberTheory
  81end IndisputableMonolith
  82