RSPrimePhaseEquidistribution
plain-language theorem explainer
RSPrimePhaseEquidistribution bundles an EffectivePrimePhaseInput with a marker asserting derivation from the RCL prime-ledger phase distribution rather than finite search. Number theorists working on the residual Erdős-Straus conjecture inside the Recognition Science framework cite this structure as the canonical source interface for the required prime-phase supply. The declaration is introduced directly as a structure definition that packages the input without performing any derivation.
Claim. A structure consisting of an effective prime phase input $I$ (a function bound : ℕ → ℕ such that for every residual trap $n$ there exists $c ≤ bound n$ with admissible hard gate $c$ and nonempty subset-product phase hit for $n$) together with the marker that $I$ is sourced from the recognition composition law applied to the prime ledger.
background
The module states the exact prime-distribution input needed for the residual Erdős-Straus proof and shows that this input implies PrimePhaseBoxDistribution. It deliberately avoids the bit-rotted PrimeDistributionBridge.lean, treating that file as a future source candidate rather than a dependency. EffectivePrimePhaseInput is the sibling structure requiring that bounded prime phase supply produces an actual subset-product phase hit for every trapped ledger. Upstream results supply the eight-tick phases (kπ/4 for k = 0..7), the J-cost of recognition events, and the cost function induced by multiplicative recognizers; these supply the phase and cost vocabulary used to interpret the prime-ledger marker.
proof idea
The declaration is a structure definition with two fields: the effective input and the boolean marker True. No lemmas are applied; the construction is a direct bundling that serves as an interface for downstream extraction.
why it matters
This structure supplies the final remaining input for the residual Erdős-Straus chain. It is extracted by effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution and fed into erdos_straus_residual_from_rsPrimePhaseEquidistribution to obtain the rational representation HasRationalErdosStrausRepr. The marker explicitly points to the RCL/J-cost prime-ledger machinery, closing the interface that connects eight-tick phase distribution and multiplicative recognizer costs to the Erdős-Straus residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.