`bounded_phase_visibility`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.BoundedPhaseVisibility
domain: NumberTheory
line: 58 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.BoundedPhaseVisibility on GitHub at line 58.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.