pith. sign in
def

experimentalTests

definition
show as:
module
IndisputableMonolith.Quantum.EntanglementEntropy
domain
Quantum
line
211 · github
papers citing
none yet

plain-language theorem explainer

This definition enumerates four empirical tests for the Ryu-Takayanagi formula derived from Recognition Science ledger projections. Quantum gravity and holography researchers would cite it when mapping ledger entropy to black-hole thermodynamics and tensor-network observations. The body is a direct list construction with no lemmas or reductions.

Claim. The experimental tests for the entanglement entropy equaling geometric area are: black hole entropy equals area over 4 in Planck units, tensor networks obey an area law, AdS/CFT calculations reproduce the Ryu-Takayanagi formula, and quantum entanglement experiments confirm the relation.

background

The module QG-008 derives the Ryu-Takayanagi formula S_A = Area(γ_A)/(4 G_N ℏ) from Recognition Science ledger structure. Ledger entries are 2D surfaces; shared entries between a region and its complement count as boundary area, so entanglement entropy scales with area rather than volume. Upstream, InitialCondition.entropy defines entropy as total defect with zero defect as the minimum state, while LedgerFactorization.of calibrates the J-cost on the positive reals.

proof idea

This is a direct definition that hardcodes the four-item list of test descriptions. No lemmas are applied and no tactics are used; the body simply returns the string array matching the doc-comment avenues.

why it matters

The definition supplies the experimental checklist for the entanglement-area relation and is referenced by the experimentalTests declarations in ThreeGenerations, NonlocalityNoSignaling, and StrongCP. It completes the QG-008 target of obtaining the Ryu-Takayanagi formula from ledger projection, reinforcing the holographic principle and the black-hole information paradox within the Recognition framework.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.