canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the CPT-from-J-cost certificate is strictly positive. Certificate and domain-cost lemmas in this foundation module cite the bound when they need a positive scale. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from the tighter golden-ratio inequality φ > 1.5.
Claim. The module's canonical threshold (the φ-derived positive scale used by the CPT certificate) satisfies $0 < \tau$, where $\tau$ is that threshold constant.
background
This module builds a structural CPT theorem from Recognition Science: physics is invariant under the combined action of charge conjugation (σ ↦ −σ), spatial reflection on the D = 3 axes, and recognition-tick reversal, realized as J-cost invariance under all three. The local toolkit includes a domain cost, a canonical threshold, and a CPT certificate object, all ultimately tied to the J-cost and the golden ratio.
The only upstream fact used here is the tighter lower bound φ > 1.5. That lemma records that √5 > 2 forces (1 + √5)/2 > 3/2. In RS, φ is the self-similar fixed point forced at T6 of the unified forcing chain; positivity of any threshold built as a simple positive combination of φ (for example a multiple of φ − 1 = φ⁻¹) is then immediate from this bound.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the single upstream lemma φ > 1.5. No case split, no induction, and no appeal to the Recognition Composition Law or to J-uniqueness beyond whatever is already baked into the unfolded definition.
why it matters
Positivity of the canonical threshold is a tiny but necessary arithmetic gate for the structural CPT certificate assembled in this module (status: 0 sorry, 0 axiom). Sibling certificate inhabitants and domain-cost nonnegativity lemmas sit next to it; without a positive threshold the certificate package would not type-check as a genuine scale. In the broader RS chain it sits under T5–T6 (J-cost uniqueness and φ as fixed point) and under the module's reading of CPT as joint J-invariance under C, P, and tick reversal. No external used-by edges are recorded yet; the lemma is presently local scaffolding for the CPT3 certificate rather than a cited export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.