IndisputableMonolith.NumberTheory.VisibilityFromFloorBudget

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.BoundedPhaseVisibility
   3import IndisputableMonolith.NumberTheory.SubsetProductPhase
   4
   5/-!
   6# Visibility From Floor And Budget
   7
   8The breakthrough step.  Given an explicit stable budget plus a uniform
   9positive failure floor at `KTheta`, derive that some admissible gate must
  10succeed for every nonidentity reciprocal ledger.
  11
  12The argument is RS-physical: failed gates accumulate `KTheta` per gate; the
  13T1/RCL budget bounds the total; hence an admissible gate count larger than
  14`budget / KTheta` cannot all fail.
  15
  16This converts `BoundedVisibilityEngine.visibility` from an assumption into
  17a theorem, conditional only on the budget and floor.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace NumberTheory
  22namespace VisibilityFromFloorBudget
  23
  24open PhaseFailureCost
  25open T1PhaseBudgetBound
  26open UniformFailureFloor
  27open BoundedPhaseVisibility
  28open SubsetProductPhase
  29open ErdosStrausRotationHierarchy
  30open ErdosStrausBoxPhase
  31open scoped Classical
  32
  33/-- Admissible gates `c ≡ 3 mod 4` of the form `4 * i + 3` for `i < k`. -/
  34def admissibleGatesByIndex (k : ℕ) : Finset ℕ :=
  35  (Finset.range k).image (fun i => 4 * i + 3)
  36
  37theorem admissibleGatesByIndex_card (k : ℕ) :
  38    (admissibleGatesByIndex k).card = k := by
  39  unfold admissibleGatesByIndex
  40  rw [Finset.card_image_of_injective _ (fun i j hij => by
  41    have : 4 * i + 3 = 4 * j + 3 := hij
  42    omega)]
  43  exact Finset.card_range k
  44
  45theorem admissibleGatesByIndex_admissible {k : ℕ}
  46    {c : ℕ} (hc : c ∈ admissibleGatesByIndex k) :
  47    AdmissibleHardGate c := by
  48  unfold admissibleGatesByIndex at hc
  49  rw [Finset.mem_image] at hc
  50  obtain ⟨i, _, rfl⟩ := hc
  51  show (4 * i + 3) % 4 = 3
  52  omega
  53
  54/-- The breakthrough lemma.  From a stable budget and uniform `KTheta` floor,
  55some admissible gate fails to fail, i.e. `HitsBalancedPhase`. -/
  56theorem hits_balanced_phase_of_floor_and_budget
  57    {n : ℕ} (_hn : NonIdentityReciprocal n)
  58    {costOf : ℕ → ℝ}
  59    (stable : StableIntegerLedgerBudget n costOf)
  60    (floor : KThetaFailureFloorHypothesis n costOf) :
  61    ∃ c : ℕ, AdmissibleHardGate c ∧ HitsBalancedPhase n c := by
  62  classical
  63  -- Pick `k` so that `KTheta * k > budget`.
  64  obtain ⟨k, hk⟩ := exists_nat_gt (stable.budget / KTheta + 1)
  65  let S := admissibleGatesByIndex k
  66  -- Assume every admissible gate in S fails.
  67  by_contra hno
  68  push_neg at hno
  69  have hfails : ∀ c ∈ S, GateFails n c := by
  70    intro c hc
  71    exact hno c (admissibleGatesByIndex_admissible hc)
  72  have hlower :
  73      KTheta * (S.card : ℝ) ≤ cumulativeFailureCost n costOf S := by
  74    have := phase_failure_cost_lower_bound (n := n) (S := S)
  75      (costOf := costOf) (δ := KTheta)
  76      hfails (fun c hc => floor.floor c (hfails c hc))
  77    simpa [cumulativeFailureCost] using this
  78  have hupper := stable.bounds_all_finite_failures S
  79  have hbound : KTheta * (S.card : ℝ) ≤ stable.budget :=
  80    le_trans hlower hupper
  81  -- But `KTheta * k > budget`, so this is a contradiction.
  82  have hcard_eq : (S.card : ℝ) = (k : ℝ) := by
  83    rw [admissibleGatesByIndex_card]
  84  rw [hcard_eq] at hbound
  85  have hKTheta_pos : 0 < KTheta := KTheta_pos
  86  have hkpos : (0 : ℝ) < (k : ℝ) := by
  87    have hk_real : (k : ℝ) > stable.budget / KTheta + 1 := hk
  88    have hbnonneg : 0 ≤ stable.budget / KTheta := by
  89      apply div_nonneg stable.budget_nonneg KTheta_nonneg
  90    linarith
  91  -- KTheta * k > KTheta * (budget/KTheta + 1) = budget + KTheta > budget.
  92  have hbudget_div : KTheta * (stable.budget / KTheta) = stable.budget := by
  93    field_simp [ne_of_gt KTheta_pos]
  94  have hKk_gt : KTheta * (k : ℝ) > stable.budget := by
  95    have hmul : KTheta * (k : ℝ) > KTheta * (stable.budget / KTheta + 1) := by
  96      apply mul_lt_mul_of_pos_left hk hKTheta_pos
  97    have heq : KTheta * (stable.budget / KTheta + 1)
  98              = stable.budget + KTheta := by
  99      rw [mul_add, mul_one, hbudget_div]
 100    linarith
 101  linarith
 102
 103end VisibilityFromFloorBudget
 104end NumberTheory
 105end IndisputableMonolith
 106