Registry · Definition IV.D394 tau-effective not_applicable

IV.D394 — CheckCrystal Decision Procedure

CheckCrystal(c,K) = true iff ∃p≤K: NF^p(c)=c. Periodic NF orbit ↔ crystalline order. Total on finite NF codes.

Book IV Part 7 Ch. 62

Dependency Graph

Depended on by (1)

IV.P233

Lean Formalization

Module: TauLib.BookIV.ManyBody.CondensedMatter