phaseBudgetEngine_of_boundedVisibilityEngine
plain-language theorem explainer
The definition constructs a PhaseBudgetEngine from any BoundedVisibilityEngine by copying its bound function and routing the supplies_hit witness through conversion of residual traps to non-identity reciprocals. Researchers extending the Erdős-Straus conjecture via Recognition Science ledger methods cite this to connect visibility engines to budget engines. It is realized as a direct structure instantiation that applies the upstream conversion lemma inside the supplies_hit tactic.
Claim. Let $E$ be a bounded visibility engine. Define the phase budget engine $P$ by $P. bound(n) = E. bound(n)$ for all $n$, and for any residual trap at $n$ let the supplies_hit witness be the visibility of the non-identity reciprocal ledger obtained from the trap via the conversion lemma.
background
A BoundedVisibilityEngine is the structure that packages a bound function, costOf, stability for non-identity reciprocal ledgers, and floor interfaces; its doc-comment states that the witness itself is supplied by the phase-budget engine field because budget arithmetic bounds failed gates but does not construct the subset-product divisor. A PhaseBudgetEngine is the dual structure whose supplies_hit field returns an admissible hard gate $c$ bounded by the engine bound together with a nonempty SubsetProductPhaseHit for every residual trap. The module turns the recovered-ledger visibility engine into the phase-budget engine already consumed by the Erdős-Straus residual proof chain.
proof idea
The definition builds the PhaseBudgetEngine record by setting the bound field directly to the input engine's bound. The supplies_hit field is supplied by a tactic that introduces the residual trap hypothesis, converts it to a non-identity reciprocal using the lemma nonIdentityReciprocal_of_residualTrap, and then applies the engine's visibility function to obtain the required witness.
why it matters
This definition is invoked inside erdos_straus_residual_closed to conclude that bounded phase visibility on recovered ledgers yields an Erdős-Straus representation for every residual trapped $n$. It supplies the exact interface step from BoundedVisibilityEngine to PhaseBudgetEngine in the NumberTheory phase-budget chain. The construction supports the T1/RCL stable-budget interface used for finite phase separation in the Recognition Science treatment of the conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.