1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
//! Tiling classification: screen enumerated cyclotomic tiles into the
//! buckets *cannot tile* / *tiles periodically* / *undecided candidate* (the
//! aperiodic-monotile / spectre-sibling hunt), via sound one-sided tests that
//! engage the real global geometry.
//!
//! Two complementary sound verdicts:
//!
//! - [`heesch`] -- the **Heesch-number reject**: how many coronas can fully
//! surround the tile (rotations only)? A *finite* Heesch number is a sound
//! proof the tile cannot tile; Heesch 0 (cannot be surrounded even once) is
//! the cheapest, highest-yield reject -- just the `bound = 1` case.
//!
//! - the sound **periodicity acceptance**: where finite Heesch proves a tile
//! cannot tile, these prove it *does* tile periodically (disqualifying it as
//! an aperiodic monotile). [`cascade::certify_periodic`] runs a cheap-first
//! cascade of constructively-verified detectors -- [`conway::conway_criterion`]
//! (p1/p2), [`torus::tiles_torus`] (patch-derived k-tile domains), the
//! [`aniso`] cluster and [`isohedral`] (p3/p4/p6) searches -- with
//! [`WithAdjacency`](crate::geom::patch::WithAdjacency) carrying the tile
//! adjacency the [`mint`] carve reads to
//! cut a translation cell, [`grow`] building the
//! lattice-exposing corona patches, the shared plane-lattice primitives in
//! `lattice`, and every positive gated by the exact verification in
//! [`tiling`] -- [`mint`]ing a provenance-tagged [`cert`]ificate a verifier
//! can replay.
//!
//! Both verdicts fire only *positively* and soundly: neither can decide tiling
//! in general (the domino problem is undecidable), so a tile that is neither
//! rejected nor accepted stays an undecided candidate.
//!
//! # Scope of the certified claims
//!
//! All verdicts are relative to SINGLE-CHIRALITY, EDGE-TO-EDGE tilings: copies
//! are rotated by ring units (multiples of one turn / `T::turn()`), never
//! reflected, and adjacent copies share complete unit edges.
//!
//! - **Rotations**: no loss of generality within edge-to-edge tilings. An
//! edge-overlapping contact forces the two edge directions to coincide, and
//! every edge direction of a rat is a ring unit, so along the (connected)
//! edge-contact graph of a tiling every copy is rotated by a ring unit.
//! - **Reflections**: excluded BY CHOICE -- this is the chiral
//! aperiodic-monotile hunt (the spectre family tiles without its mirror
//! image; admitting reflections would be a different question).
//! - **Edge-to-edge**: the SEARCH only ever generates full unit-edge
//! contacts, and `Z[zeta_12]` is dense, so brick-wall-style slides exist in
//! principle (translating a neighbour by e.g. `2 - sqrt(3)` along a shared
//! edge line produces T-vertices -- a corner resting on the interior of
//! another tile's edge). This is NOT a gap in the cannot-tile claims: by
//! the edge-to-edge reduction theorem (`docs/math/edge-to-edge-reduction.md`),
//! any single-chirality tiling of the plane by a unit-edge polygon can be
//! realigned, strip by strip along its parallel slid fault lines, into an
//! edge-to-edge tiling. Hence "no edge-to-edge tiling" (what a
//! [`cert::HeeschCert`] with `Finite` status establishes) already implies
//! "no single-chirality tiling at all". Periodic ACCEPTS never needed the
//! reduction: a verified cert exhibits a concrete tiling.
pub
/// Debug-trace toggles, each read from its env var ONCE per process (the
/// searches consult these in inner paths; a fresh `env::var` per call is
/// wasted work and clutter).
pub