PrimePhaseBoxDistribution
Prime phase box distribution packages a bound function from naturals to naturals together with a hits predicate that supplies, for every residual-trapped n, an admissible gate c inside the bound whose divisor box lands in balanced phase. Number theorists extending the Erdős-Straus conjecture inside Recognition Science cite this structure as the exact interface between prime-phase supply and bounded search. The declaration is a pure structure definition carrying no proof obligations.
claimA structure consisting of a function $bound : ℕ → ℕ$ and the property that for every $n$ satisfying ResidualTrap($n$) (i.e., $n>1$, $n≡1 mod 24$, and all prime factors of both $n$ and $(n+3)/4$ are ≡1 mod 3) there exists $c≤bound(n)$ with $c≡3 mod 4$ such that HitsBalancedPhase($n$,$c$) holds.
background
ResidualTrap($n$) requires $n>1$, $n≡1 mod 24$, and that both $n$ and $(n+3)/4$ have exclusively prime factors ≡1 mod 3. AdmissibleHardGate($c$) is the condition $c≡3 mod 4$. HitsBalancedPhase($n$,$c$) asserts existence of $x$, $N$ and a divisor-exponent box such that $N=nx$, $c=4x-n$, and $c$ divides $N$ plus the box divisor, ensuring both reciprocal defects lie in phase $-N$ modulo $c$ (EightTick.phase supplies the underlying $kπ/4$ angles; LedgerForcing.balanced supplies the ledger balance predicate).
proof idea
This is a structure definition with an empty proof body. It simply records the bound function and the universal quantifier over residual traps; no lemmas or tactics are applied.
why it matters in Recognition Science
The structure is the input type for boundedBalancedSearch_of_primePhaseBoxDistribution, which converts it into a BoundedBalancedSearchEngine and thereby yields ErdosStrausRCL.HasRationalErdosStrausRepr via erdos_straus_residual_from_prime_phase_box_distribution. It supplies the precise distribution statement required by the module's remaining global step for square-budget phase hits. In the Recognition framework it bridges the prime ledger to the Erdős-Straus conjecture using the RCL algebra and eight-tick structure; RSPrimePhaseBoxTheorem records the intent to derive the distribution from first-principles RCL/J-cost machinery.
scope and limits
- Does not assert existence of any concrete bound function.
- Does not construct or compute the bound explicitly.
- Does not verify the hits property for any specific integer n.
- Does not reference J-cost, forcing chain, or phi-ladder directly.
formal statement (Lean)
27structure PrimePhaseBoxDistribution where
28 bound : ℕ → ℕ
29 hits :
30 ∀ n : ℕ, ResidualTrap n →
31 ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ HitsBalancedPhase n c
32
33/-- The exact finite-combinatorial conversion:
34prime phase box distribution gives the bounded balanced search engine. -/