No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
195structure SelfReferenceComplete where
196 /-- The Meta-RRF exists. -/
197 meta_rrf : MetaRRF
198 /-- It's a fixed point. -/
199 is_fixed_point : DescriptiveFixedPoint
200 /-- It's internally consistent. -/
201 is_consistent : InternalConsistency
202 /-- Compilation is recognition. -/
203 compilation_is_recognition : CompilationAsRecognition
204
205/-- The self-reference structure is complete. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
complete
in IndisputableMonolith.Complexity.SAT.Backprop
decl_use
-
consistent
in IndisputableMonolith.Complexity.SAT.Backprop
decl_use
-
RRF
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
point
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
self
in IndisputableMonolith.RecogSpec.Core
decl_use
-
CompilationAsRecognition
in IndisputableMonolith.RRF.Foundation.SelfReference
decl_use
-
DescriptiveFixedPoint
in IndisputableMonolith.RRF.Foundation.SelfReference
decl_use
-
InternalConsistency
in IndisputableMonolith.RRF.Foundation.SelfReference
decl_use
-
MetaRRF
in IndisputableMonolith.RRF.Foundation.SelfReference
decl_use