finite_cert_of_global_engine
plain-language theorem explainer
A bounded balanced search engine for residual traps supplies a uniform natural-number bound B such that every trapped n up to any prescribed maxN admits an admissible gate c ≤ B together with balanced pair phase support. Number theorists formalizing finite certificates for the Erdős-Straus conjecture would cite the result when reducing an assumed global engine to a computable check. The argument extracts the supremum of the engine's per-instance bounds over the finite interval and lifts the local witness via transitivity of ≤.
Claim. Let E be a bounded balanced search engine. For every natural number M there exists a natural number B such that, for all n ≤ M, if n is a residual trap then there exists c ≤ B with c ≡ 3 (mod 4) and (n, c) admitting balanced pair phase support.
background
The module develops a rotation hierarchy for the Erdős-Straus conjecture inside Recognition Science. A residual trap is an integer n > 1 with n ≡ 1 (mod 24) whose prime factors lie in the class 1 (mod 3), together with the same property for (n + 3)/4. An admissible hard gate is any c ≡ 3 (mod 4). Balanced pair phase support for n and c is the existence of x, N, d, e satisfying N = n x, c = 4x − n, d e = N², and c dividing both N + d and N + e.
proof idea
The term proof works classically. It defines B as the supremum of engine.bound over the finite set {0, …, maxN}. For any qualifying n the engine's bound_ok supplies a witness c together with the gate and support properties. The inequality c ≤ B is obtained by applying le_trans to the local bound and the fact that every local bound is ≤ the supremum of the range.
why it matters
The declaration closes the finite-range certificate piece of the Erdős-Straus rotation hierarchy. It shows that any global engine immediately yields a uniform bound for all trapped n up to maxN, thereby isolating the two missing engines (prime phase separation and reciprocal pair closure) as explicit structure fields. The result sits inside the module's RCL-based attack without new axioms and supplies the finite/gate skeleton referenced in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.