UniformFailureFloor
plain-language theorem explainer
UniformFailureFloor defines the predicate that a finite set S of gates all fail at phase n with identical positive cost lower bound δ. Phase-budget analysts in Recognition Science cite it when deriving cardinality bounds on unresolved failures from a stable ledger. The definition is the direct conjunction of δ > 0, universal gate failure, and the uniform cost inequality.
Claim. Let $n$ be a natural number, $costOf : ℕ → ℝ$ a cost function, $S$ a finite set of gate indices, and $δ ∈ ℝ$. The predicate holds precisely when $δ > 0$, every gate $c ∈ S$ fails at level $n$, and $δ ≤ costOf(c)$ for all $c ∈ S$.
background
The T1 Phase Budget Bound module shows that a stable integer ledger with finite T1/RCL budget cannot sustain unbounded unresolved finite-phase cost. UniformFailureFloor encodes the uniform-failure scenario that feeds the cardinality bound. It draws on the J-cost structure from PhiForcingDerived and the ledger factorization from DAlembert.LedgerFactorization, both of which supply the costOf map and the notion of gate failure.
proof idea
The declaration is a definition whose body is the conjunction of three atomic conditions: positivity of δ, the predicate GateFails n c for every c in S, and the lower bound δ ≤ costOf c for every c in S. No lemmas are applied; the body directly assembles the uniform-floor hypothesis.
why it matters
It supplies the hypothesis for the theorem failed_gate_count_bounded_by_budget, which concludes δ · |S| ≤ stable.budget. This step closes the argument that a finite budget forbids unbounded unresolved phase cost, consistent with the T1 phase-budget claim in the module doc-comment. The construction sits inside the broader Recognition forcing chain that derives discrete phase structure from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.