structure
definition
TimeArrow
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Foundation.Consciousness on GitHub at line 167.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
164/-! ## The Arrow of Time -/
165
166/-- Time flows from unverified to verified. -/
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. -/
176def present_is_boundary (s : ProofState) : Prop :=
177 s.current ∉ s.verified ∧ s.current ∉ s.unverified
178
179/-- Every valid ProofState has present as boundary. -/
180theorem proofstate_has_boundary (s : ProofState) : present_is_boundary s :=
181 ⟨s.current_not_in_past, s.current_not_in_future⟩
182
183/-! ## Navigation Points -/
184
185/-- A navigation point: where computation cannot locally close. -/
186structure NavigationPoint where
187 /-- The state where closure fails. -/
188 state : ProofState
189 /-- Multiple valid next moves exist. -/
190 has_choice : (validMoves state).Nonempty
191 /-- No single move is forced. -/
192 no_unique : ¬∃! p, p ∈ validMoves state
193
194/-- At navigation points, consciousness "chooses". -/
195theorem navigation_requires_choice (n : NavigationPoint) :
196 ∃ p, p ∈ validMoves n.state :=
197 let ⟨p, hp⟩ := free_will_exists n.state n.has_choice