Pith. sign in
theorem

canonicalThreshold_pos

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

plain-language theorem explainer

The canonical threshold constant is strictly positive. Anyone citing gap-45 structural bounds or domain-cost comparisons at the minimum stable self-reference rung needs this sign fact. The proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.

Claim. The canonical threshold (the real constant obtained by unfolding its definition in terms of the golden ratio $\varphi$) satisfies $0 < \mathrm{canonical\,threshold}$.

background

Module RS_FDN_Structural_004 packages the gap-45 structural fact: at spatial dimension $D=3$, the combination $D^2(D+2)=9\cdot 5=45$ is the minimum rung supporting stable self-reference. The module defines a domain cost and a canonical threshold used to mark that stability floor.

The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced by the Recognition Composition Law (T6). The upstream lemma phi_gt_onePointFive records the elementary bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The canonical threshold is a real expression in $\varphi$ whose positivity is the content of the present theorem; sibling lemmas establish nonnegativity and evaluation identities for the related domain cost.

proof idea

One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting strict inequality by linarith using the single fact $\varphi>1.5$ from phi_gt_onePointFive. No further Recognition-specific lemmas are required.

why it matters

Positivity of the canonical threshold is the sign gate for gap-45 comparisons in the structural foundation layer. Without $0<$ threshold, domain-cost inequalities that certify the minimum rung for stable self-reference at $D=3$ cannot fire. The result sits inside the T8/$D=3$ and T6/$\varphi$ forcing chain: eight-tick octave structure and the $\varphi$-ladder both presuppose a positive scale against which rung offsets (including the gap-45 offset) are measured. No downstream consumers are wired yet in the graph; the certificate objects in the same module (RSFDNStructural004Cert, cert_inhabited) are the immediate packaging layer.

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