theorem proved term proof

`discrete_ledger_computable`

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

formal statement (Lean)

  74theorem discrete_ledger_computable (t : LedgerTransition) :
  75    ∃ (table : Finset (DiscreteLedgerState × DiscreteLedgerState)),
  76      ∀ (s : DiscreteLedgerState),
  77        ∃ (s' : DiscreteLedgerState), (s, s') ∈ table ∧ t s = s' := by

proof body

Term-mode proof.

  78  use Finset.image (fun s => (s, t s)) Finset.univ
  79  intro s
  80  exact ⟨t s, Finset.mem_image.mpr ⟨s, Finset.mem_univ s, rfl⟩, rfl⟩
  81
  82/-- The number of possible discrete ledger states. -/

depends on (7)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
DiscreteLedgerState in IndisputableMonolith.Information.ChurchTuringPhysicsStructure decl_use
LedgerTransition in IndisputableMonolith.Information.ChurchTuringPhysicsStructure decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use