CompanionForests.lean

1 import PaperXII.ReuseCompactness
2 import Mathlib.Data.Fintype.EquivFin
3 
4 /-! Paper XII 10.3–10.4 and the branch portion of 10.5.
5 The two finite-set compactness primitives are reused from Paper X unchanged.
6 Index 0 is the first residual level. No transition surjectivity is assumed. -/
7 namespace PaperXII.CompanionForests
8 
9 open PaperX.Compactness
10 
11 /-- Ordinary finiteness supplies the exhaustive lists required by the reused proof. -/
12 theorem finiteLevels (T : Tower) [∀ n, Finite (T.Level n)] : FiniteLevels T := by
13   classical
14   intro n
15   let _ := Fintype.ofFinite (T.Level n)
16   exact ⟨Finset.univ.toList, fun x ↦ by simp⟩
17 
18 /-- Claim 10.3 without the unnecessary fixed-root restriction. -/
19 theorem branch_exists (T : Tower) [∀ n, Finite (T.Level n)]
20     (hne : ∀ n, Nonempty (T.Level n)) : Nonempty (Branch T) :=
21   finite_branch_compactness T (finiteLevels T) hne
22 
23 /-- A branch is determined by its values. -/
24 theorem branch_ext {T : Tower} (b c : Branch T)
25     (h : ∀ n, b.value n = c.value n) : b = c := by
26   cases b with
27   | mk bv bh =>
28     cases c with
29     | mk cv ch =>
30       have hv : bv = cv := funext h
31       cases hv
32       rfl
33 
34 /-- Composite reduction from level n to the first residual level. -/
35 def reduceToFirst (T : Tower) : (n : ℕ) → T.Level n → T.Level 0
36   | 0 => id
37   | n + 1 => fun x ↦ reduceToFirst T n (T.parent n x)
38 
39 /-- Every coordinate of a branch reduces to its first value. -/
40 theorem branch_reduces_to_first (T : Tower) (b : Branch T) (n : ℕ) :
41     reduceToFirst T n (b.value n) = b.value 0 := by
42   induction n with
43   | zero => rfl
44   | succ n ih =>
45     change reduceToFirst T n (T.parent n (b.value (n + 1))) = _
46     rw [b.compatible n, ih]
47 
48 /-- Claim 10.3 with the source's fixed residual root retained explicitly. -/
49 theorem rooted_branch_exists (T : Tower) [∀ n, Finite (T.Level n)]
50     (hne : ∀ n, Nonempty (T.Level n)) (root : T.Level 0)
51     (hroot : ∀ n (x : T.Level n), reduceToFirst T n x = root) :
52     ∃ b : Branch T, b.value 0 = root ∧
53       ∀ n, reduceToFirst T n (b.value n) = root := by
54   obtain ⟨b⟩ := branch_exists T hne
55   exact ⟨b, hroot 0 (b.value 0), fun n ↦ hroot n (b.value n)⟩
56 
57 /-- The complete finite-level criterion, in both directions. -/
58 theorem branch_iff_nonempty_levels (T : Tower) [∀ n, Finite (T.Level n)] :
59     Nonempty (Branch T) ↔ ∀ n, Nonempty (T.Level n) :=
60   branch_iff_levels_nonempty T (finiteLevels T)
61 
62 /-- A missing finite level rules out every branch, even without finiteness. -/
63 theorem empty_level_no_branch (T : Tower) (n : ℕ) (h : ¬ Nonempty (T.Level n)) :
64     ¬ Nonempty (Branch T) := empty_level_obstruction T n h
65 
66 /-- Claim 10.4 applies to any complete realization carrying its actual finite reductions. -/
67 theorem empty_level_no_realization (T : Tower) {R : Type*}
68     (reduce : ∀ n, R → T.Level n) (n : ℕ) (h : ¬ Nonempty (T.Level n)) :
69     ¬ Nonempty R := by
70   rintro ⟨r⟩
71   exact h ⟨reduce n r⟩
72 
73 /-- For finite towers, failure of completion has a finite-level witness. -/
74 theorem no_branch_has_empty_level (T : Tower) [∀ n, Finite (T.Level n)]
75     (h : ¬ Nonempty (Branch T)) : ∃ n, ¬ Nonempty (T.Level n) := by
76   exact Classical.not_forall.mp (fun hne ↦ h ((branch_iff_nonempty_levels T).mpr hne))
77 
78 /-- The branch-selection portion of 10.5, with no effectivity conclusion hidden in it. -/
79 theorem simultaneous_branches {I : Type} (T : I → Tower)
80     [∀ i n, Finite ((T i).Level n)]
81     (hne : ∀ i n, Nonempty ((T i).Level n)) : Nonempty (∀ i, Branch (T i)) :=
82   indexed_finite_completion T (fun i ↦ finiteLevels (T i)) hne
83 
84 end PaperXII.CompanionForests

Back to source controls