theorem
proved
hard_problem_dissolution_consistent
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 212.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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