failed_gate_count_bounded_at_KTheta
plain-language theorem explainer
Under a stable ledger budget and the explicit KTheta failure floor hypothesis, any finite collection of failed gates has total cost at most the budget. Number theorists working on phase-cost accumulation in Recognition Science cite this to obtain uniform bounds at the RS floor scale. The proof is a one-line wrapper that instantiates the general failed-gate budget theorem by packaging KTheta positivity, the failure set, and the per-gate floor map.
Claim. Let $n$ be a natural number, let costOf map naturals to reals, and let $S$ be a finite set of naturals. Assume a stable ledger budget exists for $n$ and costOf, and assume the KTheta failure floor hypothesis holds (every failed gate has cost at least $K_Theta$). If every element of $S$ fails to hit the balanced phase, then $K_Theta$ times the cardinality of $S$ is at most the budget.
background
The module BoundedPhaseVisibility shows that stable unresolved-phase budgets together with a uniform KTheta floor prevent finite phase invisibility from exceeding the supplied bound. KThetaFailureFloorHypothesis is the structure whose single field requires that every failed gate (i.e., every c with GateFails n c) satisfies KTheta ≤ costOf c. GateFails n c is the proposition that c does not hit the balanced square-budget phase. StableIntegerLedgerBudget supplies a nonnegative real budget that upper-bounds the cumulative failure cost of every finite set. The upstream theorem failed_gate_count_bounded_by_budget states that a uniform positive floor δ on the costs of all members of S yields δ · card(S) ≤ budget.
proof idea
The proof is a one-line wrapper. It applies failed_gate_count_bounded_by_budget to the given stable budget, then supplies the required UniformFailureFloor witness as the triple consisting of KTheta_pos, the assumption that every element of S fails, and the map that sends each failed c to the lower bound furnished by the KThetaFailureFloorHypothesis.floor field.
why it matters
The declaration supplies the concrete KTheta-scale instance of the general budget bound inside the BoundedPhaseVisibility module. It therefore closes the explicit-hypothesis interface for the RS phase-failure floor (KTheta := Jcost(phi)/45) and feeds any later argument that needs a uniform cost lower bound at that scale. The parent result is the general failed_gate_count_bounded_by_budget theorem; the local setting is the module's claim that finite phase invisibility cannot persist beyond the stable budget once the KTheta floor is assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.