BoundaryRegion
plain-language theorem explainer
BoundaryRegion is a structure that packages a positive real size for a boundary region in a holographic CFT. Holographic entropy calculations in Recognition Science cite it as the typed input to minimal-surface and Ryu-Takayanagi constructions. The definition is a direct record with a size field and an explicit positivity constraint.
Claim. A boundary region $A$ consists of a positive real number $s>0$ that records its linear size.
background
The module derives the Ryu-Takayanagi formula from Recognition Science ledger structure. Ledger entries are two-dimensional surfaces, so shared entries between a region and its complement count as area rather than volume; the formula therefore reads $S_A = $ Area($γ_A$) / (4 $G_N$ ℏ). BoundaryRegion supplies the minimal data needed for that counting: a positive size on the boundary. Upstream structures include ledger factorization of the positive reals and the active-edge count $A$ at $D=3$.
proof idea
The declaration is a direct structure definition. It introduces the size field together with the size_pos hypothesis and performs no further reduction or lemma application.
why it matters
BoundaryRegion supplies the typed argument to minimalSurfaceArea and ryuTakayanagi, which realize the RT formula inside the QG-008 target. It anchors the holographic entropy claim to the ledger-projection insight that entries live on surfaces. The parent results are the RT formula itself and the constants $G_N$, ℏ drawn from the Constants module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.