pith. sign in
module module high

IndisputableMonolith.NumberTheory.PhaseFailureCost

show as:
view Lean formalization →

The PhaseFailureCost module quantifies costs from gates missing the balanced phase inside square-budget divisor boxes. It introduces failure predicates, cost functions, and accumulation lemmas that track unresolved finite-phase expenses. Researchers bounding phase budgets in Recognition Science cite it to control ledger costs under finite T1/RCL constraints. The module consists of direct definitions and basic accumulation properties drawn from the upstream box-phase isolation.

claimFor square budget $N^2$ and complementary divisor pair $(d,e)$ with $d e = N^2$, a gate fails when it misses the balanced phase. The failure cost function $C_f$ and its cumulative sum satisfy $C_f(S) = 0$ only on balanced phases and admit a positive lower bound on any unresolved set.

background

The upstream Erdős-StrausBoxPhase module isolates the finite combinatorial part of the residual Erdős-Straus proof. For a square budget $N^2$, a divisor exponent box is represented by a complementary pair $(d,e)$ with $d e = N^2$. This representation works directly with exponent ranges $0 ≤ a_p ≤ 2 v_p(N)$ without expanding the full prime factorization.

proof idea

This is a definition module, no proofs. It first declares the failure predicate and cost function, then states the accumulation lemma and the packaged lower-bound statement.

why it matters in Recognition Science

The module supplies the finite-phase cost machinery required by the T1 Phase Budget Bound theorem. That theorem states a stable integer ledger with finite T1/RCL budget cannot carry unbounded unresolved finite-phase cost. The definitions and accumulation properties close the accounting step that converts phase misses into explicit budget charges.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)