effectivePrimePhaseInput_of_phaseBudgetEngine
plain-language theorem explainer
A phase-budget engine supplies an effective prime phase input by direct reuse of its bound function and hit-supplying predicate. Number theorists extending the Erdős-Straus conjecture through Recognition Science phase budgets cite this conversion. The definition is a one-line structure coercion that equates the two interfaces without additional proof obligations.
Claim. Let $E$ be a phase-budget engine. Then $E$ induces an effective prime phase input $I$ defined by $I.bound(n) = E.bound(n)$ and $I.supplies_generators(n,h) = E.supplies_hit(n,h)$ for every residual trap $h$.
background
PhaseBudgetEngine is the structure with fields bound : ℕ → ℕ and supplies_hit : ∀ n, ResidualTrap n → ∃ c ≤ bound n ∧ AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c). EffectivePrimePhaseInput is the parallel structure whose supplies_generators field carries the same logical content. The module composes the phase-budget interface with the already-proved Erdős-Straus RCL closure chain, treating the engine as the explicit package that turns T1/RCL budget facts into a bounded gate witness. Upstream results include the eight-tick phase definition and the balanced ledger property that underwrite the residual-trap setting.
proof idea
This definition is a one-line wrapper that projects the bound and supplies_hit fields of the PhaseBudgetEngine directly into the EffectivePrimePhaseInput structure.
why it matters
The conversion lets any phase-budget engine feed the bounded balanced search engine and the Erdős-Straus residual theorem. It supplies the remaining physical bridge from budget facts to explicit gate witnesses in the RCL closure chain. The immediate parents are boundedBalancedSearch_of_phaseBudget and erdos_straus_residual_from_phaseBudget, both of which apply the resulting effective input to solve trapped classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.