StableIntegerLedgerBudget
plain-language theorem explainer
A stable ledger budget for natural number n and cost function costOf is a non-negative real B that upper-bounds the cumulative unresolved phase-failure cost summed over every finite gate set S. Number theorists working on bounded visibility in Recognition Science cite this interface to enforce that unresolved costs stay finite under the T1 budget. The structure is introduced directly by three fields: the budget value, its non-negativity, and the universal inequality against all finite cumulative costs.
Claim. A stable ledger budget for $n ∈ ℕ$ and cost function $costOf : ℕ → ℝ$ consists of a real number $B ≥ 0$ such that the cumulative unresolved phase-failure cost $C(n, costOf, S) ≤ B$ for every finite set $S ⊆ ℕ$.
background
The T1 Phase Budget Bound module states the third phase-budget theorem: a stable integer ledger with finite T1/RCL budget cannot carry unbounded unresolved finite-phase cost. The cumulative unresolved phase cost for any finite S is the sum of per-gate failure costs drawn from costOf, where individual costs originate as J-costs from the multiplicative recognizer and observer-forcing constructions. Upstream, the eight-tick phase supplies the periodic angles kπ/4 for k = 0..7, while the active-edge count A = 1 per tick anchors the φ-power balance at D = 3.
proof idea
This is a structure definition that directly encodes the stable budget interface. It introduces the budget field together with its non-negativity proof obligation and the universal quantification that every finite cumulative failure cost lies below the budget. No lemmas or tactics are invoked; the definition serves as the explicit hypothesis carrier for all downstream bounds.
why it matters
The structure supplies the budget interface required by the no-unbounded-unresolved-phase-cost theorem and the failed-gate-count-bounded-by-budget result in the same module. It is invoked to build BoundedVisibilityEngine and MinimalEngine, which in turn prove that stable budgets force some admissible gates to hit balanced phases. Within the Recognition framework it closes the T1 phase-budget step, ensuring finite budgets derived from the RCL and eight-tick octave prevent unbounded phase costs while remaining consistent with the φ-ladder and α band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.