pith. machine review for the scientific record. sign in
inductive definition def or abbrev

Resolution

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  75inductive Resolution
  76| Firewall          -- High-energy particles at horizon
  77| Complementarity   -- No single observer sees contradiction
  78| ERisEPR           -- Entanglement = wormholes
  79| Fuzzball          -- Stringy structure, no interior
  80| RS_Ledger         -- Ledger non-locality
  81deriving Repr, DecidableEq
  82
  83/-! ## RS Resolution: Ledger Non-Locality -/
  84
  85/-- In Recognition Science, the resolution is ledger non-locality:
  86
  87    The ledger is NOT local. It spans the horizon naturally.
  88
  89    **Key insight**: Entanglement = shared ledger entries.
  90
  91    For Hawking pairs:
  92    - Pair A and B share ledger entries across horizon
  93    - Early radiation shares ledger with late via the BLACK HOLE
  94    - Monogamy is preserved because it's ONE ledger, not two copies -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (12)

Lean names referenced from this declaration's body.