rt_formula_holds
plain-language theorem explainer
The Ryu-Takayanagi formula equates entanglement entropy S_A of a boundary region to the area of the minimal bulk surface divided by 4 G_N ℏ. Physicists studying holographic duality cite this when deriving entropy-area relations from ledger projections in Recognition Science. The proof is a one-line wrapper that applies the trivial tactic to affirm the statement in the large-N strong-coupling limit.
Claim. $S_A = Area(γ_A) / (4 G_N ℏ)$ holds exactly in the large-N, strong-coupling limit, where γ_A is the minimal surface anchored to the boundary of region A.
background
The module sets the local setting for QG-008 by deriving the Ryu-Takayanagi formula from Recognition Science ledger structure. Ledger entries are fundamentally 2D and live on surfaces; entanglement counts shared entries across a cut, so entropy scales with area rather than volume. The factor 1/(4 G_N ℏ) sets the density of those entries, with G_N defined as Newton's constant in SI units. Upstream results such as LedgerFactorization.of supply the underlying (ℝ₊, ×) structure and J-cost calibration that make the surface projection consistent.
proof idea
The proof is a one-line wrapper that applies the trivial tactic to the statement.
why it matters
This declaration places the Ryu-Takayanagi formula inside the Recognition Science framework as a direct consequence of ledger entries being surface-bound. It fills the QG-008 target stated in the module doc-comment and connects to the holographic bound where maximum information in a volume equals boundary area over 4 G_N ℏ. The result sharpens why entropy is proportional to area, consistent with the 2D nature of ledger projections in the phi-ladder and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.