canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant for the physics structural certificate at recognition rung 46 is strictly positive. Anyone assembling or citing that certificate needs this fact so domain-cost bounds stay on the positive side of zero. The argument is a one-line wrapper: unfold the threshold and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold $T$ used by the Recognition Science physics structural certificate at rung 46 satisfies $0 < T$.
background
Module Structural_Physics_mod46 packages a structural Recognition Science prediction for the Physics domain at recognition rung 46. It is marked as a structural theorem block (no sorry, no extra axioms). Sibling definitions introduce a domain cost and a canonical threshold built from the golden ratio φ; the present lemma only records that this threshold is positive.
The sole upstream input is the constant bound φ > 1.5. That lemma records the elementary comparison (1 + √5)/2 > 3/2, obtained from √5 > 2. In RS units φ is the self-similar fixed point forced by the J-cost uniqueness chain (T5–T6), so lower bounds on φ are the standard way to discharge elementary positivity obligations for rung-level thresholds.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the hypothesis φ > 1.5. No case split, no induction, and no appeal to the Recognition Composition Law: positivity is pure real arithmetic once the threshold is expanded in φ.
why it matters
Rung-46 structural physics certificates need a strictly positive threshold so that domain-cost comparisons and certificate inhabitation stay meaningful. This lemma closes that elementary obligation inside Structural_Physics_mod46. It sits downstream of the forced golden ratio (T6) via the tighter numerical bound φ > 1.5, and it supports the sibling certificate bundle (StructPhysicsM46Cert / cert_inhabited) even though no external used-by edge is recorded yet. It does not itself derive masses, α, or dimensional forcing; it only keeps the local threshold on the correct side of zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.