NonIdentityReciprocal

formal source

  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. -/