theorem proved term proof

`current_understanding_consistent`

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

formal statement (Lean)

 258theorem current_understanding_consistent :
 259    -- String theory, AdS/CFT, and recent calculations support information preservation
 260    -- Page curve has been derived in various models
 261    -- No evidence for firewalls
 262    True := trivial

proof body

Term-mode proof.

 263
 264end BlackHoleInformation
 265end Quantum
 266end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
evidence in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use