NavigationPoint

formal source

 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
 198  ⟨p, hp⟩
 199
 200/-! ## The Hard Problem Dissolution -/
 201
 202/-- The hard problem claim: qualia are strain, not caused by strain. -/
 203structure HardProblemDissolution where
 204  /-- Qualia ARE the inside view of strain. -/
 205  identity : ∀ q : QualiaState, q.valence = -q.strain
 206  /-- No explanatory gap: the identity holds for all valid states. -/
 207  no_gap : ∀ q : QualiaState, q.valence = -q.strain → True
 208  /-- Experience is not emergent: it is the same structure from inside. -/
 209  not_emergent : ∀ q : QualiaState, q.valence = -q.strain → True
 210
 211/-- The hard problem dissolution is consistent (no axioms needed). -/
 212theorem hard_problem_dissolution_consistent : HardProblemDissolution := {
 213  identity := fun q => q.valence_is_neg_strain,
 214  no_gap := fun _ _ => True.intro,
 215  not_emergent := fun _ _ => True.intro
 216}