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)
66structure DirectedEdge where
67 /-- Source vertex (3-bit binary) -/
68 source : Fin 8
69 /-- Target vertex (3-bit binary) -/
70 target : Fin 8
71 /-- They differ in exactly one coordinate (edge condition) -/
72 adjacent : source ≠ target
73
74/-- The number of undirected edges in Q_D: D · 2^{D-1}. -/
depends on (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
one
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
one
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
one
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
one
in IndisputableMonolith.RecogSpec.Core
decl_use