structure
definition
HardProblemDissolution
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 203.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
all -
all -
of -
consistent -
all -
of -
identity -
is -
of -
from -
is -
of -
for -
is -
gap -
of -
gap -
gap -
is -
Qualia -
all -
QualiaState -
identity -
gap
used by
formal source
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}
217
218end RRF.Foundation
219end IndisputableMonolith