theorem
proved
topologicalDefect_count
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.TopologicalDefectsFromRS on GitHub at line 25.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
22 | texture
23 deriving DecidableEq, Repr, BEq, Fintype
24
25theorem topologicalDefect_count : Fintype.card TopologicalDefect = 4 := by decide
26
27/-- 4 = 2² = 2^(D-1) at D = 3. -/
28theorem four_eq_2pow_Dm1 : (4 : ℕ) = 2 ^ 2 := by decide
29
30structure TopologicalDefectCert where
31 four_defects : Fintype.card TopologicalDefect = 4
32 four_as_2pow : (4 : ℕ) = 2 ^ 2
33
34def topologicalDefectCert : TopologicalDefectCert where
35 four_defects := topologicalDefect_count
36 four_as_2pow := four_eq_2pow_Dm1
37
38end IndisputableMonolith.Physics.TopologicalDefectsFromRS