SeedExamples.lean

1 import PaperX.SeedCertificates
2 import PaperX.SeedBoundary
3 
4 /-!
5 A new explicit seven-root transport model matching the manuscript's component
6 pattern. This is not presented as a rerun of the unretrieved companion script.
7 -/
8 set_option autoImplicit false
9 set_option maxRecDepth 4096
10 set_option maxHeartbeats 2000000
11 namespace PaperX.SeedExamples
12 
13 open PaperX.DirectedSeeds PaperX.SeedCertificates
14 
15 def edges : Finset (Fin 7 × Fin 7) :=
16   {(0,1),(1,0),(1,2),(2,5),(3,4),(4,3),(4,5),(6,5)}
17 
18 def edge (a b : Fin 7) : Prop := (a,b) ∈ edges
19 
20 instance edgeDecidable : DecidableRel edge := fun _ _ => inferInstanceAs (Decidable (_ ∈ edges))
21 
22 theorem closure_closed : ClosedAt edge 3 := by decide +kernel
23 
24 theorem reach_iff (a b : Fin 7) : Reach edge a b ↔ b ∈ reachableWithin edge 3 a :=
25   reach_iff_certificate edge 3 closure_closed a b
26 
27 def label : Fin 7 → Fin 5 := ![0,0,1,2,2,3,4]
28 
29 def rep : Fin 5 → Fin 7 := ![0,2,3,5,6]
30 
31 theorem label_rep : ∀ k, label (rep k) = k := by decide
32 
33 theorem label_law : ∀ a b, label a = label b ↔ Reach edge a b ∧ Reach edge b a := by
34   simp only [reach_iff]
35   decide +kernel
36 
37 noncomputable def componentEquiv : Component edge ≃ Fin 5 :=
38   componentEquivOfLabels edge label rep label_rep label_law
39 
40 theorem component_count : Nat.card (Component edge) = 5 := by
41   rw [Nat.card_congr componentEquiv]
42   simp
43 
44 def sourceLabel (k : Fin 5) : Prop := k = 0 ∨ k = 2 ∨ k = 4
45 
46 instance sourceLabelDecidable : DecidablePred sourceLabel :=
47   fun _ => inferInstanceAs (Decidable (_ = 0 ∨ _ = 2 ∨ _ = 4))
48 
49 theorem source_label_iff (k : Fin 5) :
50     IsSource edge (component edge (rep k)) ↔ sourceLabel k := by
51   rw [source_iff]
52   simp only [reach_iff]
53   revert k
54   decide +kernel
55 
56 noncomputable def sourceEquiv : Source edge ≃ {k : Fin 5 // sourceLabel k} :=
57   componentEquiv.subtypeEquiv (fun c => by
58     have h := source_label_iff (componentEquiv c)
59     have heq : component edge (rep (componentEquiv c)) = c := componentEquiv.left_inv c
60     rw [heq] at h
61     exact h)
62 
63 theorem source_count : Nat.card (Source edge) = 3 := by
64   rw [Nat.card_congr sourceEquiv, Nat.card_eq_fintype_card]
65   decide
66 
67 theorem rank_three : seedRank edge = 3 := by
68   rw [directed_minimum_seed, source_count]
69 
70 def chosenSeeds : Finset (Fin 7) := {0,3,6}
71 
72 theorem chosenSeeds_cover : Covers edge chosenSeeds := by
73   apply (certifiedCover_iff edge 3 closure_closed _).1
74   decide +kernel
75 
76 theorem chosenSeeds_optimal (S : Finset (Fin 7)) (hS : Covers edge S) :
77     chosenSeeds.card ≤ S.card := by
78   have h := seedRank_le edge S hS
79   rw [rank_three] at h
80   exact h
81 
82 /-- All minima in the explicit example, computed from a certified path closure. -/
83 def minimumSeedSets : Finset (Finset (Fin 7)) :=
84   Finset.univ.powerset.filter (fun S => S.card = 3 ∧ certifiedCover edge 3 S)
85 
86 theorem minimumSeedSets_iff (S : Finset (Fin 7)) :
87     S ∈ minimumSeedSets ↔ Covers edge S ∧ S.card = seedRank edge := by
88   simp only [minimumSeedSets, Finset.mem_filter, Finset.mem_powerset,
89     Finset.subset_univ, true_and, certifiedCover_iff edge 3 closure_closed,
90     rank_three, and_comm]
91 
92 theorem minimumSeedSets_exact : minimumSeedSets =
93     {{0,3,6},{0,4,6},{1,3,6},{1,4,6}} := by decide +kernel
94 
95 theorem four_minimum_sets : minimumSeedSets.card = 4 := by
96   rw [minimumSeedSets_exact]
97   decide
98 
99 /-- Removing the seed for G fails, despite the downstream meeting at F. -/
100 theorem two_seeds_do_not_cover : ¬ Covers edge {0,3} := by
101   rw [← certifiedCover_iff edge 3 closure_closed]
102   decide +kernel
103 
104 /-- The empty graph is included, with rank zero rather than a forced seed. -/
105 theorem empty_graph_rank : seedRank (fun _ _ : Fin 0 => False) = 0 :=
106   (PaperX.SeedConsequences.rank_zero_iff _).2 inferInstance
107 
108 end PaperX.SeedExamples

Back to source controls