RSAdSCFTRS
plain-language theorem explainer
A certificate structure for the RS reading of AdS/CFT: bulk cost vanishes on the diagonal, is nonnegative off it for positive mass/energy, and the canonical threshold is strictly positive. Anyone citing the structural AdS/CFT claim in RS (D=3 forcing bulk D+1=4) uses this bundle. It is a pure field package; inhabitation is discharged separately by the concrete cert instance.
Claim. A record asserting three facts about the domain cost $C$ and the canonical threshold $\tau$: (i) $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module frames AdS/CFT inside Recognition Science: spatial dimension $D=3$ is forced (forcing chain T8), so the bulk AdS dimension is $D+1=4$ and the boundary CFT lives in dimension $D=3$. The duality is treated as structurally natural once that dimension count is fixed.
The structure packages analytic side-conditions on a real bivariate cost domainCost (the local stand-in for bulk/boundary mismatch cost) together with a positive scalar canonicalThreshold. Upstream, the ordinary recognition cost is already known to be nonnegative: any recognition event $e$ satisfies $0\le e.\mathrm{cost}$ by nonnegativity of the $J$-cost on positive states. The present fields lift that nonnegativity (and a diagonal-vanishing identity) to the domain-cost used for the AdS/CFT certificate.
proof idea
No proof body: this is a structure declaration. It only names three Prop-valued fields that any inhabitant must supply. Concrete discharge is deferred to the sibling definitions domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, which are assembled into the instance cert.
why it matters
Gives the typed interface for the module's structural AdS/CFT claim (status: structural theorem, zero sorry). Downstream, cert builds an explicit inhabitant by wiring the three sibling lemmas, and cert_inhabited records Nonempty RSAdSCFTRS. That inhabitation is what lets later foundation material treat the RS AdS/CFT reading as available data rather than an open hypothesis.
Framework landmark: T8 forces $D=3$, which is exactly the dimension count the module-doc uses to identify bulk $D+1=4$ with boundary $D=3$. The structure does not re-prove T8; it only packages the cost/threshold side-conditions that sit on top of that dimension forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.