A rank-three refutation of the Okada discriminant identity

Abstract

Hivert–Scott Conjecture 7.9 fails at N = 3 over the rationals with X = (1,2) and Y = (1): the regular-trace determinant is -16 and the cell-determinant product is 1.

Definition 1.1 (Presentation relations).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,(\forall i:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right),\mathrm{Relations}\left(N,K,X,Y,\mathrm{iota}\left(K,i\right)\cdot \mathrm{iota}\left(K,i\right),\mathrm{smul}\left(X\left(i\right),\mathrm{iota}\left(K,i\right)\right)\right))\wedge ((\forall i:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right),\forall j:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right),((\mathrm{val}\left(i\right)+2\le \mathrm{val}\left(j\right))\vee (\mathrm{val}\left(j\right)+2\le \mathrm{val}\left(i\right)))\Rightarrow (\mathrm{Relations}\left(N,K,X,Y,\mathrm{iota}\left(K,i\right)\cdot \mathrm{iota}\left(K,j\right),\mathrm{iota}\left(K,j\right)\cdot \mathrm{iota}\left(K,i\right)\right)))\wedge (\forall i:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right),\forall h:\mathrm{val}\left(i\right)+1<\mathrm{natSub}\left(N,1\right),\mathrm{Relations}\left(N,K,X,Y,\mathrm{iota}\left(K,Fin.mk\left(\mathrm{val}\left(i\right)+1,h\right)\right)\cdot \mathrm{iota}\left(K,Fin.mk\left(\mathrm{val}\left(i\right),Nat.l{\mathrm{t}}_{\mathrm{o}{\mathrm{f}}_{\mathrm{suc}{\mathrm{c}}_{\mathrm{lt}}}}\left(h\right)\right)\right)\cdot \mathrm{iota}\left(K,Fin.mk\left(\mathrm{val}\left(i\right)+1,h\right)\right),\mathrm{smul}\left(Y\left(i\right),\mathrm{iota}\left(K,Fin.mk\left(\mathrm{val}\left(i\right)+1,h\right)\right)\right)\right)))$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.Relations (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 3.1, page 10: “Fix a positive integer N. Given a field 𝕂, let X = (x₁, …, x_{N−1}) and Y = (y₁, …, y_{N−2}) be two sequences of element of 𝕂. The Okada algebra O_N(X,Y) is the algebra generated by {E_i | i = 1 … N − 1} and subject to the relations E_i² = x_i E_i (1 ≤ i ≤ N − 1), E_i E_j = E_j E_i (|i − j| ≥ 2), E_{i+1} E_i E_{i+1} = y_i E_{i+1} (1 ≤ i ≤ N − 2).” Relations is the least inductive binary relation with these three constructors in the free K-algebra. All generator indices are shifted down by one. natSub is natural subtraction truncated at zero; smul is scalar multiplication. Fin.mk inserts the indicated natural value and its bound proof. Qualified proof names display underscore-separated suffixes as nested subscripts.

Definition 1.2 (The presented algebra).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\mathrm{Presented}\left(N,K,X,Y\right)=\mathrm{RingQuot}\left(\mathrm{Relations}\left(N,K,X,Y\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.Presented (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

RingQuot takes the algebra quotient imposing the three presentation relations; the carrier is the actual presented algebra, rather than a matrix chosen to stand in for it.

Definition 1.3 (Quotient generators).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\forall i:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right),\mathrm{generator}\left(N,K,X,Y,i\right)=\mathrm{mkAlgHom}\left(K,\mathrm{Relations}\left(N,K,X,Y\right)\right)\left(\mathrm{iota}\left(K,i\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.generator (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

The generator is the image of the corresponding free-algebra generator under the quotient algebra homomorphism. Paper E_i is generator(i-1).

Definition 1.4 (Permutation code).

$$\forall N:\mathbb{N},\forall sigma:\mathrm{Perm}\left(\mathrm{Fin}\left(N\right)\right),\forall i:\mathrm{Fin}\left(N\right),\mathrm{code}\left(N,sigma,i\right)=\mathrm{card}\left(\mathrm{filter}\left((\lambda k:\mathrm{Fin}\left(N\right),(k<i)\wedge (\mathrm{symm}\left(sigma\right)\left(i\right)<\mathrm{symm}\left(sigma\right)\left(k\right))),\mathrm{univ}\left(\mathrm{Fin}\left(N\right)\right)\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.code (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 3.3, pages 10–11: “The code of a permutation σ ∈ S_N is the N-tuple code(σ) = (c₁, …, c_N) where c_i := #{k < i | σ⁻¹(k) > σ⁻¹(i)}.” Finset.card is cardinality, filter retains precisely the elements satisfying its predicate, and symm is the inverse permutation.

Definition 1.5 (Lexicographically minimal word).

$$\forall N:\mathbb{N},\forall sigma:\mathrm{Perm}\left(\mathrm{Fin}\left(N\right)\right),\mathrm{lexmin}\left(N,sigma\right)=\mathrm{flatMap}\left((\lambda i:\mathrm{Fin}\left(N\right),\mathrm{map}\left((\lambda j:\mathrm{Fin}\left(\mathrm{val}\left(i\right)\right),Fin.mk\left(\mathrm{val}\left(j\right),Nat.l{\mathrm{t}}_{\mathrm{o}{\mathrm{f}}_{\mathrm{l}{\mathrm{t}}_{\mathrm{o}{\mathrm{f}}_{\mathrm{le}}}}}\left(Fin.isLt\left(j\right),Nat.l{\mathrm{e}}_{\mathrm{su}{\mathrm{b}}_{\mathrm{on}{\mathrm{e}}_{\mathrm{o}{\mathrm{f}}_{\mathrm{lt}}}}}\left(Fin.isLt\left(i\right)\right)\right)\right)),\mathrm{filter}\left((\lambda j:\mathrm{Fin}\left(\mathrm{val}\left(i\right)\right),\mathrm{natSub}\left(\mathrm{val}\left(i\right),\mathrm{code}\left(N,sigma,i\right)\right)\le \mathrm{val}\left(j\right)),\mathrm{reverse}\left(\mathrm{finRange}\left(\mathrm{val}\left(i\right)\right)\right)\right)\right)),\mathrm{finRange}\left(N\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.lexmin (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Page 11: “It is well known that the product ∏(i=1)^n s{i−1}s_{i−2} ··· s_{i−c_i} is the lexicographically minimal reduced factorization of the permutations σ. We denote the associated index word by LexMin(σ).” finRange lists Fin elements increasingly. Each block is reversed and filtered to the last code(σ,i) entries, then converted to generator indices. flatMap concatenates the blocks in increasing i order.

Definition 1.6 (Lexmin algebra elements).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\forall sigma:\mathrm{Perm}\left(\mathrm{Fin}\left(N\right)\right),\mathrm{lexElement}\left(N,K,X,Y,sigma\right)=\mathrm{prod}\left(\mathrm{map}\left(\mathrm{generator}\left(N,K,X,Y\right),\mathrm{lexmin}\left(N,sigma\right)\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.lexElement (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 3.4, page 11: “Fix a family of generators (g_i) of a monoid or an algebra. To a permutation σ we associate the element g_σ defined by g_σ := g_LexMin(σ) = ∏(i=1)^n g{i−1}g_{i−2} ··· g_{i−c_i}, where (c₁, …, c_N) = code(σ), and the product is increasing with i.” prod of a list is its ordered product, including the unit for the empty word.

Definition 1.7 (Regular-trace Gram matrix).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\forall sigma:\mathrm{Perm}\left(\mathrm{Fin}\left(N\right)\right),\forall tau:\mathrm{Perm}\left(\mathrm{Fin}\left(N\right)\right),\mathrm{regularGram}\left(N,K,X,Y\right)\left(sigma,tau\right)=\mathrm{trace}\left(K,\mathrm{Presented}\left(N,K,X,Y\right),\mathrm{lmul}\left(K,\mathrm{Presented}\left(N,K,X,Y\right),\mathrm{lexElement}\left(N,K,X,Y,sigma\right)\right)\cdot \mathrm{lmul}\left(K,\mathrm{Presented}\left(N,K,X,Y\right),\mathrm{lexElement}\left(N,K,X,Y,tau\right)\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.regularGram (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Page 60: “Recall the discriminant of the Okada algebra is determinant of the N! × N! matrix G_N with entries given by [G_N]_{σ,τ} := tr [ϱ^reg(E_σ)ϱ^reg(E_τ)] where ϱ^reg is the left-regular representation of O_N(X,Y) and σ, τ ∈ S_N.” lmul(K,A,z) denotes left multiplication by z on A. trace(K,A,f) is the trace of the linear endomorphism f. The dimension and basis used for this trace are proved at the rational rank-three specialization.

Definition 1.8 (Fibonacci-set predicate).

$$\forall N:\mathbb{N},\forall S:\mathrm{Finset}\left(\mathrm{Fin}\left(N\right)\right),(\mathrm{IsFibonacciSet}\left(N,S\right))\iff ((\mathrm{mod}\left(\mathrm{card}\left(S\right),2\right)=\mathrm{mod}\left(N,2\right))\wedge (\forall s:\mathrm{Fin}\left(N\right),(s\in S)\Rightarrow (\mathrm{mod}\left(\mathrm{val}\left(s\right)+1,2\right)=\mathrm{mod}\left(\mathrm{card}\left(\mathrm{filter}\left((\lambda t:\mathrm{Fin}\left(N\right),t<s),S\right)\right)+1,2\right))))$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.IsFibonacciSet (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 4.5, page 33: “A Fibonacci set of rank N is a subset S = {s₁ < s₂ < ··· < s_k} of [N] whose size k has the same parity as N and such that s_i has the same parity as i for all i ∈ {1, …, k}.” mod is natural-number remainder. Counting the members less than s gives its zero-based rank in the increasing enumeration. val of a Fin element extracts its natural label.

Definition 1.9 (Fibonacci-set carrier).

$$\forall N:\mathbb{N},\mathrm{FibonacciSet}\left(N\right)=\{S:\mathrm{Finset}\left(\mathrm{Fin}\left(N\right)\right)\mid \mathrm{IsFibonacciSet}\left(N,S\right)\}$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.FibonacciSet (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

The subtype carries a finite set together with the Fibonacci-set predicate. Its finite enumeration and decidable equality are the existing subtype instances.

Definition 1.10 (Incidence data for a half diagram).

$$\forall N:\mathbb{N},\mathrm{HalfData}\left(N\right)=(\mathrm{Fin}\left(N\right)\to \mathrm{Fin}\left(N\right))\times (\mathrm{Fin}\left(N\right)\to \mathrm{Fin}\left(N\right))$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.HalfData (✓ std3).

Source. Repository-derived.

Commentary.

Half-diagram incidence is encoded by a partner map and a label map, both on Fin(N). A fixed partner is a propagating endpoint. Arc and endpoint labels are shifted down by one from the paper.

Definition 1.11 (Valid labelled half diagrams).

$$\forall N:\mathbb{N},\forall H:\mathrm{HalfData}\left(N\right),(\mathrm{HalfValid}\left(N,H\right))\iff ((\forall i:\mathrm{Fin}\left(N\right),\mathrm{fst}\left(H\right)\left(\mathrm{fst}\left(H\right)\left(i\right)\right)=i)\wedge ((\forall i:\mathrm{Fin}\left(N\right),\mathrm{snd}\left(H\right)\left(\mathrm{fst}\left(H\right)\left(i\right)\right)=\mathrm{snd}\left(H\right)\left(i\right))\wedge ((\forall i:\mathrm{Fin}\left(N\right),(\mathrm{snd}\left(H\right)\left(i\right)\le i)\wedge (\mathrm{mod}\left(\mathrm{val}\left(\mathrm{snd}\left(H\right)\left(i\right)\right),2\right)=\mathrm{mod}\left(\mathrm{val}\left(\min \left(i,\mathrm{fst}\left(H\right)\left(i\right)\right)\right),2\right)))\wedge ((\forall i:\mathrm{Fin}\left(N\right),\forall j:\mathrm{Fin}\left(N\right),(i<\mathrm{fst}\left(H\right)\left(i\right))\Rightarrow ((\mathrm{fst}\left(H\right)\left(j\right)=j)\Rightarrow (\neg ((i<j)\wedge (j<\mathrm{fst}\left(H\right)\left(i\right))))))\wedge ((\forall i:\mathrm{Fin}\left(N\right),\forall j:\mathrm{Fin}\left(N\right),(i<\mathrm{fst}\left(H\right)\left(i\right))\Rightarrow ((j<\mathrm{fst}\left(H\right)\left(j\right))\Rightarrow ((i<j)\Rightarrow ((j<\mathrm{fst}\left(H\right)\left(i\right))\Rightarrow (\mathrm{fst}\left(H\right)\left(j\right)<\mathrm{fst}\left(H\right)\left(i\right))))))\wedge ((\forall i:\mathrm{Fin}\left(N\right),\forall j:\mathrm{Fin}\left(N\right),(i<\mathrm{fst}\left(H\right)\left(i\right))\Rightarrow ((j<\mathrm{fst}\left(H\right)\left(j\right))\Rightarrow ((i<j)\Rightarrow ((\mathrm{fst}\left(H\right)\left(j\right)<\mathrm{fst}\left(H\right)\left(i\right))\Rightarrow (\mathrm{snd}\left(H\right)\left(i\right)<\mathrm{snd}\left(H\right)\left(j\right))))))\wedge ((\forall i:\mathrm{Fin}\left(N\right),\forall j:\mathrm{Fin}\left(N\right),(\mathrm{fst}\left(H\right)\left(i\right)=i)\Rightarrow ((j<\mathrm{fst}\left(H\right)\left(j\right))\Rightarrow ((i<j)\Rightarrow (\mathrm{snd}\left(H\right)\left(i\right)<\mathrm{snd}\left(H\right)\left(j\right)))))\wedge (\forall i:\mathrm{Fin}\left(N\right),\forall j:\mathrm{Fin}\left(N\right),(\mathrm{fst}\left(H\right)\left(i\right)=i)\Rightarrow ((\mathrm{fst}\left(H\right)\left(j\right)=j)\Rightarrow ((i<j)\Rightarrow (\mathrm{snd}\left(H\right)\left(i\right)<\mathrm{snd}\left(H\right)\left(j\right))))))))))))$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.HalfValid (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 3.39, page 23: “A labelled, non-crossing arc-diagram is called an Okada arc-diagram if the following conditions are satisfied: (1) the label of each arc a — b must be at least 1 and at most min(|a|, |b|), (2) the label of each arc a — b must have the same parity as min(|a|, |b|). (3) if an arc a — b is nested in an arc c — d then the label of a — b is strictly larger than the label of c — d.” Page 31: “A half Okada arc-diagram H is a labelled, non-crossing half arc-diagram which satisfies Conditions 1 to 3, or, equivalently, if gluing H with its mirror produces a valid Okada arc-diagram.” The eight conjuncts encode involutivity, label constancy along an arc, bounds and parity, absence of a propagating point under a nonpropagating arc, noncrossing, and the three nested label orders. fst and snd project incidence data.

Definition 1.12 (Half-diagram carrier).

$$\forall N:\mathbb{N},\mathrm{HalfDiagram}\left(N\right)=\{H:\mathrm{HalfData}\left(N\right)\mid \mathrm{HalfValid}\left(N,H\right)\}$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.HalfDiagram (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

A half diagram consists of its incidence data and the validity predicate. Incidence identifies diagrams up to planar isotopy.

Definition 1.13 (Propagating endpoints).

$$\forall N:\mathbb{N},\forall H:\mathrm{HalfDiagram}\left(N\right),\mathrm{propagatingIndices}\left(N,H\right)=\mathrm{filter}\left((\lambda i:\mathrm{Fin}\left(N\right),\mathrm{fst}\left(\mathrm{val}\left(H\right)\right)\left(i\right)=i),\mathrm{univ}\left(\mathrm{Fin}\left(N\right)\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.propagatingIndices (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 4.3, page 31: “The propagating index set of a half Okada arc-diagram H of rank N is the subset PInd(H) of [N] containing the indices of the nodes of its propagating arcs.” Precisely the fixed points of the partner map propagate.

Definition 1.14 (Propagating labels).

$$\forall N:\mathbb{N},\forall H:\mathrm{HalfDiagram}\left(N\right),\mathrm{propagatingLabels}\left(N,H\right)=\mathrm{image}\left(\mathrm{snd}\left(\mathrm{val}\left(H\right)\right),\mathrm{propagatingIndices}\left(N,H\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.propagatingLabels (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 4.3, page 31: “The propagating label set of a half Okada arc-diagram H of rank N is the subset PLab(H) of [N] containing the labels of its propagating arcs.” The image of the fixed points under the label map is a finite set, with duplicates removed by Finset.image.

Definition 1.15 (Full diagrams).

$$\forall N:\mathbb{N},\mathrm{Diagram}\left(N\right)=\{HK:(\mathrm{HalfDiagram}\left(N\right))\times (\mathrm{HalfDiagram}\left(N\right))\mid \mathrm{propagatingLabels}\left(N,\mathrm{fst}\left(HK\right)\right)=\mathrm{propagatingLabels}\left(N,\mathrm{snd}\left(HK\right)\right)\}$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.Diagram (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Lemma 4.4 (Gluing lemma), page 33, identifies a full diagram with a pair of valid halves having equal propagating label sets. Subtype.val extracts this pair.

Definition 1.16 (Gluing halves).

$$\forall N:\mathbb{N},\forall H:\mathrm{HalfDiagram}\left(N\right),\forall L:\mathrm{HalfDiagram}\left(N\right),\forall h:\mathrm{propagatingLabels}\left(N,H\right)=\mathrm{propagatingLabels}\left(N,L\right),\mathrm{val}\left(\mathrm{glue}\left(N,H,L,h\right)\right)=(H,L)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.glue (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Gluing lemma, page 33: “Moreover if L and R are two Okada half arc-diagrams such that PLab(L) = PLab(R), then there is a unique Okada arc-diagram L ⋈ R such that |L ⋈ R⟩ = L and ⟨L ⋈ R| = R.” glue stores the ordered pair and the equality proof. The formula displays its underlying pair; h is used as the gluing proof argument.

Definition 1.17 (Signed arc data).

$$\mathrm{Arc}=(\mathbb{Z})\times ((\mathbb{N})\times (\mathbb{Z}))$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.Arc (✓ std3).

Source. Repository-derived.

Commentary.

An arc is a signed left endpoint, a positive paper label, and a signed right endpoint. The tuple is right associated.

Definition 1.18 (Undirected labelled-arc lookup).

$$\forall arcs:\mathrm{List}\left(\mathrm{Arc}\right),\forall i:\mathbb{Z},\forall label:\mathbb{N},\forall j:\mathbb{Z},\mathrm{hasArc}\left(arcs,i,label,j\right)=\mathrm{any}\left((\lambda a:\mathrm{Arc},\mathrm{band}\left(\mathrm{beq}\left(\mathrm{fst}\left(\mathrm{snd}\left(a\right)\right),label\right),\mathrm{bor}\left(\mathrm{band}\left(\mathrm{beq}\left(\mathrm{fst}\left(a\right),i\right),\mathrm{beq}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right),j\right)\right),\mathrm{band}\left(\mathrm{beq}\left(\mathrm{fst}\left(a\right),j\right),\mathrm{beq}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right),i\right)\right)\right)\right)),arcs\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.hasArc (✓ std3).

Source. Repository-derived.

Commentary.

hasArc is Boolean lookup in a list of arc triples. beq denotes Boolean equality, band and bor are Boolean conjunction and disjunction, and any is existential Boolean list search. Reversing the endpoints preserves lookup.

Definition 1.19 (Signed arcs of glued halves).

$$\forall N:\mathbb{N},\forall D:\mathrm{Diagram}\left(N\right),\mathrm{diagramArcs}\left(N,D\right)=\mathrm{append}\left(\mathrm{append}\left(\mathrm{filterMap}\left((\lambda i:\mathrm{Fin}\left(N\right),\mathrm{ite}\left(i<\mathrm{fst}\left(\mathrm{val}\left(\mathrm{fst}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right),\mathrm{some}\left((\mathrm{castZ}\left(\mathrm{val}\left(i\right)+1\right),(\mathrm{val}\left(\mathrm{snd}\left(\mathrm{val}\left(\mathrm{fst}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right)\right)+1,\mathrm{castZ}\left(\mathrm{val}\left(\mathrm{fst}\left(\mathrm{val}\left(\mathrm{fst}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right)\right)+1\right)))\right),\mathrm{none}\right)),\mathrm{finRange}\left(N\right)\right),\mathrm{filterMap}\left((\lambda i:\mathrm{Fin}\left(N\right),\mathrm{ite}\left(i<\mathrm{fst}\left(\mathrm{val}\left(\mathrm{snd}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right),\mathrm{some}\left((-\mathrm{castZ}\left(\mathrm{val}\left(i\right)+1\right),(\mathrm{val}\left(\mathrm{snd}\left(\mathrm{val}\left(\mathrm{snd}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right)\right)+1,-\mathrm{castZ}\left(\mathrm{val}\left(\mathrm{fst}\left(\mathrm{val}\left(\mathrm{snd}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right)\right)+1\right)))\right),\mathrm{none}\right)),\mathrm{finRange}\left(N\right)\right)\right),\mathrm{filterMap}\left((\lambda i:\mathrm{Fin}\left(N\right),\mathrm{ite}\left(\mathrm{fst}\left(\mathrm{val}\left(\mathrm{fst}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right)=i,\mathrm{some}\left((\mathrm{castZ}\left(\mathrm{val}\left(i\right)+1\right),(\mathrm{val}\left(\mathrm{snd}\left(\mathrm{val}\left(\mathrm{fst}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right)\right)+1,-\mathrm{castZ}\left(\mathrm{val}\left(\mathrm{getD}\left(\mathrm{find}\left((\lambda j:\mathrm{Fin}\left(N\right),(\mathrm{fst}\left(\mathrm{val}\left(\mathrm{snd}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(j\right)=j)\wedge (\mathrm{snd}\left(\mathrm{val}\left(\mathrm{snd}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(j\right)=\mathrm{snd}\left(\mathrm{val}\left(\mathrm{fst}\left(\mathrm{val}\left(D\right)\right)\right)\right)\left(i\right))),\mathrm{finRange}\left(N\right)\right),i\right)\right)+1\right)))\right),\mathrm{none}\right)),\mathrm{finRange}\left(N\right)\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.diagramArcs (✓ std3).

Source. Repository-derived.

Commentary.

The first list records left nonpropagating arcs, the second right nonpropagating arcs with negative endpoints, and the third propagating arcs. For each left propagating endpoint, find searches for the right fixed point with the same label. getD uses that left index if the search fails. This fallback is explicit in the expression; all rank-three arcs used in the refutation are checked. filterMap discards none and retains the value of some.

Definition 1.20 (Recursive diagram flattening).

$$\forall arcs:\mathrm{List}\left(\mathrm{Arc}\right),(\mathrm{flattenWord}\left(0,arcs\right)=[])\wedge (\forall n:\mathbb{N},\mathrm{flattenWord}\left(n+1,arcs\right)=\mathrm{ite}\left(\mathrm{hasArc}\left(arcs,\mathrm{castZ}\left(n+1\right),n+1,-\mathrm{castZ}\left(n+1\right)\right),\mathrm{flattenWord}\left(n,\mathrm{filter}\left((\lambda a:\mathrm{Arc},\mathrm{boolNot}\left(\mathrm{hasArc}\left([a],\mathrm{castZ}\left(n+1\right),n+1,-\mathrm{castZ}\left(n+1\right)\right)\right)),arcs\right)\right),\mathrm{let}\left(\mathrm{foldl}\left(\max ,0,\mathrm{filter}\left((\lambda d:\mathbb{N},\mathrm{band}\left(\mathrm{decide}\left(0<d\right),\mathrm{hasArc}\left(arcs,-\mathrm{castZ}\left(d\right),d,-\mathrm{castZ}\left(d+1\right)\right)\right)),\mathrm{range}\left(n+1\right)\right)\right),(\lambda d:\mathbb{N},\mathrm{append}\left(\mathrm{flattenWord}\left(n,\mathrm{map}\left((\lambda a:\mathrm{Arc},((\lambda t:\mathbb{Z},\mathrm{ite}\left(t=\mathrm{castZ}\left(n+1\right),-\mathrm{castZ}\left(n\right),\mathrm{ite}\left((t<0)\wedge (d+2\le \mathrm{natAbs}\left(t\right)),-\mathrm{castZ}\left(\mathrm{natSub}\left(\mathrm{natAbs}\left(t\right),2\right)\right),t\right)\right))\left(\mathrm{fst}\left(a\right)\right),(\mathrm{fst}\left(\mathrm{snd}\left(a\right)\right),(\lambda t:\mathbb{Z},\mathrm{ite}\left(t=\mathrm{castZ}\left(n+1\right),-\mathrm{castZ}\left(n\right),\mathrm{ite}\left((t<0)\wedge (d+2\le \mathrm{natAbs}\left(t\right)),-\mathrm{castZ}\left(\mathrm{natSub}\left(\mathrm{natAbs}\left(t\right),2\right)\right),t\right)\right))\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right)))),\mathrm{filter}\left((\lambda a:\mathrm{Arc},\mathrm{boolNot}\left(\mathrm{hasArc}\left([a],-\mathrm{castZ}\left(d\right),d,-\mathrm{castZ}\left(d+1\right)\right)\right)),arcs\right)\right)\right),\mathrm{filter}\left((\lambda i:\mathbb{N},d\le i),\mathrm{map}\left((\lambda i:\mathbb{N},i+1),\mathrm{reverse}\left(\mathrm{range}\left(n\right)\right)\right)\right)\right))\right)\right))$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.flattenWord (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 3.55 and Proposition 3.56, pages 27–28, flatten the largest right descent after removing a top identity arc. The formula gives the implemented recursion, including the largest eligible descent d (foldl(max,0)) and the endpoint relabelling. A boolNot predicate removes the selected arc. natAbs is integer absolute value valued in the naturals; castZ is the natural-to-integer cast. Correctness of this recursion for arbitrary rank is not asserted here. Its six rank-three values are checked in the proof.

Definition 1.21 (Diagram words in the quotient).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\forall D:\mathrm{Diagram}\left(N\right),\mathrm{diagramElement}\left(N,K,X,Y,D\right)=\mathrm{prod}\left(\mathrm{map}\left((\lambda i:\mathbb{N},\mathrm{dite}\left((0<i)\wedge (i<N),(\lambda h:(0<i)\wedge (i<N),\mathrm{generator}\left(N,K,X,Y,Fin.mk\left(\mathrm{natSub}\left(i,1\right),Nat.su{\mathrm{b}}_{\mathrm{l}{\mathrm{t}}_{\mathrm{su}{\mathrm{b}}_{\mathrm{right}}}}\left(Nat.suc{\mathrm{c}}_{\mathrm{l}{\mathrm{e}}_{\mathrm{o}{\mathrm{f}}_{\mathrm{lt}}}}\left(\mathrm{fst}\left(h\right)\right),\mathrm{snd}\left(h\right)\right)\right)\right)),0\right)),\mathrm{flattenWord}\left(N,\mathrm{diagramArcs}\left(N,D\right)\right)\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.diagramElement (✓ std3).

Source. Repository-derived.

Commentary.

The flattened positive word is mapped to quotient generators and multiplied in order. An index outside 0 < i < N contributes zero. At rank three every index in the six flattened words is within this interval.

Definition 1.22 (Totalized diagram coordinates).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\forall D:\mathrm{Diagram}\left(N\right),\forall z:\mathrm{Presented}\left(N,K,X,Y\right),\mathrm{diagramCoefficient}\left(N,K,X,Y,D,z\right)=\mathrm{dite}\left(\mathrm{Bijective}\left(Fintype.linearCombination\left(K,\mathrm{diagramElement}\left(N,K,X,Y\right)\right)\right),(\lambda h:\mathrm{Bijective}\left(Fintype.linearCombination\left(K,\mathrm{diagramElement}\left(N,K,X,Y\right)\right)\right),\mathrm{symm}\left(\mathrm{ofBijective}\left(Fintype.linearCombination\left(K,\mathrm{diagramElement}\left(N,K,X,Y\right)\right),h\right)\right)\left(z,D\right)),0\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.diagramCoefficient (✓ std3).

Source. Repository-derived.

Commentary.

If diagram expansion is bijective, coefficient extraction is evaluation of its inverse linear equivalence. Otherwise it is zero. The symbol h is the proof of bijectivity used in ofBijective; dite binds it in the positive branch. General diagram-basis bijectivity remains unproved in this module. The proof establishes bijectivity at N = 3 over Q with X = (1,2), Y = (1), so the zero branch is unused there.

Definition 1.23 (Half diagrams in a cell).

$$\forall N:\mathbb{N},\forall S:\mathrm{FibonacciSet}\left(N\right),\mathrm{CellHalf}\left(N,S\right)=\{H:\mathrm{HalfDiagram}\left(N\right)\mid \mathrm{propagatingLabels}\left(N,H\right)=\mathrm{val}\left(S\right)\}$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.CellHalf (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Section 6.1, Restriction and induction of cell modules, equation (35), page 50: “The left O_N(X,Y) cell module V^S associated to S ∈ 𝕐𝔽𝕊_N can be realized by the vector space spanned by rank N half Okada arc-diagrams |D⟩ such that PLab|D⟩ = S equipped with the left action • obtained by extending linearly the formula E_C • |D⟩ := {λ(C,D) |C · D⟩ if PLab(C · D) = S; 0 otherwise} where D ∈ O_N(X,Y).” CellHalf is this basis index set; its cardinality supplies dim(Fib(S)) in the conjecture.

Definition 1.24 (Action on a half-diagram cell).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\forall S:\mathrm{FibonacciSet}\left(N\right),\forall z:\mathrm{Presented}\left(N,K,X,Y\right),\forall v:\mathrm{CellHalf}\left(N,S\right)\to K,\forall H:\mathrm{CellHalf}\left(N,S\right),\mathrm{cellAction}\left(N,K,X,Y,S,z,v\right)\left(H\right)=\sum _{L:\mathrm{CellHalf}\left(N,S\right)}v\left(L\right)\cdot \mathrm{diagramCoefficient}\left(N,K,X,Y,\mathrm{glue}\left(N,\mathrm{val}\left(H\right),\mathrm{val}\left(L\right),\mathrm{trans}\left(\mathrm{prop}\left(H\right),\mathrm{symm}\left(\mathrm{prop}\left(L\right)\right)\right)\right),z\cdot \mathrm{diagramElement}\left(N,K,X,Y,\mathrm{glue}\left(N,\mathrm{val}\left(L\right),\mathrm{val}\left(L\right),\mathrm{rfl}\left(\mathrm{propagatingLabels}\left(N,\mathrm{val}\left(L\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.cellAction (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Equation (35), Section 6.1, page 50: the action retains the output half with the prescribed propagating labels. The coordinate at H sums over input halves L, multiplying their vector coefficients by the coefficient of H glued to L in z times the representative of L glued to itself. At rank three, these coefficients are independent of the ket used to represent each input half.

Definition 1.25 (The cell-form coefficients).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\forall S:\mathrm{FibonacciSet}\left(N\right),\forall H:\mathrm{CellHalf}\left(N,S\right),\forall L:\mathrm{CellHalf}\left(N,S\right),\mathrm{cellForm}\left(N,K,X,Y,S,H,L\right)=\mathrm{dite}\left((\exists c:K,\mathrm{cellAction}\left(N,K,X,Y,S,\mathrm{diagramElement}\left(N,K,X,Y,\mathrm{glue}\left(N,\mathrm{val}\left(H\right),\mathrm{val}\left(H\right),\mathrm{rfl}\left(\mathrm{propagatingLabels}\left(N,\mathrm{val}\left(H\right)\right)\right)\right)\right),Pi.single\left(L,1\right)\right)=\mathrm{smul}\left(c,Pi.single\left(H,1\right)\right)),(\lambda h:(\exists c:K,\mathrm{cellAction}\left(N,K,X,Y,S,\mathrm{diagramElement}\left(N,K,X,Y,\mathrm{glue}\left(N,\mathrm{val}\left(H\right),\mathrm{val}\left(H\right),\mathrm{rfl}\left(\mathrm{propagatingLabels}\left(N,\mathrm{val}\left(H\right)\right)\right)\right)\right),Pi.single\left(L,1\right)\right)=\mathrm{smul}\left(c,Pi.single\left(H,1\right)\right)),Classical.choose\left(h\right)),0\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.cellForm (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Definition 7.7, page 60: “Let S be a rank N Fibonacci set and let V^S be the associated cell module of O_N(X,Y). Attached to this module is an O_N(X,Y)-invariant bilinear form φ_S: V^S × V^S → 𝕂 implicitly defined for two half diagrams H, K with propagating sets PLab(H) = PLab(K) = S by E_{H ⋈ H} • K = φ_S(H,K) H.” The definition selects the scalar c satisfying this action equation. Pi.single(H,1) is the half-diagram basis vector; choose(h) selects a scalar from the existence proof h. If no scalar satisfies the equation the value is zero. At rank three the proof establishes existence, the full equation including off-support components, and agreement of this scalar with the diagram coordinate used for the Gram matrices. The solution is unique because its H coordinate is c. General existence and action laws are not proved here.

Definition 1.26 (Cell Gram matrices).

$$\forall N:\mathbb{N},\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\forall S:\mathrm{FibonacciSet}\left(N\right),\forall H:\mathrm{CellHalf}\left(N,S\right),\forall L:\mathrm{CellHalf}\left(N,S\right),\mathrm{cellGram}\left(N,K,X,Y,S\right)\left(H,L\right)=\mathrm{cellForm}\left(N,K,X,Y,S,H,L\right)$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.cellGram (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Page 60: “The Gram matrix G^S_N of the bilinear form φ_S is the dim V^S × dim V^S matrix whose entries are given by [G^S_N]_{H,K} := φ_S(H,K).” Its index set is exactly CellHalf(N,S).

Definition 1.27 (Hivert–Scott Conjecture 7.9).

$$(claim)\iff (\forall N:\mathbb{N},(0<N)\Rightarrow (\forall K:\mathrm{Type},[\mathrm{Field}\left(K\right)]\forall X:\mathrm{Fin}\left(\mathrm{natSub}\left(N,1\right)\right)\to K,\forall Y:\mathrm{Fin}\left(\mathrm{natSub}\left(N,2\right)\right)\to K,\det \left(\mathrm{regularGram}\left(N,K,X,Y\right)\right)=\prod _{S:\mathrm{FibonacciSet}\left(N\right)}(\det \left(\mathrm{cellGram}\left(N,K,X,Y,S\right)\right){)}^{2\cdot \mathrm{card}\left(\mathrm{CellHalf}\left(N,S\right)\right)}))$$

Formalization. D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.claim (✓ std3).

Citation. Hivert, Florent; Scott, Jeanne (2026). Diagrammatic Okada monoid and cellularity of the Okada algebra. DOI: 10.48550/arXiv.2609.01440. URL: https://arxiv.org/abs/2609.01440v1.

Commentary.

Conjecture 7.9, page 60: “det G_N = ∏_{S ∈ 𝕐𝔽𝕊_N} [det G^S_N]^{2 dim(Fib(S))}.” The preamble specifies regular trace, not a normalized trace. The claim quantifies over every positive N, every field in Lean Type, and all parameter sequences. Perm(Fin(N)) indexes the lexmin basis, FibonacciSet(N) indexes the cells, and card(CellHalf(N,S)) encodes dim(Fib(S)). The universal coordinate encoding has the totalization boundary stated above; the specialization that disproves the identity has a checked diagram basis and the source’s defining cell-form equation.

Theorem 1.28 (Refutation at rank three).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.result (✓ std3). ∎

Resolves. Problems/hivert-scott-2026-okada-discriminant-refutation (refuted) by D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.result.

Source. Repository-derived.

Commentary.

At N = 3 over Q with X = (1,2), Y = (1), the quotient words (1,E₁,E₂,E₁E₂,E₂E₁,E₁E₂E₁) form a basis. Span induction proves generation and an explicit map into Q × Q × M₂(Q) proves independence. The regular-trace Gram matrix has rows (6,3,4,2,2,2), (3,3,2,2,2,2), (4,2,8,4,4,2), (2,2,4,2,4,2), (2,2,4,4,2,2), (2,2,2,2,2,2); an exact rational LU factorization gives determinant -16. The three cell Gram matrices are (1), (1), and ((2,1),(1,1)), each with determinant 1. Their dimensions are 1,1,2, so the conjectured product is 1. Thus the exact identity fails. The proof computes both sides from the quotient and gluing definitions.

References

• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.Arc
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.CellHalf
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.Diagram
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.FibonacciSet
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.HalfData
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.HalfDiagram
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.HalfValid
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.IsFibonacciSet
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.Presented
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.Relations
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.cellAction
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.cellForm
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.cellGram
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.claim
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.code
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.diagramArcs
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.diagramCoefficient
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.diagramElement
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.flattenWord
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.generator
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.glue
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.hasArc
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.lexElement
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.lexmin
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.propagatingIndices
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.propagatingLabels
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.regularGram
• Truth anchor: D5/S0/Certificates/Combinatorics/OkadaDiscriminantRefutation.result