IndisputableMonolith.NumberTheory.UniformFailureFloor

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Uniform Failure Floor
   7
   8Defines the RS floor scale used in the phase-budget engine:
   9
  10`KTheta = J(φ) / 45`.
  11
  12This file proves only positivity.  The claim that every failed finite phase
  13gate costs at least `KTheta` is kept as a separate explicit interface in
  14`BoundedPhaseVisibility`.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace NumberTheory
  19namespace UniformFailureFloor
  20
  21open Constants Cost
  22
  23/-- The RS phase-failure floor scale. -/
  24noncomputable def KTheta : ℝ := Jcost phi / 45
  25
  26theorem Jcost_phi_pos : 0 < Jcost phi :=
  27  Jcost_pos_of_ne_one phi phi_pos phi_ne_one
  28
  29theorem KTheta_pos : 0 < KTheta := by
  30  unfold KTheta
  31  exact div_pos Jcost_phi_pos (by norm_num : (0 : ℝ) < 45)
  32
  33theorem KTheta_nonneg : 0 ≤ KTheta := le_of_lt KTheta_pos
  34
  35end UniformFailureFloor
  36end NumberTheory
  37end IndisputableMonolith
  38