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)
175structure DerivationChain where
176 /-- Starting point: a recognition structure exists. -/
177 has_recognition : ∃ (X : Type), Nonempty (RecognitionStructure X)
178 /-- Step 1: Recognition forces ledger (modeled by MPForcesLedger). -/
179 forces_ledger : True
180 /-- Step 2: Ledger + self-similarity forces φ (proved by self_similarity_forces_phi). -/
181 forces_phi : True
182
183/-- The derivation chain is consistent. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (15)
Lean names referenced from this declaration's body.
-
RecognitionStructure
in IndisputableMonolith.Chain
decl_use
-
consistent
in IndisputableMonolith.Complexity.SAT.Backprop
decl_use
-
forces
in IndisputableMonolith.Foundation.MagnitudeOfMismatch
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
RecognitionStructure
in IndisputableMonolith.Foundation.RecognitionForcing
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
-
RecognitionStructure
in IndisputableMonolith.Recognition
decl_use
-
self
in IndisputableMonolith.RecogSpec.Core
decl_use
-
RecognitionStructure
in IndisputableMonolith.RRF.Core.Recognition
decl_use
-
MPForcesLedger
in IndisputableMonolith.RRF.Foundation.MetaPrinciple
decl_use
-
RecognitionStructure
in IndisputableMonolith.RRF.Foundation.MetaPrinciple
decl_use
-
self_similarity_forces_phi
in IndisputableMonolith.RRF.Foundation.MetaPrinciple
decl_use