KTheta_pos
plain-language theorem explainer
KTheta_pos establishes that the RS phase-failure floor KTheta is strictly positive. Phase-budget analyses cite it to guarantee that failure costs stay bounded away from zero. The proof is a direct term-mode division of the known positivity of Jcost phi by the positive constant 45.
Claim. The RS phase-failure floor scale satisfies $0 < K_Theta$ where $K_Theta := J(phi)/45$.
background
The Uniform Failure Floor module defines KTheta as the RS phase-failure floor scale via the noncomputable definition KTheta := Jcost phi / 45. This quantity supplies the minimum cost per failed finite phase gate inside the phase-budget engine. The module proves only positivity; the explicit KThetaFailureFloorHypothesis interface is stated separately in BoundedPhaseVisibility.
proof idea
The proof unfolds the definition of KTheta to expose the division Jcost phi / 45. It applies the upstream lemma Jcost_phi_pos to obtain positivity of the numerator, then invokes div_pos together with the norm_num fact that 0 < 45.
why it matters
KTheta_pos supplies the strict positivity input to KTheta_nonneg and to the bounding results failed_gate_count_bounded_at_KTheta and hits_balanced_phase_of_floor_and_budget. It completes the positivity step for the uniform failure floor construction that anchors the phase-budget engine. The result sits inside the NumberTheory layer that supports later visibility and balanced-phase claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.