PrimePhaseBoxDistribution
plain-language theorem explainer
Prime phase box distribution packages a bound function and hits predicate ensuring admissible gates exist for every residual trapped n. Number theorists working on the Erdős-Straus conjecture inside Recognition Science cite this structure to supply the required square-budget phase hits. The declaration is a direct structure definition with no lemmas or reduction steps.
Claim. A prime phase box distribution consists of a bound function $b:ℕ→ℕ$ and the property that for every $n$ satisfying the residual trap conditions there exists $c≤b(n)$ with $c≡3 mod 4$ such that the square-budget divisor box for $n$ hits the balanced residual phase at gate $c$.
background
The module establishes the interface for prime phase distribution over square-budget divisor boxes in the Erdős-Straus setting after RCL algebra and finite closure are secured. Upstream definitions include the eight-tick phase $kπ/4$ for $k=0..7$, ledger balanced as balanced event list, HitsBalancedPhase requiring a divisor exponent box where gate $c$ divides both $N+boxDivisor$ and the reciprocal defects land in phase, AdmissibleHardGate as $c≡3 mod 4$, and ResidualTrap as $n>1$, $n≡1 mod 24$, with all prime factors ≡1 mod 3 for both $n$ and $(n+3)/4$. The wedge phase supplies the unimodular complex $e^{iw}$.
proof idea
This is a structure definition that directly introduces the bound field of type $ℕ→ℕ$ and the hits field as the stated universal quantifier over ResidualTrap. No lemmas are applied and no tactics are used.
why it matters
The structure supplies the exact interface consumed by boundedBalancedSearch_of_primePhaseBoxDistribution and erdos_straus_residual_from_prime_phase_box_distribution, which in turn yields the rational Erdős-Straus representation. It also populates the distribution field inside RSPrimePhaseBoxTheorem, closing the module's stated remaining step from RS prime ledger to square-budget phase hits and linking to the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.