module module high

`IndisputableMonolith.NumberTheory.ErdosStrausRotationHierarchy`

The ErdosStrausRotationHierarchy module defines the rotation hierarchy for nonzero residuals in the Erdős-Straus RCL reduction. It introduces NonzeroResidual with positive finite modulus c together with ResidualPhaseQuotient, AdmissibleHardGate, and GateClosureWitness. Researchers attacking the conjecture via algebraic ledger reduction would cite it for the phase-support scaffolding. The module consists of definitions and lemmas that organize the finite combinatorial objects directly from the residual equation supplied by ErdosStrausRCL.

claimA nonzero residual satisfies $c/N = 1/y + 1/z$ where $c = 4x - n$, $N = nx$, and $c$ is a positive finite modulus. The rotation hierarchy is built from the residual phase quotient, admissible hard gates, gate-ladder forcing, and gate-closure witnesses that represent balanced-pair phase support.

background

This module belongs to the NumberTheory domain and imports ErdosStrausRCL. The upstream ledger reduction records that after the first denominator $x$ is chosen, the residual equation is $c/N = 1/y + 1/z$ with $c = 4x - n$ and $N = nx$. The module defines NonzeroResidual as a nonzero residual $c/N$ possessing a positive finite modulus $c$. It then introduces ResidualPhaseQuotient, finite_quotient_necessity, AdmissibleHardGate, gate_ladder_forced, admissible_gate_posts, GateClosureWitness, gate_closure_witness_gives_repr, BalancedPairPhaseSupport, and balanced_pair_phase_support_gives_repr to organize the rotation hierarchy.

proof idea

This is a definition module, no proofs. It structures the argument by successive definitions: NonzeroResidual supplies the positive finite modulus, finite_quotient_necessity forces the quotient, AdmissibleHardGate and gate_ladder_forced generate the admissible posts, GateClosureWitness and balanced_pair_phase_support_gives_repr close the representation, and AllPrimeFactorsOneModThree together with ResidualTrap complete the hierarchy.

why it matters in Recognition Science

The module feeds ErdosStrausBoxPhase, which isolates the finite combinatorial part of the residual Erdős-Straus proof by representing square-budget divisor-exponent boxes via complementary pairs $(d,e)$ with $d*e = N^2$. It supplies the rotation-hierarchy objects required for that box-phase construction and thereby advances the RCL attack on the conjecture.

scope and limits

Does not prove the Erdős-Straus conjecture itself.
Does not treat the zero-residual case.
Does not supply explicit solutions or numerical checks for concrete $n$.
Does not link to Recognition Science constants or forcing chain.

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