KThetaFailureFloorHypothesis
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of KTheta from the phi-ladder.
- Does not assert existence of any failing gate.
- Does not bound the cardinality of the failure set.
- Does not connect costOf to the J-cost functional beyond the supplied map.
Lean usage
theorem use_floor {n : ℕ} {costOf : ℕ → ℝ} (floor : KThetaFailureFloorHypothesis n costOf) : Prop := floor.floorformal statement (Lean)
33structure KThetaFailureFloorHypothesis (n : ℕ) (costOf : ℕ → ℝ) : Prop where
34 floor :
35 ∀ c : ℕ, GateFails n c → KTheta ≤ costOf c
36
37/-- A bounded visibility package: a gate below `bound n` with a concrete
38subset-product phase hit. -/