PrimePhaseEquidistributionEngine
plain-language theorem explainer
Prime phase equidistribution asserts that every residual trap n (n > 1, n ≡ 1 mod 24, all prime factors ≡ 1 mod 3) admits an admissible gate c ≡ 3 mod 4 whose finite quotient exhibits non-identity phase support. Number theorists closing the Erdős-Straus conjecture via the Recognition rotation hierarchy would cite this structure when separating trapped ledgers. The declaration is a bare structure definition packaging the universal quantification as an explicit assumption.
Claim. An engine for prime phase equidistribution is the proposition that for all natural numbers $n$, if $n$ is a residual trap (i.e., $n > 1$, $n ≡ 1 mod 24$, and all prime factors of $n$ and $(n+3)/4$ are ≡ 1 mod 3), then there exists $c ∈ ℕ$ with $c ≡ 3 mod 4$ such that the gate for $n$ and $c$ has phase support (a non-identity phase in the residual quotient).
background
In the Erdős-Straus Recognition Rotation Hierarchy module the current RCL attack is turned into a theorem-shaped proof skeleton. The module isolates two missing number-theoretic engines as structure fields: prime phase separation across admissible residual quotients and reciprocal pair closure once enough phase support appears. No new axiom is introduced; the missing engines are explicit assumptions that a future proof must supply.
proof idea
The declaration is a structure definition with no proof body. It packages the phase support property directly as the single field of the structure.
why it matters
This structure supplies the prime phase separation engine required by the rotation hierarchy. It is used by the theorem showing that a bounded search engine implies phase equidistribution and by the theorem that rotation separation plus reciprocal closure solves the residual class, yielding a rational Erdős-Straus representation. In the Recognition framework it fills the gap between the explicit formulas and full conjecture resolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.