experimentalStatus
plain-language theorem explainer
The declaration defines a list of three experimental statuses affirming the Ryu-Takayanagi area law for entanglement entropy inside the Recognition Science ledger model. A physicist working on holographic duality or quantum gravity would cite the list when summarizing empirical support for the area-law relation. It is assembled as a direct enumeration of string pairs, each pairing a test category with its reported confirmation status.
Claim. The experimental status is the list consisting of the pairs (``BH entropy formula'', ``Confirmed by all calculations''), (``Area law in CFT'', ``Verified in many examples''), and (``Tensor network area law'', ``Confirmed'').
background
The module sets the local theoretical setting for QG-008 by deriving the Ryu-Takayanagi formula from Recognition Science ledger projections: ledger entries are fundamentally 2D, entanglement counts shared entries across a boundary, and the resulting entropy scales with area rather than volume, yielding S_A = Area(γ_A) / (4 G_N ℏ). RTFalsifier is the structure that records a potential falsification type as a String together with its status String. Upstream results include the entropy definition stating that entropy of a configuration is proportional to its total defect (zero defect yields minimum entropy) and several domain-wide lists that supply cross-references for the broader ledger framework.
proof idea
The definition is a direct list literal that constructs three RTFalsifier instances by pairing each falsifier description with its confirmation status. No lemmas or tactics are invoked; the body is a static enumeration of the three pairs.
why it matters
This definition documents empirical alignment for the QG-008 target of obtaining the Ryu-Takayanagi formula from ledger structure, listing confirmations for the black-hole entropy formula, the CFT area law, and tensor-network area laws. It thereby supports the framework claim that entanglement entropy arises from counting 2D ledger entries rather than volume information. With zero downstream uses, the list serves as a standing record of consistency checks rather than feeding a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.