PhaseBudgetEngineLogic
plain-language theorem explainer
Logic-native phase-budget engine wraps the classical PhaseBudgetEngine using LogicNat carriers and a compatibility condition on bounds. Researchers lifting Erdős-Straus residual theorems to the logic setting cite this structure. It is defined as a record with bound map, classical engine reference, and the toNat agreement axiom.
Claim. A structure comprising a map $b : N_{logic} → N_{logic}$, a classical phase-budget engine $E$, and the axiom $∀ n, toNat(b(n)) = E.bound(toNat(n))$.
background
LogicNat is the inductive type with constructors identity and step, representing the orbit generated by multiplication in the positive reals under the logic-forced arithmetic. The map toNat extracts the iteration count as an ordinary natural number. PhaseBudgetEngine is the structure supplying a bound function on naturals together with the guarantee that for any residual trap there exists a small admissible gate realizing a subset-product phase hit. This module provides the logic wrapper so that the Erdős-Straus residual result can be stated directly in the recovered-rational language.
proof idea
The declaration is a structure definition assembling the bound function on LogicNat, the classical engine, and the single compatibility axiom that equates the bounds after applying toNat. No tactics or lemmas are applied; the type is introduced directly.
why it matters
This structure supplies the interface used by erdos_straus_residual_from_phaseBudget_logic to transport the residual trap solution into the logic setting. It closes the bridge between the classical phase-budget engine and the logic-native arithmetic, allowing the final residual theorem to be read as a recovered-rational statement. In the Recognition framework it connects the eight-tick phase structure to the Erdős-Straus conjecture via the phase-budget mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.