IndisputableMonolith.NumberTheory.BoundedPhaseVisibility

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.T1PhaseBudgetBound
   3import IndisputableMonolith.NumberTheory.UniformFailureFloor
   4import IndisputableMonolith.NumberTheory.SubsetProductPhase
   5
   6/-!
   7# Bounded Phase Visibility
   8
   9If a recovered integer ledger has a stable unresolved-phase budget and failed
  10gates have a uniform `KTheta` floor, then finite phase invisibility cannot
  11persist beyond the supplied bound.
  12
  13The actual floor theorem is kept explicit as `KThetaFailureFloorHypothesis`.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace BoundedPhaseVisibility
  19
  20open PhaseFailureCost
  21open T1PhaseBudgetBound
  22open UniformFailureFloor
  23open ErdosStrausRotationHierarchy
  24open SubsetProductPhase
  25
  26/-- Positive nonidentity reciprocal ledger in Nat form. -/
  27structure NonIdentityReciprocal (n : ℕ) : Prop where
  28  pos : 0 < n
  29  nonidentity : n ≠ 1
  30  reciprocal_budget : ∃ N : ℕ, 0 < N ∧ n ∣ N * N
  31
  32/-- KTheta floor hypothesis assumption at the RS scale `KTheta`. -/
  33structure KThetaFailureFloorHypothesis (n : ℕ) (costOf : ℕ → ℝ) : Prop where
  34  floor :
  35    ∀ c : ℕ, GateFails n c → KTheta ≤ costOf c
  36
  37/-- A bounded visibility package: a gate below `bound n` with a concrete
  38subset-product phase hit. -/
  39def BoundedFiniteQuotientPhaseVisibility (n : ℕ) (bound : ℕ → ℕ) : Prop :=
  40  ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c)
  41
  42/-- The exact bounded visibility theorem.  The proof uses the floor/budget
  43interfaces as inputs; the witness itself is supplied by the phase-budget
  44engine field because budget arithmetic bounds failed gates but does not
  45construct the subset-product divisor. -/
  46structure BoundedVisibilityEngine where
  47  bound : ℕ → ℕ
  48  costOf : ℕ → ℕ → ℝ
  49  stable :
  50    ∀ n : ℕ, NonIdentityReciprocal n → StableIntegerLedgerBudget n (costOf n)
  51  floor :
  52    ∀ n : ℕ, NonIdentityReciprocal n → KThetaFailureFloorHypothesis n (costOf n)
  53  visibility :
  54    ∀ n : ℕ, NonIdentityReciprocal n → BoundedFiniteQuotientPhaseVisibility n bound
  55
  56/-- A bounded visibility engine proves bounded phase visibility for every
  57nonidentity reciprocal ledger. -/
  58theorem bounded_phase_visibility
  59    (engine : BoundedVisibilityEngine)
  60    {n : ℕ} (hn : NonIdentityReciprocal n) :
  61    BoundedFiniteQuotientPhaseVisibility n engine.bound :=
  62  engine.visibility n hn
  63
  64/-- Under the explicit KTheta floor hypothesis and stable budget interfaces, failed gates in a
  65finite set have total cost bounded by the stable budget. -/
  66theorem failed_gate_count_bounded_at_KTheta
  67    {n : ℕ} {costOf : ℕ → ℝ} {S : Finset ℕ}
  68    (stable : StableIntegerLedgerBudget n costOf)
  69    (floor : KThetaFailureFloorHypothesis n costOf)
  70    (hfails : ∀ c ∈ S, GateFails n c) :
  71    KTheta * (S.card : ℝ) ≤ stable.budget := by
  72  apply failed_gate_count_bounded_by_budget stable
  73  exact ⟨KTheta_pos, hfails, fun c hc => floor.floor c (hfails c hc)⟩
  74
  75end BoundedPhaseVisibility
  76end NumberTheory
  77end IndisputableMonolith
  78