Pith. sign in
theorem

canonicalThreshold_pos

proved
show as:
module
IndisputableMonolith.Foundation.Tribonacci_RS
domain
Foundation
line
21 · github
papers citing
none yet

plain-language theorem explainer

The canonical threshold constant in the Tribonacci recognition module is strictly positive. Anyone building domain-cost bounds or Tribonacci certificates at D=3 cites this hygiene fact. The proof is a one-line unfold of the threshold definition followed by linear arithmetic from the bound φ > 1.5.

Claim. The canonical threshold real $t$ (the explicit $\varphi$-built constant of this module) satisfies $0 < t$.

background

The module treats the Tribonacci constant $T \approx 1.839$ as a structural object in Recognition Science: at spatial dimension $D=3$ the recognition chain carries three prior terms, matching the recurrence $T^3 = T^2 + T + 1$. Status is structural (zero sorry, zero axiom). The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the chain (T6).

The canonical threshold is a real assembled from $\varphi$ for domain-cost comparisons in this file. The only upstream fact needed is the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$ so that $(1+\sqrt{5})/2 > 3/2$.

proof idea

One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the lemma $\varphi > 1.5$. No further case splits or algebraic identities are required; positivity is immediate from the linear inequality after unfolding.

why it matters

Basic positivity hygiene for the Tribonacci certificate layer under Foundation. Sibling facts (domain-cost nonnegativity, certificate inhabitation) rely on a positive threshold scale when comparing costs at D=3. In the forcing chain this sits under T8 (three spatial dimensions) and the three-term memory that makes Tribonacci natural beside the eight-tick octave (T7). No recorded downstream consumers yet; the lemma closes a local positivity obligation inside the structural Tribonacci development rather than a paper proposition by name.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.