FiniteBoundedBalancedSearchCert
plain-language theorem explainer
The FiniteBoundedBalancedSearchCert structure packages a computable finite certificate for the Erdős-Straus problem inside the Recognition rotation hierarchy: every residual-trapped n up to maxN admits a gate c up to bound that meets both the admissible-hard-gate and balanced-pair-phase-support conditions. Number theorists working on finite verification of the conjecture would cite it as the honest computational form. The declaration is a direct structure definition with no internal proof steps or lemmas.
Claim. A finite bounded balanced search certificate consists of natural numbers $M$ and $B$ together with the assertion that for every $n$ with $n ≤ M$ and ResidualTrap$(n)$, there exists $c ≤ B$ such that AdmissibleHardGate$(c)$ and BalancedPairPhaseSupport$(n,c)$ hold. Here ResidualTrap$(n)$ requires $n > 1$, $n ≡ 1 mod 24$, and all prime factors of both $n$ and $(n+3)/4$ congruent to 1 mod 3; AdmissibleHardGate$(c)$ requires $c ≡ 3 mod 4$; BalancedPairPhaseSupport$(n,c)$ asserts positive integers $x,N,d,e$ satisfying $N = n·x$, $c = 4x - n$, $d·e = N^2$, and $c$ dividing both $N+d$ and $N+e$.
background
The Erdős-Straus Recognition Rotation Hierarchy module converts the RCL attack into a theorem-shaped proof skeleton. It establishes the finite and gate pieces while isolating two missing number-theoretic engines as explicit structure fields: prime phase separation across admissible residual quotients, and reciprocal pair closure once sufficient phase support appears. No new axioms are added; the missing engines remain open assumptions for future proofs.
proof idea
The declaration is a direct structure definition packaging the verified predicate. It invokes no lemmas or tactics beyond the module-local definitions of ResidualTrap, AdmissibleHardGate, and BalancedPairPhaseSupport.
why it matters
This definition supplies the precise finite certificate form that computation can certify inside the Erdős-Straus Recognition Rotation Hierarchy. It isolates the bounded check so the two missing engines can be stated as future hypotheses. The module doc-comment states that the construction turns the current RCL attack into a theorem-shaped proof skeleton without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.