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)
133def past (states : ℕ → LedgerSnapshot) (now : ℕ) : Set LedgerSnapshot :=
proof body
Definition body.
134 { s | ∃ n, n < now ∧ states n = s }
135
136/-- The future is the set of uncommitted entries (later ticks). -/
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
-
PredictabilityThreshold
in IndisputableMonolith.Climate.PredictabilityFromJCost
decl_use
-
dark_energy_w
in IndisputableMonolith.Cosmology.CosmologicalConstant
decl_use
-
future
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
past_is_fixed
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
present
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
enhancement_unbounded
in IndisputableMonolith.Gravity.ILGAsymptoticEnhancement
decl_use
-
ProofState
in IndisputableMonolith.RRF.Foundation.Consciousness
decl_use
-
TimeArrow
in IndisputableMonolith.RRF.Foundation.Consciousness
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
future
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
LedgerSnapshot
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use