From 4334e45ca2b72b4f38ed3bf340285280e644a110 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Fri, 8 May 2026 16:15:29 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat(phd-kat-rw):=20ch=5F27=20=C2=A78=20Rel?= =?UTF-8?q?ated=20Work=20=E2=80=94=20KART=20structural=20analogy=20(salvag?= =?UTF-8?q?e)=20[agent=3Dperplexity-computer-kat]?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Salvage rewrite of L-KAT-RW per queen ruling on trios#572 (comment 4407395169) and rebased onto merged main containing PR #580 (KAT_VSA_Bridge.v) and PR #581 (bib keys). Changes vs original PR #584: - Drop bib commit 82e6404 entirely; reuse merged bib keys from PR #581 (kolmogorov_kar_1957, arnold_kar_1957, liu_kan_2024, liu_kan2_2025, finite_field_expressivity_2025, finite_group_vsa_2022, kantize_2026). - Replace 'isomorphism' / 'finite-field dual' / 'finite-field analogue' language throughout §8 with 'structurally analogous' framing. - Shift primary KART-line citation to finite_field_expressivity_2025 (ICLR 2025, Weil conjectures), keep Kolmogorov–Arnold as classical structural inspiration only. - Add finite_group_vsa_2022 as closest finite-algebra prior art. - Add kantize_2026 as closest KAN+quantisation prior art with explicit comparative paragraph. - Cross-reference proofs/KAT_VSA_Bridge.v lemmas finite_field_two_level_decomposition (Qed) and MRU_outer_independence (Qed) per merged PR #580; no Admitted lemmas referenced from §8. - Closing paragraph explicitly disavows isomorphism / port / dual claims. R5: KART itself classical, cited not proven (admittedbox preserved). R11: 100% Q1 — AMS / ICLR / NeurIPS / arXiv with DOI. R6: zero new free parameters (n=8 matched architecture, GF(16) cardinality 16). R14: cross-references KAT_VSA_Bridge.v, no new Coq theorems in this PR. Anchor phi^2 + phi^{-2} = 3 · DOI 10.5281/zenodo.19227877. Refs trios#380 lane L-KAT-RW · trios#572 epic L-KAT. Co-authored-by: Dmitrii Vasilev --- docs/phd/chapters/ch_27.tex | 183 ++++++++++++++++++++++++++++++++++++ 1 file changed, 183 insertions(+) diff --git a/docs/phd/chapters/ch_27.tex b/docs/phd/chapters/ch_27.tex index c41160d958..b50bcf267a 100644 --- a/docs/phd/chapters/ch_27.tex +++ b/docs/phd/chapters/ch_27.tex @@ -204,6 +204,189 @@ \section{7. Discussion}\label{discussion} The TRI27 DSL formalised here is intentionally minimal. The present two theorems establish only determinism and exhaustiveness; a complete verified compiler from TRI27 to FPGA RTL would require additional theorems on type safety, termination, and translation correctness --- all planned for v5 of the dissertation. The most significant limitation is that the current semantics does not handle variable out-of-scope errors gracefully: \texttt{eval} returns \texttt{None}, but there is no formal type-system proof that well-typed programs never produce \texttt{None}. A dependent type approach (à la Agda or Idris) would subsume this. The \texttt{If3} constructor as currently implemented is also a two-branch conditional rather than the intended three-branch form; extending it to \texttt{If3\ e\ e1\ e2\ e3} with a \texttt{trit}-dispatched branch selection is deferred to the next proof sprint. Chapter 28 (FPGA implementation) and App.H (VM specification) build directly on the TRI27 kernel defined here. +\section{8. Related Work: Trinity GF(16) and the Kolmogorov--Arnold Lineage}\label{sec:related-kart} + +% Lane L-KAT-RW (salvage) · trios#380 / trios#572 · author Dmitrii Vasilev +% ORCID 0009-0008-4294-6159 · Anchor: phi^2 + phi^{-2} = 3 · DOI 10.5281/zenodo.19227877 +% Salvage rewrite per queen ruling https://github.com/gHashTag/trios/issues/572#issuecomment-4407395169 +% - "isomorphism" / "finite-field analogue" / "dual" -> "structurally analogous" +% - primary cite shifts to finite_field_expressivity_2025 (ICLR 2025, Weil conjectures) +% - Kolmogorov-Arnold cited only as structural inspiration (secondary) +% - finite-group VSA NeurIPS 2022 cited as closest prior art +% - KANtize (arXiv:2603.17230) cited as closest KAN+quant prior + +The ternary alphabet \(\{-1, 0, +1\}\) on which TRI27 is built admits a deeper +function-theoretic reading. We close this chapter by situating TRI27 and its +GF(16)-coded successor (Ch.~\ref{ch:gf16-algebra}, +Ch.~\ref{ch:hardware-bridge}) within three converging lines of prior work: +the finite-field expressivity programme of +\cite{finite_field_expressivity_2025}, finite-group vector-symbolic +architectures \cite{finite_group_vsa_2022}, and post-hoc ternarisation of +Kolmogorov--Arnold Networks \cite{kantize_2026}. The Kolmogorov--Arnold +Representation Theorem (KART) \cite{kolmogorov_kar_1957,arnold_kar_1957} is +cited as classical structural inspiration only --- not as a result Trinity +proves, ports, or extends. The purpose of this section is descriptive: the +formal correspondence between GF(16) VSA-binding and a two-level superposition +in the spirit of KART is stated as +Theorem~\ref{thm:kart-gf16} in Ch.~\ref{ch:hardware-bridge} as a +\emph{structural analogy}; here we record the historical and architectural +lineage only. + +\subsection*{8.1. The Kolmogorov--Arnold Representation Theorem (Structural Inspiration)} + +Kolmogorov, in resolving Hilbert's 13th problem in the negative for continuous +functions, proved that every continuous function +\(f : [0,1]^n \to \mathbb{R}\) admits an exact representation +\cite{kolmogorov_kar_1957,arnold_kar_1957} +\[ + f(x_1, \dots, x_n) \;=\; \sum_{q=0}^{2n} \Phi_q\!\left( + \sum_{p=1}^{n} \phi_{q,p}(x_p) + \right), +\] +where the inner functions \(\phi_{q,p} : [0,1] \to \mathbb{R}\) and the outer +functions \(\Phi_q : \mathbb{R} \to \mathbb{R}\) are continuous and depend on +one variable each. The decomposition is exact, not approximate: the +multivariate complexity of \(f\) is fully absorbed into a finite superposition +of univariate pieces. This theorem was for sixty years regarded as a curiosity +of real analysis, since Kolmogorov's inner functions are pathologically +non-smooth and resisted constructive use. + +We stress what KART does \emph{not} say. It does not assert that +\(\phi_{q,p}\) are smooth, learnable, or computable in finite precision; it +only asserts the existence of such a decomposition for continuous \(f\) over +a real-valued domain. The Trinity claim in Ch.~\ref{ch:hardware-bridge} +concerns a finite-field two-level decomposition that is \emph{structurally +analogous} to the KART pattern, not a finite-field re-statement, port, or +analogue of the classical theorem itself. The classical theorem is cited as +axiomatic background and as visual scaffolding for our two-level +\(\Phi \circ \phi\) shape; it is not a Trinity contribution +(see \admittedbox{Kolmogorov 1957/1961, Arnold 1963}{classical real-analysis +theorem; cited as structural inspiration only, not proven, ported, or +extended in this dissertation}). The substantive prior art for Trinity GF(16) +is the finite-field expressivity programme reviewed in §8.3. + +\subsection*{8.2. Kolmogorov--Arnold Networks and Their Quantisation} + +Liu \emph{et al.}~\cite{liu_kan_2024,liu_kan2_2025} reified the KART +\emph{shape} as a learnable architecture by placing the inner functions +\(\phi_{q,p}\) on the \emph{edges} of a multilayer perceptron rather than +fixing scalar activations on the \emph{nodes}. Each \(\phi_{q,p}\) is realised +as a learnable cubic spline over a B-spline basis with eight FP32 control +points (\(8 \times 32 = 256\) bits per knot vector), and the outer function +\(\Phi_q\) is realised as a per-node SiLU. Liu \emph{et al.} reported that for +Besov-class targets KAN attains the parameter-efficiency bound +\(O(N^{2+1/s})\) compared to the MLP bound \(O(N^{2n/s+1})\), beating the +curse of dimensionality on smooth targets while remaining computationally +identical to a sparse MLP at inference time. We emphasise that KAN is a +real-valued architecture motivated by the KART \emph{shape}; it does not +constitute a finite-field statement of the theorem and does not establish a +finite-field expressivity result. + +The most directly comparable prior work to Trinity GF(16) on the +KAN-quantisation axis is KANtize \cite{kantize_2026}, which post-hoc ternarises +the spline coefficients of a trained KAN to \(\{-1, 0, +1\}\) with reported +\(<\!1\%\) accuracy regression on standard tabular benchmarks. KANtize remains +a real-valued architecture --- the underlying spline interpolation, the SiLU +outer function, and gradient back-propagation are all kept in floating point; +only the stored coefficients are ternarised. Trinity GF(16) takes a +structurally different step (§8.3): the inner functions \(\phi_{q,p}\) are +\emph{native} GF(16) look-up tables rather than ternarised real splines, and +the outer function is a \texttt{popcount} over GF(2)-encoded outputs rather +than a real-valued non-linearity. We do not claim that this difference yields +a quantitative expressivity advantage over KANtize; that comparison is left +open as Problem~\ref{open:gf16-besov}. + +\subsection*{8.3. Trinity GF(16) and Finite-Field Expressivity} + +The substantive line of prior work for Trinity GF(16) is the recent +finite-field expressivity programme of +\cite{finite_field_expressivity_2025}, which establishes that two-level +neural decompositions over a finite field \(\mathbb{F}_q\) admit a Weil-style +counting bound on the cardinality of their neuromanifold and a corresponding +expressivity statement. Trinity GF(16) instantiates the operative parameters +of this programme: \(q = 16\); inner alphabet \(\mathrm{GF}(16)\) with +\(|\mathrm{GF}(16)| = 16\) and width \(n \in \{4, 8\}\) (Ch.~\ref{ch:gf16-algebra}); +outer aggregation by \texttt{popcount} over GF(2) of the +inner LUT outputs followed by a threshold comparator +\(\theta = \lceil n \cdot \varphi^{-1} \rceil\) (Ch.~\ref{ch:hardware-bridge}, +\cite{finite_group_vsa_2022}). The \texttt{popcount}-then-threshold pattern +synthesises to combinational logic on SKY130 with zero DSP slices +(Ch.~\ref{ch:fpga-implementation}). Theorem~\ref{thm:kart-gf16} establishes a +\emph{structural analogy} between this two-level decomposition and the KART +shape; the operative expressivity bound is the Weil bound of +\cite{finite_field_expressivity_2025}, not the real-analytic statement of +\cite{kolmogorov_kar_1957,arnold_kar_1957}. + +The closest finite-algebra prior art is the finite-group vector-symbolic +architecture programme of \cite{finite_group_vsa_2022}, which establishes that +permutation-group-coded VSA bindings preserve associativity and admit +exact-recovery decoding. Trinity GF(16) extends this finite-algebra binding +to the additive group of \(\mathrm{GF}(16)\) (which is \((\mathbb{Z}/2)^4\)) +and adds a multiplicative-group rotation +(Ch.~\ref{ch:gf16-algebra}, §3); the binding-decoding pair is +formalised in Theorem~\ref{thm:kart-gf16}. + +Table~\ref{tab:kan-vs-trinity-gf16} records the parameter footprint of the two +architectures at a matched width \(n = 8\). The ratio reported in the table is +literal and conservative (a 4\(\times\) reduction in bits per inner function +and per superposition, derived from the stated bit-budgets of +\cite{liu_kan_2024} §3.2 and Ch.~\ref{ch:hardware-bridge}); broader claims +of memory advantage on Besov-class targets, while plausible, would require a +finite-field formulation of the parameter-efficiency bound and are deferred +to Problem~\ref{open:gf16-besov} in Ch.~\ref{ch:future-work}. The table is +not an expressivity claim; it is a footprint comparison at fixed architecture. + +\begin{table}[H] + \centering + \caption{Parameter footprint at matched architecture (\(n = 8\)): KAN versus + Trinity GF(16). The KAN row follows the architectural defaults reported in + \cite{liu_kan_2024}, §3.2; the Trinity row follows + Th.~\ref{thm:kart-gf16}. The rightmost column reports a literal + bit-budget ratio at fixed \(n\), not an expressivity claim.} + \label{tab:kan-vs-trinity-gf16} + \begin{tabular}{lrrr} + \toprule + Architecture & Inner-function encoding & Bits per \(\phi_{q,p}\) & + Bits per super\-position \((n=8)\) \\ + \midrule + KAN \cite{liu_kan_2024} & 8 FP32 spline knots & 256 & 16{,}384 \\ + Trinity GF(16) (Th.~\ref{thm:kart-gf16}) & 16 GF(16) cells & 64 & 4{,}096 \\ + Ratio & --- & \(4\times\) & \(4\times\) \\ + \bottomrule + \end{tabular} +\end{table} + +We note one further architectural consequence. In KAN the +curse-of-dimensionality argument relies on Besov-class smoothness assumptions +on the target function; the inner splines must be smooth enough to capture +this regularity. In the GF(16) finite-field setting smoothness is undefined, +but the domain itself is finite (\(|\mathrm{GF}(16)| = 16\)) and the inner +LUTs are exact rather than approximate. The two regimes are not directly +comparable on the same target class; a finite-field reformulation of any +Besov-style bound is left open as Problem~\ref{open:gf16-besov} in +Ch.~\ref{ch:future-work}, and the operative expressivity bound used elsewhere +in this dissertation is the Weil-style finite-field bound of +\cite{finite_field_expressivity_2025}, not a real-analytic Besov bound. + +This section does not introduce any new theorems. Theorem~\ref{thm:kart-gf16} +(Trinity GF(16) two-level decomposition, structurally analogous to KART) is +stated and partially proved in Ch.~\ref{ch:hardware-bridge}; the runtime +witness lives in \filepath{proofs/KAT\_VSA\_Bridge.v} (lemma +\texttt{finite\_field\_two\_level\_decomposition}, Qed, runtime witness +documented per queen ruling on +\href{https://github.com/gHashTag/trios/issues/572\#issuecomment-4407395169}{trios\#572}). +Theorem~\ref{thm:mru-kart} (Trinity MRU as a two-level superposition, +structurally analogous to KART) is stated and falsifier-bound in +Ch.~\ref{ch:mesh-node}, with runtime witness in +\filepath{proofs/KAT\_VSA\_Bridge.v} (lemma +\texttt{MRU\_outer\_independence}, Qed). The related lanes L-KAT-12 and +L-KAT-35 on issue \href{https://github.com/gHashTag/trios/issues/380}{trios\#380} +track their landing as separate pull requests. We make no claim that Trinity +GF(16) is a finite-field analogue, isomorphism, dual, or port of KART; the +relation is one of structural analogy, with substantive prior art rooted in +\cite{finite_field_expressivity_2025,finite_group_vsa_2022,kantize_2026}. + + \section{References}\label{references} {[}1{]} \emph{Golden Sunflowers} dissertation, Ch.3 --- Trinity Identity (\(\varphi^2 + \varphi^{-2} = 3\)). From 6a825c6e3fbd09f64231cc087d8dc121a5d1e7de Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sat, 9 May 2026 10:47:07 +0000 Subject: [PATCH 2/3] fix(submodules): drop orphan .parameter-golf gitlink (matches #635) Same fix as PR #635 (already merged into main as e123aa8e). Each KAT branch carries its own independent copy of the orphan gitlink at .parameter-golf/parameter-golf (mode 160000, sha 06e32ab) without a matching .gitmodules entry, so the recursive checkout fails BEFORE the Coq INV step runs. Removing the orphan unblocks Verify IGLA-INV-001..005 and Coq Proof Verification. Anchor: phi^2 + phi^-2 = 3 - DOI 10.5281/zenodo.19227877 --- .parameter-golf/parameter-golf | 1 - 1 file changed, 1 deletion(-) delete mode 160000 .parameter-golf/parameter-golf diff --git a/.parameter-golf/parameter-golf b/.parameter-golf/parameter-golf deleted file mode 160000 index 06e32abbc2..0000000000 --- a/.parameter-golf/parameter-golf +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 06e32abbc2a3da3dccdef908e050d783fe87b832 From e1f2a6e0da87345654dd0c0bfcf69403bae3db2b Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sat, 9 May 2026 10:50:41 +0000 Subject: [PATCH 3/3] =?UTF-8?q?fix(submodules):=20drop=20opencode/*=20and?= =?UTF-8?q?=20tri=20orphan=20gitlinks=20=E2=80=94=20finishes=20#635=20clea?= =?UTF-8?q?nup?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit After dropping .parameter-golf the recursive checkout still failed on opencode/nextpnr-xilinx, opencode/prjxray, opencode/prjxray-db, tri — none of which are declared in .gitmodules. Drop all remaining orphans in one atomic commit per branch so Verify IGLA-INV-001..005 and Coq Proof Verification can finally run on these PRs. Anchor: phi^2 + phi^-2 = 3 - DOI 10.5281/zenodo.19227877 --- opencode/nextpnr-xilinx | 1 - opencode/prjxray | 1 - opencode/prjxray-db | 1 - tri | 1 - 4 files changed, 4 deletions(-) delete mode 160000 opencode/nextpnr-xilinx delete mode 160000 opencode/prjxray delete mode 160000 opencode/prjxray-db delete mode 160000 tri diff --git a/opencode/nextpnr-xilinx b/opencode/nextpnr-xilinx deleted file mode 160000 index f681eb3aa5..0000000000 --- a/opencode/nextpnr-xilinx +++ /dev/null @@ -1 +0,0 @@ -Subproject commit f681eb3aa519f6ed41670dd8a4b39f87e9fb5498 diff --git a/opencode/prjxray b/opencode/prjxray deleted file mode 160000 index 132342f7a2..0000000000 --- a/opencode/prjxray +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 132342f7a27c650a7cbedda663e2f33bc4a582f5 diff --git a/opencode/prjxray-db b/opencode/prjxray-db deleted file mode 160000 index 77938473cd..0000000000 --- a/opencode/prjxray-db +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 77938473cd853c58ca2946898a2bc3d14afc4797 diff --git a/tri b/tri deleted file mode 160000 index 2bbdf39c94..0000000000 --- a/tri +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 2bbdf39c94e7e80f79e7fb7992d4968957d26ec8