The Spectre Knot the proofPictures and ideas →
Draft proof, not peer reviewed. What has been checked

lean/Axioms.lean

128 lines · no declarations · on GitHub ·

Prints the axioms each main theorem depends on. build.sh fails unless they are among Lean's standard three (propext, Classical.choice, Quot.sound): no sorryAx, no Lean.ofReduceBool (which native_decide would add); and unless every #print axioms below has printed its answer. At the end, each main theorem is pinned to its claim in Statement.lean.

← SpectreKnot/Statement.leanSpectreKnot/ProofA.lean →

All 39 files, and the declarations of this one
1/-
2Prints the axioms each main theorem depends on. `build.sh` fails unless they are among Lean's standard three
3(`propext`, `Classical.choice`, `Quot.sound`): no `sorryAx`, no `Lean.ofReduceBool` (which `native_decide` would add);
4and unless every `#print axioms` below has printed its answer. At the end, each main theorem is pinned to its claim in
5`Statement.lean`.
6-/
8
9open SpectreKnot
11-- §3: strands (Lemma 3.4); §4: the box of a patch with the signature (Lemma 4.1), and a tile has the signature
12-- (Lemma 4.4)
16-- The pilot's model of the tile, its 14 pieces as a pairing of its 28 ports (`Box.lean`, not used by the main results)
17#print axioms tileBox_proper
18#print axioms tile_signature
19-- §5: the Zigzag Lemma (Lemma 5.1), for every length
20#print axioms Zigzag.zigzag
21-- §6: side lengths (Prop 6.1, Prop 6.2, Cor 6.3, Lemma 6.4, Lemma 6.5), and Prop 6.1 for the supertiles themselves
23#print axioms letterLen_fib
24#print axioms letterLen_parity
25#print axioms sideLen_parity
26#print axioms dOff_fib
27#print axioms bounds
29-- §7: Computation 7.3, the 18 compositions at the level-1 lengths, from the tables alone, as the kernel checks it and
30-- as the paper words it; negative control
33#print axioms Compose.sig_base
34#print axioms Compose.comp_7_3
36-- §7: the lengthening (Lemma 7.1): a move is a cut, and a cut keeps the signature, the new path by the Zigzag Lemma
37-- with n = 3 (`cross_three`), the new ports by the old ones (`Cut.OK.noLoops`)
38#print axioms Gluing.cross_three
39#print axioms Gluing.Cut.OK.sim
41#print axioms Gluing.Cut.OK.sig
42#print axioms Gluing.Equiv.sig
45-- §7: reachability (Lemma 7.2, an induction principle), and Prop 7.4 (Computation 7.3 at every level m ≥ 1), as the
46-- induction uses it and as the paper words it
47#print axioms Compose.adm_level
48#print axioms Compose.adm_induct
49#print axioms Compose.adm_sig
54#print axioms Compose.prop_7_4
55-- Theorem A (the statement file's `TheoremA`): Thm 7.6 at tile level, by induction from the level-1 clusters
56-- (Computation 7.5), the parent's corners where Table 3 puts its Γ child's; and the corner A of a supertile is that of
57-- its Γ child (§2.3)
58#print axioms Statement.good_one
62#print axioms Statement.own_rot
63#print axioms Statement.aPos_succ
64#print axioms Statement.good
66#print axioms Statement.theoremA
69-- Theorem B (the statement file's `TheoremB`, `TheoremB_sharp`): the junction map (Computation 9.2, Lemma 9.3) at every
70-- level, then the nest
71#print axioms Statement.step_base
76#print axioms Statement.step_tile
79#print axioms Statement.chain_odd
82#print axioms Statement.theoremB
83-- The bound is exact (the statement file's `TheoremB_exact`, the last two rows of Table 5): hooks at different
84-- vertices lie on different strands, and each of the two strands is reached
88-- The Grandparent Lemma (the statement file's `Grandparent`, Lemma 8.3(a) at tile vertices): every supertile is a disc
89-- at its rim, and the tables make every vertex of N_b surrounded in N_{b+2}; negative control
97-- The Signature Theorem (the statement file's `SignatureTheorem`, Thm 7.6): the conclusion of the induction, with the
98-- corners written out (Lemma 6.4), and every supertile a disc at its rim
101-- Theorem B, final form (the statement file's `NestModel`, `TheoremB_strand`): the nest tiling as one patch, and
102-- Lemma 3.4 applied to it
106#print axioms Statement.all_same
108-- Theorem A in strand form (the statement file's `ChainModel`, `TheoremA_strand`): the union of any chain of
109-- supertiles that covers, and Lemma 3.4 applied to it; and a chain that covers exists (`NestCovers`)
116/-! The main theorems prove exactly the claims of `Statement.lean`: each `example` states one claim, as written there,
117and gives the main theorem as its proof, so this file fails to build if a main theorem's statement is changed. -/

← SpectreKnot/Statement.leanSpectreKnot/ProofA.lean →