KTheta_nonneg
plain-language theorem explainer
The nonnegativity of the RS phase-failure floor scale follows from its strict positivity. Researchers applying phase-budget bounds in Recognition Science cite this result to confirm the floor remains nonnegative when bounding finite gate sets. The proof is a direct one-line reduction using the order lemma on the positivity theorem for the same quantity.
Claim. $0 ≤ J(φ)/45$
background
The UniformFailureFloor module defines the RS phase-failure floor scale as Jcost(phi) divided by 45. This quantity acts as the uniform positive δ in the upstream definition UniformFailureFloor, which requires δ > 0 together with the condition that every gate in a finite set S fails and incurs cost at least δ. KTheta_pos proves the strict inequality 0 < J(φ)/45 by unfolding the definition and invoking positivity of Jcost_phi_pos with the fact that 45 > 0. The local setting is the phase-budget engine that supplies a concrete lower bound on failure costs for finite phase gates.
proof idea
The proof is a one-line wrapper that applies le_of_lt to KTheta_pos.
why it matters
This nonnegativity result supplies the sign condition required by the parent theorem hits_balanced_phase_of_floor_and_budget in VisibilityFromFloorBudget. That theorem derives the existence of an admissible hard gate hitting a balanced phase from a stable integer ledger budget together with the KTheta failure floor hypothesis. It completes the positivity step for the floor scale J(φ)/45 inside the NumberTheory layer, ensuring the uniform failure floor construction can be invoked without sign obstructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.