Pith. sign in
def

canonicalThreshold

definition
show as:
module
IndisputableMonolith.Materials.RS_Matl_Module_012
domain
Materials
line
20 · github
papers citing
none yet

plain-language theorem explainer

Defines the canonical materials threshold as $\varphi - 3/2$, a fixed positive real used as a comparison scale for domain costs in the RS materials module. Materials and condensed-matter workers in the Recognition stack cite it when checking BCS-coherence length scales against the $\varphi$-ladder. The body is a one-line constant definition from the golden ratio.

Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of the Recognition self-similarity relation.

background

Module 12 of the RS materials layer treats BCS coherence lengths as $\varphi$-ladder quantities: $\varphi^7,\mathrm{nm}\approx 29,\mathrm{nm}$ for cuprates and $\varphi^{15},\mathrm{nm}\approx 1364,\mathrm{nm}$ for conventional superconductors, reported as a structural match with no sorry and no axioms.

The constant $\varphi$ is imported from the RS Constants layer (T6: the unique self-similar fixed point forced by the J-cost uniqueness chain). The Cost import supplies the nonnegativity and evaluation infrastructure for domain costs that this threshold is meant to bound or compare against. Sibling facts in the same file assert positivity of the threshold and nonnegativity of the domain cost.

proof idea

Pure definitional abbreviation: the real is set equal to $\varphi - 3/2$ with no proof obligations. Downstream positivity is handled by a separate lemma (canonicalThreshold_pos), not by this declaration.

why it matters

Gives a single named scale against which materials domain costs can be compared inside the RS stack, tying condensed-matter length matches (cuprate and conventional BCS $\xi$) to the same $\varphi$ forced at T6 of the unified forcing chain. It sits beside the domain-cost definitions and the module certificate (RSMatl012Cert) that package the structural match. No parent theorems are recorded as direct dependents in the graph; its role is local scaffolding for the materials certificate rather than a step in the T0–T8 forcing spine.

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