Overview. The detector branch: interpolation to full-rank orders [cn-0062]

    The detector must do three things at once: kill the additive ambiguity, charge at most one rank per crossing contribution, and give full rank for every vertex order. Barycentric cancellation gives the first property; rank-one atoms give the second; two-triangle interpolation gives the third. The four-by-four example [cn-0040] makes the construction concrete.

    Definition 1. Interpolation nodes [cn-0063]

      Choose distinct real numbers \(t_1,\ldots ,t_m\) at which polynomials will be evaluated. These chosen evaluation points are called interpolation nodes, or simply nodes. A non-node is a real number \(t\notin \{t_1,\ldots ,t_m\}\).

      In the constrained polynomial spaces [cn-0019], the conditions \(P(t_i)\in U_i\) are imposed at these points, so they are also called constraint nodes. They are auxiliary scalars: any distinct choices work, for example \(t_i=i\). With three nodes \(1,2,3\), the conditions concern \(P(1),P(2),P(3)\), while \(t=0\) is a non-node.

      Proof dependencies
      None.
      Provenance
      Terminology used in OpenAI, 23 September 2026 [cn-0042], Sections 2 and 4; explanatory definition added on 9 October 2026.

      Definition 2. Bivariate evaluation vectors and the two triangles [cn-0028]

        Fix \(s\geq 1\), \(n=2s+1\), and distinct real interpolation nodes [cn-0063] \(x_1,\ldots ,x_n\). The bivariate polynomial space used here consists of \(P(u,v)\) of degree at most \(s-1\) in each variable separately. Its dimension is \(s^2\), with basis \(u^a v^b\), \(0\leq a,b<s\). Its evaluation vector at \((x_p,x_q)\) is \(h_{pq}=(x_p^a x_q^b)_{0\leq a,b<s}\).

        The two-triangle pattern is

        \[Q_s=\{(p,q):1\leq q<p\leq s+1\}\ \cup \ \{(p,q):s+1<p<q\leq 2s+1\}.\]

        It has \(s(s+1)/2+s(s-1)/2=s^2\) positions. For \(s=2\), it is \(\{(2,1),(3,1),(3,2),(4,5)\}\). The order of the nodes need not agree with their numerical sizes. This freedom is crucial when relabeling spoke orders [cn-0034].

        For \(s=3\), the selected positions are the bullets in this grid (row \(p\), column \(q\)). The proof first removes row \(4\), then column \(1\); exchanging the remaining groups and swapping coordinates leaves the pattern for \(s=2\).

        \[\begin {array}{c|ccccccc} &1&2&3&4&5&6&7\\\hline 1&\cdot &\cdot &\cdot &\cdot &\cdot &\cdot &\cdot \\ 2&\bullet &\cdot &\cdot &\cdot &\cdot &\cdot &\cdot \\ 3&\bullet &\bullet &\cdot &\cdot &\cdot &\cdot &\cdot \\ 4&\bullet &\bullet &\bullet &\cdot &\cdot &\cdot &\cdot \\ 5&\cdot &\cdot &\cdot &\cdot &\cdot &\bullet &\bullet \\ 6&\cdot &\cdot &\cdot &\cdot &\cdot &\cdot &\bullet \\ 7&\cdot &\cdot &\cdot &\cdot &\cdot &\cdot &\cdot \end {array}\]
        Proof dependencies
        Interpolation nodes [cn-0063]
        Provenance
        OpenAI, 23 September 2026 [cn-0042], Lemma 4.1, equation (4.1); reconstructed as a reading account on 9 October 2026. Lean source: TwoTriangleIndices.

        Lemma 3. Two-triangle interpolation [cn-0029]

          Status:

          Statement. For any distinct real nodes \(x_1,\ldots ,x_{2s+1}\), the \(s^2\) evaluation vectors [cn-0028] \(h_{pq}\), \((p,q)\in Q_s\), form a basis of \(\mathbb R^{s^2}\). Equivalently, evaluation on the two triangles determines a bivariate polynomial of degree at most \(s-1\) in each variable uniquely.

          Proof. There are \(s^2\) positions and coefficients, so it is enough to show that vanishing on the pattern forces the polynomial \(P\) to be zero. Induct on \(s\). For \(s=1\), \(P\) is constant and vanishes at \((x_2,x_1)\).

          For \(s>1\), the row \(p=s+1\) supplies \(s\) roots of \(P(x_{s+1},v)\), whose degree is at most \(s-1\). Hence it vanishes identically, and \(P=(u-x_{s+1})P_1\) with degree at most \(s-2\) in \(u\). The remaining positions \((p,1)\), \(2\leq p\leq s\), give \(s-1\) roots of \(P_1(u,x_1)\), since their first factors are nonzero. Therefore

          \[P(u,v)=(u-x_{s+1})(v-x_1)R(u,v),\qquad \deg _u R,\deg _v R\leq s-2.\]

          On the remaining triangles the two factors are nonzero, so \(R(x_p,x_q)=0\) for \(2\leq q<p\leq s\) and for \(s+2\leq p<q\leq 2s+1\). Relabel the surviving nodes as

          \[(y_1,\ldots ,y_{2s-1})=(x_{s+2},\ldots ,x_{2s+1},x_2,\ldots ,x_s),\qquad S(u,v)=R(v,u).\]

          Swapping the variables interchanges the remaining triangles, and this relabeling makes them exactly \(Q_{s-1}\). The induction hypothesis gives \(S=0\), hence \(R=0\) and \(P=0\). Thus the square evaluation matrix is invertible.

          Proof dependencies
          Bivariate space and pattern [cn-0028]
          Provenance
          OpenAI, 23 September 2026 [cn-0042], Lemma 4.1, equation (4.2); reconstructed as a reading account on 9 October 2026. Lean source: TwoTriangleUnisolvence.

          Definition 4. Barycentric interpolation weights [cn-0030]

            For distinct real interpolation nodes [cn-0063] \(x_1,\ldots ,x_n\), define the node polynomial and barycentric weights by

            \[F(t)=\prod _{p=1}^n(t-x_p),\qquad w_p=\frac 1{F'(x_p)}=\frac 1{\prod _{q\ne p}(x_p-x_q)}.\]

            Distinctness makes every denominator nonzero. The usual Lagrange basis polynomial is \(w_p F(t)/(t-x_p)\). See Berrut–Trefethen, Section 3 [cn-0044] for the classical weights. The next lemma extracts the particular cancellation needed by the detector.

            Proof dependencies
            Interpolation nodes [cn-0063]
            Provenance
            OpenAI, 23 September 2026 [cn-0042], equation (4.3); reconstructed as a reading account on 9 October 2026. Lean source: NodeMoments.

            Lemma 5. Barycentric cancellation below the top degree [cn-0031]

              Status:

              Statement. For the barycentric weights [cn-0030] on \(n\) distinct nodes, every scalar polynomial \(A\) of degree at most \(n-2\) satisfies

              \[\sum _{p=1}^n w_p A(x_p)=0.\]

              Proof. Lagrange interpolation gives

              \[A(t)=\sum _p A(x_p)w_p\frac {F(t)}{t-x_p}.\]

              Both sides have degree at most \(n-1\) and agree at all \(n\) nodes, so the identity follows from the root bound for polynomials. Each quotient \(F(t)/(t-x_p)\) is monic of degree \(n-1\), whereas the coefficient of that degree in \(A\) is zero. Comparing those coefficients proves the assertion.

              Proof dependencies
              Barycentric weights [cn-0030]
              Provenance
              OpenAI, 23 September 2026 [cn-0042], equation (4.5); reconstructed as a reading account on 9 October 2026. Lean source: NodeMoments.

              Definition 6. The rank detector and its atoms [cn-0032]

                Fix \(s\geq 1\), \(n=2s+1\), and distinct real nodes. Using the evaluation vectors [cn-0028] and barycentric weights [cn-0030], define the detector atoms and the linear rank detector

                \[B_{pq}=(x_p-x_q)w_pw_q\,h_{pq}h_{pq}^T,\qquad \Phi (H)=\sum _{p,q=1}^n H(p,q)B_{pq}.\]

                Thus \(\Phi :\mathbb R^{n\times n}\to \mathbb R^{s^2\times s^2}\). The nodes are fixed once for the entire drawing. Different vertex orders are fed into this same map. The scalar weights may have either sign: the argument uses matrix rank and invertibility, not positive semidefiniteness.

                Proof dependencies
                Evaluation vectors [cn-0028]; Barycentric weights [cn-0030]
                Provenance
                OpenAI, 23 September 2026 [cn-0042], equation (4.3); reconstructed as a reading account on 9 October 2026. Lean source: RankDetector.

                Lemma 7. What the detector kills, and its support rank bound [cn-0033]

                  Status:

                  Statement. The rank detector [cn-0032] annihilates every diagonal matrix and every row-plus-column matrix [cn-0017]. Its atom \(B_{pq}\) has rank one for \(p\ne q\) and is zero for \(p=q\). In particular,

                  \[\operatorname {rank}\Phi (H)\leq \#\{(p,q):p\ne q,\ H(p,q)\ne 0\}.\]

                  Proof. For \(p=q\), the factor \(x_p-x_q\) vanishes. For \(p\ne q\), the scalar weight is nonzero and \(h_{pq}\) has constant coordinate \(1\), so its outer product has rank one. Rank subadditivity gives the support bound.

                  An entry of \(B_{pq}\), indexed by \((a,b),(a',b')\), is

                  \[w_p w_q(x_p-x_q)x_p^{a+a'}x_q^{b+b'}.\]

                  Its numerator has degree at most \(2s-1=n-2\) in either variable separately. Apply barycentric cancellation [cn-0031] with the other variable fixed to obtain \(\sum _q B_{pq}=0\) for every \(p\) and \(\sum _p B_{pq}=0\) for every \(q\). Consequently \(\Phi ((r_p+c_q)_{p,q})=0\).

                  Proof dependencies
                  Additive matrices [cn-0017]; Barycentric cancellation [cn-0031]; Detector [cn-0032]
                  Provenance
                  OpenAI, 23 September 2026 [cn-0042], Lemma 4.2(i)–(ii), equation (4.4); reconstructed as a reading account on 9 October 2026. Lean source: DetectorAnnihilation.

                  Lemma 8. Every spoke order has an invertible detector image [cn-0034]

                    Status:

                    Statement. For every half-order matrix [cn-0011] \(S_\prec \), the image \(\Phi (S_\prec )\) under the fixed rank detector [cn-0032] is invertible.

                    Proof. The natural order. Put \(H(p,q)=1_{q<p}\). Then \(S=\tfrac 12\mathbf 1\mathbf 1^T-H-\tfrac 12 I_n\). Since additive and diagonal terms are killed [cn-0033], \(\Phi (S)=-\Phi (H)\). Subtract \(1\) from every row of \(H\) with \(p>s+1\), obtaining \(H'\). This row operation changes \(H\) by an additive matrix, so \(\Phi (H')=\Phi (H)\).

                    Off the diagonal, \(H'\) is supported exactly on the two triangles [cn-0028]: its value is \(+1\) on the lower triangle and \(-1\) on the upper triangle. Let \(A_Q\) have columns \(h_{pq}\) for those \(s^2\) positions. Then

                    \[\Phi (S)=-A_Q D_Q A_Q^T,\qquad D_Q=\operatorname {diag}\bigl (H'(p,q)(x_p-x_q)w_pw_q\bigr )_{(p,q)\in Q_s}.\]

                    Two-triangle interpolation [cn-0029] makes \(A_Q\) invertible; all diagonal entries of \(D_Q\) are nonzero. Their product is invertible, regardless of its signature.

                    An arbitrary order. List its indices as \(\pi (1)\prec \cdots \prec \pi (n)\) and apply the argument to the distinct node tuple \(x_{\pi (1)},\ldots ,x_{\pi (n)}\). This only reindexes the sum defining \(\Phi (S_\prec )\): the node polynomial \(F\) and the original linear map are unchanged. The interpolation theorem required distinct nodes, not increasing numerical order. Thus one fixed detector works at every vertex.

                    Proof dependencies
                    Half-order matrices [cn-0011]; Two-triangle pattern [cn-0028]; Interpolation basis [cn-0029]; Detector [cn-0032]; Annihilation [cn-0033]
                    Provenance
                    OpenAI, 23 September 2026 [cn-0042], Lemma 4.2(iii), equation (4.6); reconstructed as a reading account on 9 October 2026. Lean source: HalfOrderInvertibility.
                    Proof dependencies
                    None.
                    Provenance
                    Expository organization and source review, 9 October 2026.