In a PSC universe with stable records, "holography" is best formalized as a closure-preserving interpretation between observational semantics (Paper 27): bulk and boundary with worldMap, obsMap, and satisfaction preservation. This paper does not prove AdS/CFT or any specific duality; it proves theorem-grade constraints. (1) World-type holography (T48. 1): boundary can determine bulk up to observational equivalence via a surjective world-type map. (2) No-free-bits reconstruction (T48. 2): deciding a non-invariant bulk predicate from boundary world-types via the world-type map violates audit soundness; extra decoding bits are selectors unless internalized. (3) No total-effective boundary decoder (T48. 3): an internal total-effective reconstruction that decides a nontrivial extensional bulk predicate on a diagonal-capable fragment would violate the Paper 29 barrier—so "holography internal halting oracle. " (4) Taxonomy (T48. 4): any holography claim lands in H0–H4 (categorical bulk, world-type equivalence, surjective encoding, partial, selector-augmented). Mechanized in Lean 4 (HolographyUnderClosure) ; 0 axioms. Trust boundary. This is a closure-theoretic bulk–boundary template, not a proof of AdS/CFT; decoder no-gos assume the Paper 29 barrier package on the stated fragment. Mechanization is nems-lean. See.
Nova Spivack (Sun,) studied this question.