# Tilings of an equilateral triangle by five lattice trapezoids (OEIS A391498)

Note, source code and data. Author: Gonzalo Barría (ORCID 0009-0003-8878-737X).

## The note (LaTeX sources in this folder)

- `main.tex` — main source. It includes `completeness_k3k4.tex` (Sections 2–6) and
  `counting.tex` (the counting section), and uses `tipos_13.png` (Figure 1).
- Build: `pdflatex main.tex`, run twice. No bibliography tool is needed.
- `nota_completitud.pdf` — a compiled copy of the note, for reference only.

## `code/` — programs and data (Python 3.12 + sympy; C with gcc)

Everything is in one folder and the scripts read their data from the current
directory, so run them from inside `code/`.

**Independent enumeration (uses no structural information)**
- `brute.py k n1 n2`, `brute.c` (`gcc -O2 -o brute brute.c; ./brute K n1 n2`): exact cover
  of the triangle of side n by k lattice trapezoids with 60° base angles, in all six
  orientations, with pairwise distinct shapes. It gives floor((n-1)(n-2)/6) for k = 3,
  A389392 for k = 4, and A391498 for k = 5 (checked up to n = 22, `brute_15_22.log`).
- `rodrigo.py n1 n2`: transcription of J. Rodrigo's program for the eight categories
  (https://oeis.org/A391498/a391498_3.txt).
- `cats.c` (`gcc -O2 -o cats cats.c; ./cats n1 n2`): C port of the eight categories; it
  extends A391498 to n = 127 (`cats_1_47.txt`, `cats_1_127.txt`).
- `compare.py`, `check_example.py`: set-by-set comparison with the enumeration, and the
  erratum in the n = 7 examples of the OEIS entry (category CC3).

**Classification (Sections 2–9)**
- `classify.py n1 n2`: canonical codes of combinatorial types (`types_6_13.pkl`).
- `verify_structure.py k n1 n2`: checks the lemmas of the note on every tiling found by
  the enumeration (k = 3, n ≤ 16; k = 4, n ≤ 15; k = 5, n ≤ 15); it finds 1, 2 and 13 types.
- `signatures.py n`, `types_table.py`, `describe_types.py`, `draw_types.py`,
  `type_vs_cat.py`: tables, descriptions, the figure `tipos_13.png`, and the comparison
  with Rodrigo's eight categories.

**Counting (Section 11)**
- `from_types.py N`: a(n) generated only from the shape formulas of the thirteen types.
- `families.c` (`./families nmax`), `families_tup.c`, `families.py N`: the eight families,
  their overlaps and fibres (`fam_1_63.txt`, `fam_tup.txt`).
- `fit_families.py`, `gf_record.py`: rational generating functions of the twelve pieces
  (`gf_familias.txt`, `gf_familias.json`).
- `lemmas.py`, `collisions.py`, `excess.py`, `dident.py`, `loci3.py`, `verify_loci.py`,
  `pieces.py`, `close_df.py`, `close_sf.py`, `close_more.py`, `close_final.py`,
  `layer2.py`: closed formulas for the pieces and the loci of identification and
  intersection, each checked against the data.
- `formula.py`: the closed formula for a(n); `python3 formula.py` compares it with
  A391498 for n = 1..127.
- `verify_formula_200.py`: agreement with the conjectured generating function up to
  n = 200, and the degree of D(x)·A(x).
- `guess.py`, `reduce.py`, `test_gf.py`, `quasipoly.py`: the generating function guessed
  from the 47 terms of the OEIS entry, and the quasi-polynomial of period 60.

**Data files**: `cats_*.txt`, `fam_*.txt`, `out_types.txt`, `brute_15_22.log`,
`gf_familias.*`, and the `.pkl` result files written by the scripts above.

## What is computer-assisted

The proofs of the structure theorems (k = 3, 4, 5) are by hand; the programs check them.
For the counting theorem, the shape formulas of the eight families come from the
classification, while the facts that only D, S and F overlap (checked for n ≤ 63) and that
the lists of loci are complete (solving the 120 linear systems attached to the
permutations of the five parts, `loci3.py`) were obtained by computation, as stated in
the remark that follows the main counting theorem of the note.