pith. sign in
module module high

IndisputableMonolith.NumberTheory.LogicPhaseBudgetBridge

show as:
view Lean formalization →

LogicPhaseBudgetBridge supplies a phase-budget engine native to LogicNat carriers for bounds and inputs. It transports finite gate witnesses to the classical Erdős-Straus surface through imported adapters. Researchers extending Recognition Science number theory bounds would cite this for maintaining representation consistency across logic and classical layers. The module composes the logic Erdős-Straus box phase adapter with the phase-budget to RCL chain.

claimThe module defines a logic-native phase-budget engine $E$ over carrier LogicNat such that finite gate witnesses transport to the classical Erdős-Straus box-phase theorem, returning results as LogicRat via the RCL closure.

background

This module sits in the NumberTheory domain and bridges logic-native structures to classical ones. It imports LogicErdosStrausBoxPhase, which supplies a logic-native adapter for the Erdős-Straus square-budget box phase with native combinatorial structures over LogicNat; the final theorem transports to the existing ℕ box-phase theorem and returns the result as a LogicRat representation via LogicErdosStrausRCL. It also imports PhaseBudgetToErdosStraus, which composes the phase-budget interface with the already-proved Erdős-Straus RCL closure chain, conditional on a PhaseBudgetEngine package that encodes the T1/RCL budget, uniform failure floor, and finite gate enumeration producing bounded subset-product phase hits for every residual trap.

proof idea

This is a definition module, no proofs. It structures the argument by importing the logic Erdős-Straus box phase adapter and the phase budget to Erdős-Straus composer, then exposing the bridged engine through sibling definitions such as PhaseBudgetEngineLogic, toClassicalEngine, and erdos_straus_residual_from_phaseBudget_logic.

why it matters in Recognition Science

The module earns its place by enabling logic-native computations to interface with the proved Erdős-Straus RCL closure chain. It feeds the parent results in the Recognition framework's number theory applications for phase-budget engines, particularly supporting the T1/RCL budget and finite gate enumeration setting. It closes the representation gap between LogicNat carriers and classical surfaces without introducing new combinatorial content.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)