structure definition def or abbrev

`RecognitionStructure`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  61structure RecognitionStructure (X : Type*) where
  62  /-- The recognition relation: R x y means "x recognizes y". -/
  63  recognizes : X → X → Prop
  64  /-- At least one thing can recognize itself (closure). -/
  65  has_self_recognition : ∃ x, recognizes x x
  66
  67/-- Any recognition structure implies nonemptiness. -/

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
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
recognition_structure_nonempty in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use

depends on (9)

Lean names referenced from this declaration's body.

RecognitionStructure in IndisputableMonolith.Chain decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
RecognitionStructure in IndisputableMonolith.Foundation.RecognitionForcing decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
RecognitionStructure in IndisputableMonolith.Recognition decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
RecognitionStructure in IndisputableMonolith.RRF.Core.Recognition decl_use
recognize in IndisputableMonolith.RRF.Foundation.Consciousness decl_use