Pith. sign in
theorem

canonicalThreshold_pos

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

plain-language theorem explainer

The canonical threshold on the D=3 recognition configuration space is strictly positive. Anyone comparing domain costs or setting cutoffs on C_3 would cite it. Proof is a one-line unfold of the threshold definition followed by linear arithmetic from φ > 1.5.

Claim. The canonical threshold (the explicit real cutoff built from $\varphi$ in the $D=3$ configuration-space module) is strictly positive: $0 < \tau_{\mathrm{can}}$.

background

The ambient module fixes the Recognition Science configuration space at spatial dimension three: $C_3=\mathbb{R}^3$ equipped with the recognition metric $ds^2=J(dx/x)$ on the positive orthant. That metric is the J-cost Riemannian structure; the module records it as positive definite for all $x>0$, and the whole file is marked a structural theorem (zero sorry, zero axiom).

The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the chain. The only upstream fact used here is the tighter numerical bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The canonical threshold is the named real constant in this module against which domain costs are compared; positivity is the elementary gate before any comparison lemmas fire.

proof idea

One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting linear inequality by linarith supplied with the lemma $\varphi>1.5$. No further Recognition identities are required.

why it matters

Supplies the positivity gate for the D=3 configuration-space certificate package (siblings ConfigSpaceD3Cert, cert, cert_inhabited). Without $0<\tau_{\mathrm{can}}$, domain-cost comparisons and threshold cuts on $C_3$ are ill-posed. It sits under the structural D=3 layer (forcing landmark T8) and the J-cost metric on the positive orthant; it does not itself invoke the Recognition Composition Law or the eight-tick octave. The dependency graph currently shows no downstream consumers, so the lemma is infrastructure waiting on later cost or certificate arguments.

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