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)
31structure RecognitionStructure where
32 U : Type
33 R : U → U → Prop
34
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
-
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
-
RecognitionStructure
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 (6)
Lean names referenced from this declaration's body.