Product-centered reflection-symmetric equilateral triangles in floretion triangular coordinates
Abstract
Dement has recently studied the unordered triples of order-n floretion base vectors whose tile centroids form a nondegenerate equilateral triangle of the triangular lattice, and has determined in closed form the number of such triangles that are local, that are product-centered and local, and that are symmetric about a main axis of the tiling. Two columns of his table of reflection-symmetric counts are left open: no closed formula is known for the number abs(Aₙ ∩ Pₙ) of axis-symmetric product-centered triangles, nor for its nonlocal part abs(Aₙ ∩ Xₙ ∩ Pₙ), and he obtains both only by exhaustive enumeration through order 6. We give a reduction of the per-axis version of that count from a search over triples, of size Θ(16ⁿ), to a search over one word of {e,i,j,k}ⁿ and one binary word, and use it to push the open column four orders further. We obtain the new values abs(Aₙ ∩ Pₙ)=16218, 49930, 152346 at n=8,9,10, and we find that on each single axis the count is abs(Aₙ(τ) ∩ Pₙ)=8 · 3ⁿ⁻²-2ⁿ at every order n ≥ 2 we can reach, so that abs(Aₙ ∩ Pₙ)=8 · 3ⁿ⁻¹-5 · 2ⁿ+2 for 2 ≤ n ≤ 10. We emphasise that this closed form is verified, not proved: it is a conjecture with a ten-order audit. Two structural consequences are recorded. First, the Fibonacci numbers that appear in the conjectured nonlocal column are an artifact of subtracting Dement's local term: the per-axis product-centered count is Fibonacci-free, and it is therefore the object to attack. Second, the two integer equations that define the reduced count are read digit by digit with a bounded carry, which we prove; the reduced count is consequently recognised by a finite automaton, and an all-n proof of the closed form is reduced to a finite verification. The finite-order counts below are formally verified in Lean 4 — apart from the few statements we mark as lying outside the formal development — and we say exactly which of them rest on exhaustive computation and what was searched.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
8e9c835d78417421f0113486ddb7df298bf36ea83fc3ffb15cf0480330b5bda5
Claim ledger
Stated results
F1known2026-08-29
the triple enumeration reproduces the |Eₙ| and |Lₙ| columns of Table 1, every column of Table 2 and every column of Table 3 of arXiv:2608.15925v1 at orders 1..5, from the paper's own definitions (the remaining columns of Table 1 count pairs by completion number and are not computed)
F2routine2026-08-29
the axis reduction returns the same per-axis counts |Aₙ(tau)| and |Aₙ(tau) cap Pₙ| as the triple enumeration, at orders 1..5
F3known2026-08-29
|Aₙ(tau)| = 3*4ⁿ⁻¹ - 2ⁿ at orders 1..7 through the reduction, and at orders 8, 9
F4candidate2026-08-29
|Aₙ(tau) cap Pₙ| = 8*3ⁿ⁻² - 2ⁿ at orders 2..7, hence |Aₙ cap Pₙ| = 8*3ⁿ⁻¹ - 5*2ⁿ + 2: a closed form for the column Remark 7.5 of arXiv:2608.15925v1 leaves open
F5routine2026-08-29
negative controls: off-by-one on the open column at orders 5, 7 and 8 is refuted; the product-centered condition and the j/k-support condition each strictly cut the count; the order-6 coincidence |A cap L cap P| = |A cap X cap P| does not already happen at order 5; the two carry increment bounds are attained and the carry window is tight
F6routine2026-08-29
bounded carry: increments of size at most C cannot drive a carry from outside (-C, C) back to 0, so every accepting run of the axis automaton has |delta| <= 2 and |delta'| <= 1; the two increment bounds for this problem are 3 and 2 and both are attained
F7candidate2026-08-29
the open column past the source's own enumeration: |Aₙ(tau) cap Pₙ| = 5576, 16984, 51464 at n = 8, 9, 10, hence |Aₙ cap Pₙ| = 16218, 49930, 152346 and |Aₙ cap Xₙ cap Pₙ| = 9744, 32193, 104331; with |Aₙ(tau)| = 3*4ⁿ⁻¹ - 2ⁿ at n = 8, 9 as a published control
F8prose2026-08-29
the axis reduction: Aₙ(tau) is in bijection with b: D(b) nonempty, x(b)+y(b) in x(W), and in the first apex case C_T = Q_T is equivalent to x(p) = x(b) where p is b₀ with e and i swapped on D(b)
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- > Corrections, 2026-08-30 (paper referee pass). > > 1. Arithmetic. Row F7 originally recorded |A₁0 ∩ X₁0 ∩ P₁0| = 108156. That > is wrong; the value is 104331. Both the subtraction > 152346 - 48015 (with |A₁0∩L₁0∩P₁0| = 3F₂2 - 5·2¹0 + 2 = 48015, F₂2 = > 17711) and the closed form 8·3⁹ - 3F₂2 = 157464 - 53133 give 104331, and an > independent enumeration of A₁0(τ) written from the source's definitions — > triangles b₀, b, τb with b₀ τ-fixed, equilaterality tested by comparing the > three q-distances, locality by Definition 5.1/5.2, product-centrin
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7