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)
315theorem arrow_of_time :
316 temporal_dim = 1 ∧ eight_tick = 8 ∧ ∀ t : ℕ, t < t + 1 :=
proof body
Term-mode proof.
317 ⟨rfl, rfl, fun _ => Nat.lt_succ_of_le le_rfl⟩
318
319/-! ## §10 Exclusion of Alternative Signatures -/
320
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
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
-
eight_tick
in IndisputableMonolith.Foundation.DimensionForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
arrow_of_time
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
eight_tick
in IndisputableMonolith.Gap45.PhysicalMotivation
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
eight_tick
in IndisputableMonolith.RRF.Foundation.Constants
decl_use
-
eight_tick
in IndisputableMonolith.Thermodynamics.RecognitionThermodynamics
decl_use
-
temporal_dim
in IndisputableMonolith.Unification.SpacetimeEmergence
decl_use