module module moderate

`IndisputableMonolith.NumberTheory.ErdosStrausRotationHierarchy`

Erdős-Straus Rotation Hierarchy module supplies definitions for nonzero residuals and their phase quotients in the algebraic reduction of the conjecture. It extends the RCL ledger reduction by introducing finite modulus conditions and gate structures. Number theorists attacking the conjecture via combinatorial boxes would reference these objects. The module is built from a collection of definitions and supporting lemmas rather than a single theorem proof.

claimA nonzero residual $c/N$ has positive finite modulus $c$. The module defines residual phase quotients, admissible hard gates, gate ladders, balanced pair phase supports, and closure witnesses on the associated hierarchy.

background

This module operates in the NumberTheory subdomain and depends on the Erdős-Straus RCL module. The upstream doc-comment states: 'This file records the algebraic reduction behind the RCL attack on the Erdős-Straus conjecture. After choosing the first denominator x, the residual equation is c / N = 1 / y + 1 / z, with c = 4x - n and N = nx.' It introduces NonzeroResidual (positive finite c for nonzero c/N), ResidualPhaseQuotient, AdmissibleHardGate, gate_ladder_forced, GateClosureWitness, BalancedPairPhaseSupport, AllPrimeFactorsOneModThree, and ResidualTrap.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies foundational objects for the Erdős-Straus Box Phase module, whose doc-comment states it 'isolates the finite combinatorial part of the residual Erdős-Straus proof' via square budgets N^2 and complementary pairs (d,e) with d*e = N^2. It advances the RCL attack by providing rotation hierarchy tools that feed into box phase representations.

scope and limits

Does not prove the full Erdős-Straus conjecture.
Does not address zero-residual cases.
Does not extend the imported RCL algebraic reduction.
Does not supply numerical checks or explicit solutions.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.ErdosStrausRCL module_import

declarations in this module (23)

def NonzeroResidual L28
abbrev ResidualPhaseQuotient L32
theorem finite_quotient_necessity L35
def AdmissibleHardGate L45
theorem gate_ladder_forced L50
theorem admissible_gate_posts L59
def GateClosureWitness L70
theorem gate_closure_witness_gives_repr L83
def BalancedPairPhaseSupport L100
theorem balanced_pair_phase_support_gives_repr L111
def AllPrimeFactorsOneModThree L152
def ResidualTrap L158
def GateHasPhaseSupport L169
structure PrimePhaseEquidistributionEngine L174
structure BoundedSearchEngine L181
structure ReciprocalPairClosureEngine L189
structure BoundedBalancedSearchEngine L196
structure FiniteBoundedBalancedSearchCert L205
theorem finite_cert_of_global_engine L213
theorem residual_trap_solved L227
theorem bounded_search_implies_phase_equidistribution L236
theorem bounded_residual_trap_solved L245
theorem bounded_balanced_search_solved L254