phaseBudgetEngine
plain-language theorem explainer
A minimal visibility engine directly supplies a phase budget engine instance for the Erdos-Straus residual class. The bound map returns the admissible gate witness chosen from the subset product hit when the input satisfies ResidualTrap, and defaults to zero otherwise. This is a direct construction whose supplies_hit property follows by extracting the chosen witness and its admissibility and hit facts from the upstream subset product theorem.
Claim. Let $E$ be a minimal visibility engine (a structure carrying a cost function together with stable budget and KTheta floor hypotheses for every non-identity reciprocal ledger). The induced phase budget engine $P_E$ has bound function sending each residual trap $n$ to the admissible hard gate $c$ witnessing a nonempty subset product phase hit for $n$, and sending all other $n$ to zero. For every residual trap $n$ the supplies_hit property then asserts existence of $c$ with $c$ admissible, $c$ at most the bound, and the subset product phase hit nonempty.
background
The Minimal Visibility Engine module repackages a bounded visibility engine by dropping the explicit visibility field (now recovered as the theorem hits_balanced_phase_of_floor_and_budget) and retaining only the RS-physical inputs: a stable budget condition and a uniform KTheta failure floor hypothesis. A MinimalEngine is the structure with fields costOf : ℕ → ℕ → ℝ, stable : ∀ n, NonIdentityReciprocal n → StableIntegerLedgerBudget n (costOf n), and floor : ∀ n, NonIdentityReciprocal n → KThetaFailureFloorHypothesis n (costOf n). Upstream, NonIdentityReciprocal n asserts that n is positive, not 1, and admits a reciprocal budget; ResidualTrap n asserts the stricter arithmetic conditions n ≡ 1 mod 24 together with all prime factors congruent to 1 mod 3. The target PhaseBudgetEngine structure (from PhaseBudgetToErdosStraus) is exactly the interface that supplies a bound map and the supplies_hit property delivering an admissible hard gate plus nonempty SubsetProductPhaseHit for each residual trap.
proof idea
The definition is a direct construction: the bound field is defined by classical choice of the gate returned by subset_product_hit_of_minimal engine (nonIdentityReciprocal_of_residualTrap hn) when ResidualTrap n holds, and by 0 otherwise. The supplies_hit proof proceeds by introducing the non-identity reciprocal from the trap, obtaining the existence witness hex from subset_product_hit_of_minimal, and refining to the chosen gate together with its three required properties (admissibility, hit membership, and the bound inequality) via Classical.choose_spec.
why it matters
This definition supplies the PhaseBudgetEngine instance required by the downstream theorem erdos_straus_residual_from_minimal_engine, which concludes that every minimal visibility engine yields a rational Erdos-Straus representation for the residual class. It therefore completes the bridge from the explicit RS inputs (stable budget and KTheta floor) to an explicit admissible gate witness inside the phase-budget-to-Erdos-Straus interface. In the larger framework the construction supports the visibility engine's role after the explicit formulas have isolated the residual traps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.