theorem proved term proof

`ledger_state_space_finite`

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

formal statement (Lean)

  86theorem ledger_state_space_finite :
  87    Fintype.card DiscreteLedgerState = 2 ^ 8 := by

proof body

Term-mode proof.

  88  simp [DiscreteLedgerState, Fintype.card_pi, Fintype.card_fin, Fintype.card_bool]
  89
  90/-! ## III. RS Dynamics are Church-Turing Computable -/
  91
  92/-- Carrier of computation_limits_from_ledger through the chain. -/

used by (1)

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

ic003_certificate in IndisputableMonolith.Information.ChurchTuringPhysicsStructure decl_use

depends on (8)

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
computation_limits_from_ledger in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Computable in IndisputableMonolith.Meta.ConstructiveNote decl_use