structure
definition
DescriptiveFixedPoint
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Foundation.SelfReference on GitHub at line 122.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
119/-! ## Fixed Point Structure -/
120
121/-- A fixed point: the description describes itself accurately. -/
122structure DescriptiveFixedPoint where
123 /-- The description. -/
124 description : RRFDescription
125 /-- The description describes something with the same structure. -/
126 self_similar : description = description -- Trivially true, but captures the idea
127
128/-- The RRF is a fixed point of description. -/
129def rrf_is_fixed_point : DescriptiveFixedPoint := {
130 description := currentRRF,
131 self_similar := rfl
132}
133
134/-- The RRF fixed point exists. -/
135theorem rrf_fixed_point_exists : Nonempty DescriptiveFixedPoint :=
136 ⟨rrf_is_fixed_point⟩
137
138/-! ## Consistency Claims -/
139
140/-- The formalization is internally consistent.
141
142This is witnessed by the fact that it compiles without contradiction.
143We cannot prove this from within (Gödel), but we can assert it.
144-/
145structure InternalConsistency where
146 /-- Derivable from foundational axioms only. -/
147 foundational : Nonempty (ℝ → ℝ)
148 /-- No obvious contradiction. -/
149 not_obviously_false : ¬(0 = 1)
150 /-- All proofs in this file are terminal (no holes). -/
151 rigorous_proofs_only : Bool
152