AdSCFT
plain-language theorem explainer
The AdSCFT structure encodes the dimensional hierarchy of the AdS/CFT correspondence for use in holographic derivations. Researchers working on quantum gravity bounds from ledger projections cite it when linking bulk gravity descriptions to boundary field theories. The declaration is a plain structure with three fields that enforce the single relation boundary dimension equals bulk dimension minus one.
Claim. A structure with bulk dimension $n$, boundary dimension $m$, and the constraint $m = n - 1$.
background
Recognition Science derives the holographic bound from ledger projection, where the ledger is fundamentally two-dimensional and volume emerges from boundary data. The module targets the inequality $S ≤ A / (4 l_P^2)$ and notes that black holes saturate the bound as maximally dense ledgers. Upstream results supply the Dimension structure tracking length-time-mass exponents and the entropy definition as total defect of a configuration.
proof idea
The declaration is a structure definition. It introduces the three fields bulk_dim, boundary_dim, and dim_relation directly with no lemmas or tactics applied.
why it matters
This definition supplies the dimensional setup required for the holographic bound derivation in QG-006. It connects to the Ryu-Takayanagi comment in the module and to the spatial dimension forcing that yields D = 3. No used_by edges are recorded, so it serves as scaffolding for sibling results such as holographic_bound and information_scales_as_area.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.