IndisputableMonolith.Verification.PhiPinnedCert

   1import IndisputableMonolith.RecogSpec.PhiSelectionCore
   2import IndisputableMonolith.PhiSupport.Lemmas
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6namespace PhiPinned
   7
   8/-- Certificate: the RS φ-selection predicate pins a unique real φ. -/
   9structure PhiPinnedCert where
  10  deriving Repr
  11
  12@[simp] def PhiPinnedCert.verified (_c : PhiPinnedCert) : Prop :=
  13  ∃! φ : ℝ, IndisputableMonolith.RecogSpec.PhiSelection φ
  14
  15@[simp] theorem PhiPinnedCert.verified_any (c : PhiPinnedCert) :
  16    PhiPinnedCert.verified c := by
  17  refine ⟨IndisputableMonolith.Constants.phi, ?_, ?_⟩
  18  · -- PhiSelection for Constants.phi
  19    constructor
  20    · simpa using IndisputableMonolith.PhiSupport.phi_squared
  21    · exact lt_trans (by norm_num : (0 : ℝ) < 1) IndisputableMonolith.PhiSupport.one_lt_phi
  22  · intro x hx
  23    exact (IndisputableMonolith.PhiSupport.phi_unique_pos_root x).mp hx
  24
  25end PhiPinned
  26end Verification
  27end IndisputableMonolith
  28