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)
167structure TimeArrow where
168 /-- Verified propositions grow monotonically. -/
169 past_only_grows : ∀ s₁ s₂ : ProofState,
170 -- If s₂ is "after" s₁, then s₁.verified ⊆ s₂.verified
171 s₁.verified ⊆ s₂.verified
172 /-- Unverified propositions shrink (or new ones appear). -/
173 future_evolves : True
174
175/-- The present is the boundary between past and future. -/
depends on (10)
Lean names referenced from this declaration's body.
-
or
in IndisputableMonolith.Constants.EulerMascheroni
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
future
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
past
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
present
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
ProofState
in IndisputableMonolith.RRF.Foundation.Consciousness
decl_use