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)
26def legalTriad (t : Triad) : Bool :=
proof body
Definition body.
27 let s := t.h + t.k + t.l
28 (s % 2 = 0) && (t.h ≠ 0 ∨ t.k ≠ 0 ∨ t.l ≠ 0)
29
30/‑ Eight-window neutrality diagnostic over a sequence of motif weights. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
countLegal
in IndisputableMonolith.Crystallography.SelectionRules
decl_use
depends on (6)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Triad
in IndisputableMonolith.Crystallography.SelectionRules
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use