Good involutions of linear quandles: a conjecture of Ta, and a complete count when 4 ∤ N

Conjecture 5.13 of arXiv:2508.16772v1 proved for EVERY odd n (not only the n = 3, 5, 7 the author's GAP program reached): |Good L_(4n,2n-1)| = 10, with the instances n = 9 (L_(36,17)) and n = 41 (L_(164,81)) spelled out

The source's Remark 5.14 proved from the family's own reduction: for n EVEN, |Good L_(4n,2n-1)| = 4, so the odd hypothesis in Conjecture 5.13 is load-bearing and not decoration

Twenty-seven rows of the source's Table 1 recomputed in Lean: the 26 rows whose reduction parameter g = gcd(N,k-1) is at most 5 (including (8,5) = 36, (15,11) = 26, (24,5) = 36 and part of the dihedral column (label corrected 2026-08-28: N = 7,17,18,19,22,23,25,26,27 have no theorem in Linear.lean; N = 3,4,5 sit under GI-G; true coverage 30 of 47 Table-1 entries)), plus the row (21,8) = 232 reached by counting involutions inside S₇ instead (coverage updated 2026-08-29: 31 of 47 after GI-6 landed (24,17) = 764)

A closed identification the source does not state (its Proposition 5.9 is the g <= 2 sub-case; g >= 3 is new): whenever k² = 1 in Z/N, g = gcd(N,k-1) and gcd(N/g, g) = 1, the good involutions of L_(N,k) are in explicit bijection with the involutions of a g-element set, so |Good L_(N,k)| = A000085(g). This is where the conjecture's 10 = A000085(4) comes from, and it reaches the Table 1 rows (21,8) and (24,17) that a gᵍ decision cannot

The reduction: for N = g*m with k² = 1 in Z/N and the ideal (k-1) equal to the ideal (g), the good involutions of L_(N,k) are in explicit bijection with the maps D: Z/g -> Z/g satisfying D(u) + D(u + m*D(u)) = 0 – a problem g symbols wide, independent of N

The encoding gate: |Good L_(N,k)| computed for N <= 5 by testing ALL N^N functions Z/N -> Z/N against the three axioms, with no structural assumption – Table 1 rows (3,-1) = 1, (4,-1) = 4, (5,-1) = 1, and on the trivial quandles L_(4,1) = 10 and L_(5,1) = 26

The linear quandle really is a quandle: sₓ(x) = x, the self-distributive law sₓ s_y = s_(sₓ(y)) sₓ, bijectivity of every s_y when k is a unit, and the identity is a good involution whenever k² = 1

Negative controls: the claim |Good L_(N,k)| <= 10 is refuted (L_(8,5) has 36), the claim |Good L_(N,k)| >= 1 is refuted (L_(5,2) has none, by full 5⁵ enumeration), and each hypothesis of the reduction is shown non-vacuous – k² = 1 fails at (16,5) where the reduced count would be 16, the ideal condition (k-1)*a = g fails at (8,5) with g = 2 where the wrong count would be 4 against the true 36, and gcd(N/g,g) = 1 fails at (16,9) where A000085(8) = 764 against the true 5776 (2026-08-29 dichotomy pull: 8 new control declarations, journal/2026-08-29-good-inv-dichotomy.md sec 6) (2026-08-30 hyper pull: 5 new control declarations, journal/2026-08-30-good-inv-hyper.md sec 6 – hyper_control_branchₙeeded, the branch hypothesis is load-bearing: at (24,17), where g = 8 and m = 3 are coprime, the hard-branch right-hand side would read A000898(4)² = 5776 against the true 764; hyper_controlₜwo_branches, the dichotomy does not collapse to one formula: at (16,9) the answer is 5776 while A000085(8) = 764; hyper_controlₙotₗe, refuting the too-small claim |Good L_(N,k)| <= 5776, since (28,15) gives 42406144; hyper_controlₙot_ge, refuting the too-large claim that the hard branch always gives at least 36, since (4,3) gives A000898(1)² = 4; and hyper_controlₙonvacuous, every hypothesis of the hard branch simultaneously satisfiable at (16,9))

The complete two-case classification of | Good Λ_(N,k) | for every N ≥ 1 and every k: ZMod N: it is 0 unless k² = 1; and with g = gcd(N,k−1), d = gcd(N/g, g), one has d ∈ 1,2 and the count is A000085(g) when d = 1 and A000898(g/2)² when d = 2. Proved in prose in journal/2026-08-29-good-inv-strategy.md §2; the d = 1 half plus the dichotomy are formalized (rows GI-5, GI-6, GI-8), the d = 2 half is not

Total in k, and the hypotheses discharged: Good Λ_(N,k) ≠ ∅ ⇒ k² = 1 (so the count is 0 for every other k, with no hypothesis on N); the dichotomy gcd(N/g, g) ∣ 2 for g = gcd(N,(k−1).val) whenever k² = 1; and the ideal hypothesis (k−1) = (g) of Reduce.lean, which every instance in this family previously discharged by decide, proved once and for all at g = gcd by divisibility and Bézout

#F: α → α | F ∘ F = id = A000085(card α) for every finite α, proved by a localized deletion induction over Finsets (the transposition-composition map F ↦ F ∘ (u₀ v) is its own inverse, so one funext discharges both halves of Finset.cardₙbij') — Mathlib has no involution-counting lemma. With it: the family's parked cell | Good Λ_(24,17) | = 764, the row (21,8) = 232 for free, | Good Λ_(4n,2n−1) | = 10 re-derived as A000085(4) rather than by a 256-case decision, and | Good Λ_(N,1) | = A000085(N) uniformly in N

Eight cells of | Good Λ_(N,k) | outside every published range, all kernel-bound, at reduction sizes g = 9..16: (45,19) = 2620, (30,11) = 9496, (33,23) = 35696, (60,49) = 140152, (39,14) = 568504, (42,29) = 2390480, (105,76) = 10349536, (48,17) = 46206736. The last also shows that 4 ∣ N does not by itself put a cell in the hard branch

A complete classification for every modulus not divisible by 4 — asymptotically three quarters of all moduli, all k at once: | Good Λ_(N,k) | = A000085(gcd(N,(k−1).val)) if k² = 1 and 0 otherwise. The mechanism is that the dichotomy's second branch needs g and N/g both even, hence 4 ∣ N; the odd-modulus form is stated separately without the if

A closed form for OEIS A387317 (the source's Table 2) at every modulus not divisible by 4 — A387317(N) = Σ_(k ≠ 1, k² = 1) A000085(gcd(N,k−1)), a sum indexed by the square roots of 1 mod N — together with every term with 4 ∤ n in [30, 60] proved in Lean — 23 terms past the sequence's published stop at n = 29, namely a(30) = 9574, a(31) = 1, a(33) = 35701, a(34) = 2, a(35) = 259, a(37) = 1, a(38) = 2, a(39) = 568509, a(41) = 1, a(42) = 2390558, a(43) = 1, a(45) = 2647, a(46) = 2, a(47) = 1, a(49) = 1, a(50) = 2, a(51) = 211799317, a(53) = 1, a(54) = 2, a(55) = 35723, a(57) = 4809701445, a(58) = 2, a(59) = 1

MEASUREMENT — compute versus proof on the same cell, and the price of the formalization. | Good Λ_(24,17) | = 764 cost 11.78 GB peak RSS and 188 s and was still killed by a memory watchdog when attempted as an S₈ count; as a corollary of the A000085 recurrence it is one.trans inside a 12.5 s file. The neighbouring (21,8) = 232, where the search does finish, costs 1 min 47 s at 8.81 GB by search and nothing measurable by proof. Formalization price: 876 Lean lines in two files (223 + 653), ten lake env lean invocations of which four ended in errors, 12 min 46 s of module-check wall plus about four minutes of axiom runs, peak RSS never above 7.04 GB against an import Mathlib baseline of 3.3–6.6 GB on this box, ≈ 0.3 CPU-hours for the whole dispatch. Mathlib v4.32.0 HAD Nat.gcdₑq_gcdₐb, Nat.gcdₘulₗeft, Nat.Coprime.dvdₒf_dvdₘulₗeft, Nat.mul_dvdₘulᵢffₗeft, Nat.dvdₚrime, Finset.cardₙbij', Finset.cardₑqₛum_card_fiberwise, Finset.card_filterₐdd_card_filterₙot, Equiv.swapₐpply_*, ZMod.natCast_zmodᵥal, ZMod.natCastₑq_zeroᵢff, ZMod.card; it LACKED any involution-counting lemma (nearest: Equiv.Perm.FixedPointFree.odd_cardₒfᵢnvolutive, a parity statement) and a Decidable (Function.Involutive F) instance for a general Fintype; and Nat.dvdₛub' has been renamed to Nat.dvdₛub. The strategist's ZMod.addOrderOf_coe, Nat.card_zmultiples and Int.gcdₑq_gcdₐb were never needed: keeping the dichotomy inside ℕ (k² = 1 ⟺ N ∣ a(a+2) with a = (k−1).val, both factors natural) removed the whole ℤ/natAbs layer and cut that lemma from a priced 40–80 lines to 20

The second branch of the family's dichotomy, closed: when k² = 1 and gcd(N/g, g) = 2 (equivalently g and N/g both even), | Good L_(N,k) | = A000898(g/2)². Proved by a deletion induction on the reduced equation itself, coloured by the parity of ZMod g – the natural map to (parity-preserving involution, orbit-colouring) pairs provably does NOT exist when g/2 is even, so the fibration route of the strategy journal is closed off. Lands every d = 2 row of the source's Table 1 that the family had parked on cost: (12,7), (24,7), (24,19) = 400, (16,9) = 5776, (20,11) = 97344, (24,13) = 1915456, (28,15) = 42406144

The complete classification, with no hypothesis at all: for every N >= 1 and every k: ZMod N, | Good L_(N,k) | is 0 unless k² = 1; and with g = gcd(N,(k-1).val) it is A000085(g) when gcd(N/g,g) = 1 and A000898(g/2)² otherwise. This is the prose theorem of row GI-C, formalized – it contains the source's Proposition 5.9 (g <= 2), its Theorem 5.11 (gcd(N/g,g) = 2 with N/g = 2), its Example 2.23 (k = 1) and its open Conjecture 5.13 (g = 4) as special cases, and it is the first statement about Good of a linear quandle quantified over N

Six cells of | Good L_(N,k) | outside EVERY published value – N > 29 puts them past the source's Table 1 and m = N/g > 2 puts them outside the family of its Theorem 5.11, so no published statement covers them: (48,41) = 5776 (g=8), (40,11) = 97344 (g=10), (56,15) = 42406144 (g=14), (72,19) = 28558296064 (g=18), (88,23) = 27271456395264 (g=22), (120,31) = 57351382681767706624 (g=30). The last searches a space of 30³0 2e44 maps at a modulus four times the largest order the source's GAP program reached

The source's Theorem 5.11 re-proved from scratch and uniformly in n: | Good L_(4n,2n+1) | = A000898(n)² for every n >= 1, which is OEIS A202828(n). The source proves it by an explicit count of involutions with i transpositions (its Lemma 5.10); here it is the instance g = 2n, m = 2 of the classification, and the square is the two parity classes of ZMod 2n

OEIS A387317 (the source's Table 2) at the moduli divisible by 4 – the eight terms a(32) = 1049760008, a(36) = 28558296078, a(40) = 848580157352, a(44) = 27271456395278, a(48) = 943132645308616, a(52) = 34877026635366414, a(56) = 1373536895464662312, a(60) = 57351382705526608630 – together with a closed form at EVERY N (no divisibility hypothesis, unlike GI-9). With GI-9's 23 terms this makes a(30)... a(60) a contiguous block of 31 kernel-bound terms past the sequence's published stop at n = 29, which is what an OEIS submission needs and what the 2026-08-29 journal recorded as blocked

MEASUREMENT – the price of Pull C, and a route that provably does not exist. The strategy journal's plan (send D to a pair (parity-preserving involution, per-orbit colour bit)) CANNOT be carried out: for even n no section s of x -> c*x on ZMod 2n satisfies s(-z) = -s(z), equivalently no phi: ZMod 2n -> Bool has both phi(x+n)!= phi(x) and phi(-x) = phi(x), because 2x = n is solvable exactly when n is even. The deletion induction that replaces it runs directly on D, coloured by parity, and needs no section. Formalization price and box conditions also recorded here