GateHasPhaseSupport

formal source

 166/-- A gate has enough phase support if its finite quotient sees a
 167non-identity phase in the divisor ledger.  This is intentionally abstract:
 168the next proof must instantiate it from prime phase distribution. -/
 169def GateHasPhaseSupport (n c : ℕ) : Prop :=
 170  ∃ _ : ResidualPhaseQuotient c, n = n
 171
 172/-- Prime phase equidistribution: trapped ledgers are eventually separated
 173by an admissible finite quotient. -/
 174structure PrimePhaseEquidistributionEngine : Prop where
 175  phase_support :
 176    ∀ n : ℕ, ResidualTrap n →
 177      ∃ c : ℕ, AdmissibleHardGate c ∧ GateHasPhaseSupport n c
 178
 179/-- Effective bounded search: the separating gate can be chosen below a
 180specific bound. -/
 181structure BoundedSearchEngine : Type where
 182  bound : ℕ → ℕ
 183  bound_ok :
 184    ∀ n : ℕ, ResidualTrap n →
 185      ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ GateHasPhaseSupport n c
 186
 187/-- Reciprocal pair closure: once a gate has enough phase support, it yields
 188the actual reciprocal divisor-pair witness required by RCL. -/
 189structure ReciprocalPairClosureEngine : Prop where
 190  close :
 191    ∀ n c : ℕ, ResidualTrap n → AdmissibleHardGate c → GateHasPhaseSupport n c →
 192      GateClosureWitness n c
 193
 194/-- Stronger, fully arithmetic bounded search: the search returns the actual
 195balanced phase pair, not merely abstract phase support. -/
 196structure BoundedBalancedSearchEngine : Type where
 197  bound : ℕ → ℕ
 198  bound_ok :
 199    ∀ n : ℕ, ResidualTrap n →