bounded_phase_visibility
plain-language theorem explainer
A bounded visibility engine proves that every non-identity reciprocal natural number n admits a phase-visible gate c below the engine's bound function, witnessed by an admissible hard gate and a nonempty subset-product phase hit. Number theorists modeling recognition costs via multiplicative recognizers would cite this to bound phase invisibility in finite quotients. The proof is a direct one-line application of the visibility field stored in the engine structure.
Claim. Let $E$ be a bounded visibility engine and let $n$ be a positive integer not equal to 1 that divides the square of some positive integer. Then there exists an integer $c$ with $c$ at most $E$.bound$(n)$ such that $c$ is an admissible hard gate and the set of subset-product phase hits for $n$ at $c$ is nonempty.
background
The module shows that a recovered integer ledger with a stable unresolved-phase budget and failed gates obeying a uniform KTheta floor cannot sustain finite phase invisibility past the supplied bound. The KThetaFailureFloorHypothesis is kept explicit as a named assumption. A BoundedVisibilityEngine packages a bound map from naturals to naturals, a cost map, a proof that every non-identity reciprocal ledger meets the stable integer ledger budget, the KTheta floor hypothesis for each such ledger, and the visibility witness itself. NonIdentityReciprocal n asserts positivity, inequality to 1, and the existence of N with n dividing N squared. BoundedFiniteQuotientPhaseVisibility n bound asserts existence of c at most bound n that is an admissible hard gate with nonempty SubsetProductPhaseHit n c. Upstream cost definitions from multiplicative recognizers and observer forcing supply the J-cost arithmetic underlying the budget interfaces.
proof idea
The proof is a term-mode one-liner that directly applies the visibility field of the supplied BoundedVisibilityEngine to the given n and the NonIdentityReciprocal hypothesis hn.
why it matters
This theorem supplies the concrete bounded visibility statement that the BoundedVisibilityEngine structure is designed to witness. It closes the argument that finite phase invisibility cannot persist beyond the supplied bound once the KTheta floor hypothesis and stable budget interfaces are granted. In the Recognition Science framework it connects the number-theoretic phase budget bounds to the broader forcing chain by ensuring that unresolved phases remain visible within explicit finite limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.