pith. machine review for the scientific record. sign in
theorem proved tactic proof

bh_entropy_from_ledger

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)

  41theorem bh_entropy_from_ledger (Rs : ℝ) (h_Rs : Rs > 0) :
  42    let A := HorizonArea Rs

proof body

Tactic-mode proof.

  43    let S_BH := A / (4 * tau0^2 * c^2) -- Standard form using ell0 = c*tau0
  44    ∃ (N : ℝ), N = LedgerCapacityLimit A ell0 ∧ S_BH = N / 4 := by
  45  intro A S_BH
  46  use LedgerCapacityLimit A ell0
  47  constructor
  48  · rfl
  49  · unfold S_BH LedgerCapacityLimit
  50    rw [← c_ell0_tau0]
  51    ring_nf
  52
  53/--- **CERT(definitional)**: Characterization of the event horizon by maximum possible recognition flux. -/

depends on (16)

Lean names referenced from this declaration's body.