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)
41abbrev RecognitionStructure := Recognition.RecognitionStructure
proof body
Definition body.
42
43/-- Re-export: Chain of recognition steps. -/
used by (29)
From the project-wide theorem graph. These declarations reference this one in their body.
-
AtomicTick
in IndisputableMonolith.Chain
decl_use
-
Chain
in IndisputableMonolith.Chain
decl_use
-
Ledger
in IndisputableMonolith.Chain
decl_use
-
RecognitionStructure
in IndisputableMonolith.Chain
decl_use
-
cost_to_recognition_bridge
in IndisputableMonolith.Foundation.RecognitionForcing
decl_use
-
recognition_forcing_complete
in IndisputableMonolith.Foundation.RecognitionForcing
decl_use
-
recognition_from_extraction
in IndisputableMonolith.Foundation.RecognitionForcing
decl_use
-
RecognitionStructure
in IndisputableMonolith.Foundation.RecognitionForcing
decl_use
-
recognition_unique
in IndisputableMonolith.Foundation.RecognitionForcing
decl_use
-
AccountRS
in IndisputableMonolith.LedgerPostingAdjacency
decl_use
-
Reaches
in IndisputableMonolith.LedgerUniqueness
decl_use
-
Kin
in IndisputableMonolith.Potential
decl_use
-
Pot
in IndisputableMonolith.Potential
decl_use
-
AtomicTick
in IndisputableMonolith.Recognition
decl_use
-
Chain
in IndisputableMonolith.Recognition
decl_use
-
Ledger
in IndisputableMonolith.Recognition
decl_use
-
Ledger
in IndisputableMonolith.Recognition
decl_use
-
M
in IndisputableMonolith.Recognition
decl_use
-
RecognitionStructure
in IndisputableMonolith.Recognition
decl_use
-
M
in IndisputableMonolith.Recognition.Cycle3
decl_use
-
SimpleStructure
in IndisputableMonolith.Recognition.ModelingExamples
decl_use
-
chainFlux
in IndisputableMonolith.RRF.Core.Recognition
decl_use
-
chainFlux_zero_of_balanced
in IndisputableMonolith.RRF.Core.Recognition
decl_use
-
phi
in IndisputableMonolith.RRF.Core.Recognition
decl_use
-
T2_atomicity
in IndisputableMonolith.RRF.Core.Recognition
decl_use
-
DerivationChain
in IndisputableMonolith.RRF.Foundation.MetaPrinciple
decl_use
-
MPForcesLedger
in IndisputableMonolith.RRF.Foundation.MetaPrinciple
decl_use
-
RecognitionStructure
in IndisputableMonolith.RRF.Foundation.MetaPrinciple
decl_use
-
recognition_structure_nonempty
in IndisputableMonolith.RRF.Foundation.MetaPrinciple
decl_use
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Chain
in IndisputableMonolith.Chain
decl_use
-
RecognitionStructure
in IndisputableMonolith.Chain
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
RecognitionStructure
in IndisputableMonolith.Foundation.RecognitionForcing
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
Chain
in IndisputableMonolith.Recognition
decl_use
-
RecognitionStructure
in IndisputableMonolith.Recognition
decl_use
-
Chain
in IndisputableMonolith.RRF.Core.Recognition
decl_use
-
RecognitionStructure
in IndisputableMonolith.RRF.Foundation.MetaPrinciple
decl_use