cert
plain-language theorem explainer
A packed certificate that the RS domain cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and that the canonical threshold is positive. Anyone citing the RS-forced AdS4/CFT3 structural theorem uses this inhabited instance. The definition is a pure structure assembly wiring three already-proved sibling lemmas into the three fields.
Claim. There is a certificate of the RS AdS/CFT structure whose three fields assert: $\mathrm{domainCost}(r,r)=0$ for every $r\neq 0$; $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; and the canonical threshold is strictly positive.
background
The module records the structural claim that AdS/CFT is natural once Recognition Science forces spatial dimension $D=3$: bulk (AdS) dimension is $D+1=4$ and boundary (CFT) dimension is $D=3$. Status is a structural theorem with no sorry and no axioms.
The structure being inhabited packages three cost-side properties of a domain cost functional on pairs of positive reals: vanishing when the two arguments agree (and are nonzero), nonnegativity for positive mass and energy arguments, and positivity of a fixed canonical threshold. Upstream, the general recognition cost is already known to be nonnegative: any recognition event has cost at least zero because the J-cost is nonnegative on positive states.
Sibling lemmas in this file discharge the three fields for the concrete domain cost and threshold used here.
proof idea
Pure structure construction, not a tactic proof. The three fields of RSAdSCFTRS are filled by direct assignment: diagonal vanishing from the sibling domainCost_at_eq, nonnegativity from domainCost_nonneg, and threshold positivity from canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
This certificate is the concrete inhabitant that makes the RS AdS/CFT structure available as data rather than as an abstract Prop. It sits inside the Foundation layer that records how the forced $D=3$ (forcing-chain step T8) makes bulk dimension four and boundary dimension three, so the AdS/CFT pairing is not an extra postulate. Downstream use is currently empty in the graph, but the sibling cert_inhabited and any later AdS/CFT bridge lemmas are the natural consumers. It does not itself derive the duality dictionary; it only locks the cost and threshold side conditions the module treats as the structural core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.