canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold scalar as φ − 3/2 in RS-native units. Cited by the AdS/CFT structural layer that ties forced D = 3 to bulk dimension 4. The body is a one-line arithmetic abbreviation of the golden-ratio constant from Constants.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point of the Recognition cost (the golden ratio).
background
The module treats AdS/CFT as natural once Recognition Science forces spatial dimension $D = 3$ (forcing chain T8): bulk AdS dimension is then $D+1 = 4$ and the dual CFT lives in dimension $D = 3$. Status is structural (no sorry, no axioms).
The constant $\varphi$ is imported from Constants and is the unique positive solution of the self-similarity fixed-point equation forced at T6; numerically $\varphi = (1+\sqrt{5})/2$. Cost infrastructure from Cost supplies the J-cost and related nonnegativity facts used by sibling lemmas in the same file.
This declaration simply names the real combination $\varphi - 3/2$ that later positivity and certificate statements treat as the working threshold scale for the RS AdS/CFT comparison.
proof idea
Definition, not a proved statement. The body is the closed term phi - 3 / 2 with phi the golden-ratio constant; no tactics or lemmas are applied.
why it matters
Gives a single named real that the RS AdS/CFT structural theorem can quote when comparing domain cost against a fixed cutoff. It sits next to domainCost, canonicalThreshold_pos, and the certificate bundle RSAdSCFTRS / cert, which package the claim that AdS$_4$/CFT$_3$ is the dimensionally forced dual once T8 has fixed $D = 3$.
In the broader framework it is a bookkeeping constant, not a new forcing step: $\varphi$ already comes from T6, and the offset $3/2$ is chosen so the threshold sits in the small positive band below the Berry scale $\varphi^{-1}$ and well below $Z_{\mathrm{cf}} = \varphi^5$. No open scaffold is closed here; the value is pure notation for downstream inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.