erdos_straus_residual_from_effectivePrimePhaseInput
plain-language theorem explainer
Effective prime phase input guarantees that every residual trap n admits a rational Erdős-Straus representation. Number theorists extending the Recognition Science treatment of the Erdős-Straus conjecture cite this as the bridge from bounded prime phase supply to the representation property. The proof is a one-line wrapper that extracts the prime phase box distribution from the input and applies the distribution-to-representation theorem.
Claim. Let $I$ be an effective prime phase input. For any natural number $n$ that is a residual trap, the rational number $n$ admits a rational Erdős-Straus representation.
background
The module states the exact prime-distribution input needed for the residual Erdős-Straus proof. An effective prime phase input consists of a bound function together with the guarantee that, for every residual trap $n$, there exists $c$ at most the bound such that $c$ is an admissible hard gate and the subset-product phase hit for $n$ and $c$ is nonempty. This input is shown to imply the prime phase box distribution statement required by the representation theorem. The construction deliberately sidesteps the bit-rotted PrimeDistributionBridge file, treating the effective input as the interface.
proof idea
The proof is a one-line wrapper that invokes the prime-phase-box-distribution-to-representation theorem on the box distribution extracted from the effective input together with the residual trap hypothesis.
why it matters
This theorem supplies the final link from effective prime phase supply to the rational representation property. It is invoked by the two sibling results that derive the input from RS prime phase equidistribution and from a phase budget engine. In the Recognition Science chain it closes the residual trapped class using the prime phase machinery, consistent with the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.