canonicalThreshold_pos
plain-language theorem explainer
The module's canonical threshold constant is strictly positive. Anyone citing the recognition-side Heisenberg bound (Δ_J Δ_σ ≥ ħ_R/2) needs this positivity to keep the right-hand side meaningful. The proof unfolds the definition and finishes by linear arithmetic from the elementary bound φ > 1.5.
Claim. The canonical threshold constant of the recognition-Heisenberg module is strictly positive: $0 < \ thr_{\mathrm{can}}$.
background
The module derives a structural Heisenberg relation from the J-cost: recognition-Heisenberg at the φ-rung reads Δ_J · Δ_σ ≥ ħ_R/2 with ħ_R = J(φ)·ħ. Status is a structural theorem (zero sorry, zero axiom).
The golden ratio φ = (1+√5)/2 is the self-similar fixed point forced at T6 of the unified forcing chain. The only upstream fact used here is the elementary tightening φ > 1.5 (from √5 > 2). The canonical threshold is the module-local constant obtained by unfolding a φ-expression; its positivity is the minimal arithmetic fact needed before any product bound can be stated with a positive floor.
proof idea
One-line wrapper: unfold the definition of the canonical threshold, then apply linarith to the lemma phi_gt_onePointFive (φ > 1.5). No further Recognition lemmas are required; the inequality is pure real arithmetic once the definition is expanded.
why it matters
Positivity of the canonical threshold is the first arithmetic gate in the UncertaintyPrinciple3Deep development. Without it the recognition-Heisenberg floor ħ_R/2 would not be known to be positive, and the structural certificate (HUP3DeepCert / cert) could not be inhabited as a genuine lower bound. It sits inside the Foundation layer that converts the J-cost and the forced φ (T5–T6) into concrete uncertainty inequalities; the module claims a consistent structural derivation of Heisenberg from recognition cost rather than from operator commutators. No downstream edges are recorded yet, so the immediate consumers are the sibling certificate constructions in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.