BoundedFiniteQuotientPhaseVisibility
Bounded finite quotient phase visibility for a natural number n under a bounding function asserts existence of an admissible hard gate c at most the bound value that admits a nonempty subset-product phase hit. Researchers on integer ledger phase budgets cite this when invoking the visibility engine to bound unresolved phases. The declaration is a direct existential packaging of the witness condition drawn from budget and floor interfaces.
claimLet $n$ be a natural number and $b:ℕ→ℕ$ a bounding function. The bounded finite quotient phase visibility property holds precisely when there exists a natural number $c≤b(n)$ such that $c$ is an admissible hard gate and the subset-product phase hit set for $n$ and $c$ is nonempty.
background
The module develops bounded phase visibility for recovered integer ledgers that possess a stable unresolved-phase budget and whose failed gates obey a uniform KTheta floor. The actual floor statement is isolated as the KThetaFailureFloorHypothesis. Upstream, the eight-tick phase supplies the discrete angles $kπ/4$ for $k=0..7$, periodic with period $2π$. AdmissibleHardGate encodes the admissibility condition on hard gates drawn from the Erdos-Straus rotation hierarchy, while SubsetProductPhaseHit records the concrete phase hits realized by subset products under the phase-budget engine.
proof idea
The declaration is a direct definition that packages an existential witness: an admissible hard gate $c$ below the supplied bound together with a nonempty subset-product phase hit. No lemmas or tactics are invoked; the body simply assembles the three conjuncts (bound check, gate admissibility, nonempty hit) for consumption by the visibility engine.
why it matters in Recognition Science
This definition supplies the core property consumed by the bounded_phase_visibility theorem, which states that every non-identity reciprocal ledger satisfies the visibility bound under the engine. It fills the visibility-package slot in the number-theory development of phase budgets, linking the eight-tick phase structure to the KThetaFailureFloorHypothesis. The accompanying engine documentation notes that budget arithmetic bounds failed gates but does not construct the subset-product divisor, leaving explicit construction as an open interface.
scope and limits
- Does not prove existence of any admissible gate or phase hit for a concrete bound.
- Does not specify the functional form or growth rate of the bounding map.
- Does not address cases of persistent phase invisibility beyond the bound.
- Does not construct an explicit subset-product divisor from budget data alone.
formal statement (Lean)
39def BoundedFiniteQuotientPhaseVisibility (n : ℕ) (bound : ℕ → ℕ) : Prop :=
proof body
Definition body.
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. -/