KThetaFailureFloorHypothesis
plain-language theorem explainer
The structure encodes the assumption that every failed gate at scale n incurs cost at least KTheta under the map costOf. Bounded-visibility and minimal-engine constructions cite it to close total-cost bounds on finite failure sets. The definition is a direct packaging of the uniform floor inequality with no additional lemmas.
Claim. Let $n$ be a natural number and let $costOf : ℕ → ℝ$. The hypothesis asserts that for every $c ∈ ℕ$, if gate $c$ fails the balanced-phase test at scale $n$ then $K_Θ ≤ costOf(c)$.
background
The Bounded Phase Visibility module assumes a stable unresolved-phase budget on recovered integer ledgers and requires failed gates to respect a uniform cost floor at the RS scale KTheta. GateFails n c is the predicate that gate c misses the balanced square-budget phase at scale n, imported from PhaseFailureCost. KTheta is the minimal failure cost supplied by UniformFailureFloor and is tied to the eight-tick phases kπ/4 from Foundation.EightTick.
proof idea
The declaration is a structure definition whose single field directly states the universal quantification ∀ c, GateFails n c → KTheta ≤ costOf c. No lemmas or tactics are invoked; the body is the literal floor condition.
why it matters
It supplies the explicit floor input required by BoundedVisibilityEngine, by the theorem failed_gate_count_bounded_at_KTheta that bounds total failure cost by the stable budget, and by the breakthrough lemma hits_balanced_phase_of_floor_and_budget that extracts a balanced-phase hit. The hypothesis closes the T7 eight-tick accounting at the KTheta scale so that phase invisibility remains finite once budget and floor are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.