From b8c8544bacfeaf421d82d926f5f90e96a732f320 Mon Sep 17 00:00:00 2001 From: trios-matrix-ledger-bot Date: Fri, 8 May 2026 05:18:49 +0000 Subject: [PATCH] =?UTF-8?q?docs(phd):=20add=20matrix-ledger=20schema=20sec?= =?UTF-8?q?tion=20(L-MATRIX-LEDGER=20=C2=B7=20trios#380=20G4)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Documents the assertions/matrix_samples.jsonl schema produced by the collect-ledger CI step in trios-trainer-igla (PR #106). 37 LOC, under the ≤40 LOC budget mandated by the queen verdict on trios#380. Refs: - trios-trainer-igla#106 (collect-ledger binary + CI step) - trios#380 G4 acceptance gate - t27/proofs/forbidden_seeds.v (R4 trace anchor) - Appendix B Falsifier-2 (R7 witness) Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877 --- docs/phd/appendix/L-pollen-channel.tex | 37 ++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/docs/phd/appendix/L-pollen-channel.tex b/docs/phd/appendix/L-pollen-channel.tex index b9043c0c97..d2898e5c63 100644 --- a/docs/phd/appendix/L-pollen-channel.tex +++ b/docs/phd/appendix/L-pollen-channel.tex @@ -125,6 +125,43 @@ \subsection*{Cross-references} (iv)~\textsc{Appendix~G: Data Availability} for the upstream Zenodo and Hugging Face datasets used by every empirical chapter. +\subsection*{Matrix-ledger schema (\texttt{assertions/matrix\_samples.jsonl})} + +The \emph{format-algo matrix} CI sweep +(\filepath{trios-trainer-igla/.github/workflows/format-algo-matrix.yml}) +emits one \filepath{cell.json} artefact per cell. The post-sweep +\texttt{collect-ledger} job runs the Rust binary +\filepath{matrix\_ledger collect} (R1, no Python or shell), merges every +artefact into a single deterministic JSONL file, and opens an auto-PR +titled \texttt{chore(matrix-ledger): refresh assertions/matrix\_samples.jsonl} +against \filepath{trios-trainer-igla} \texttt{main}. + +Each row of \filepath{matrix\_samples.jsonl} carries the keys +\texttt{cell\_id}, \texttt{format}, \texttt{algo}, \texttt{seed}, +\texttt{seed\_painted}, \texttt{hidden}, \texttt{step}, \texttt{bpb}, +\texttt{initial\_bpb}, \texttt{delta\_bpb}, \texttt{loss\_final}, +\texttt{falsifier\_2\_hit}, \texttt{commit\_sha}, \texttt{run\_id}, +\texttt{ts\_unix}, and an optional \texttt{parse\_error}. Forbidden +seeds $\{42, 43, 44, 45\}$ are repainted to $\varphi$-derived integers +$\{47, 89, 144, 123\}$ via \texttt{paint\_seed} (Lucas$_8$, Fib$_{11}$, +Fib$_{12}$, Lucas$_{10}$ respectively), traced to +\filepath{t27/proofs/forbidden\_seeds.v::forbidden\_seed\_repaint}; the +original raw value is preserved in \texttt{seed\_raw} for audit. The +falsifier-2 boolean fires per cell iff +$\mathrm{bpb} > 1.85$ \emph{or} the reconstructed +$\mathrm{loss}_{\text{final}} = \mathrm{bpb} \cdot \ln 2$ is non-finite +or $\geq 10^{6}$, matching Appendix~B Falsifier-2. + +A full per-column R4 trace (Rust source file, line range, Coq proof if +applicable) lives in +\filepath{assertions/igla\_assertions.json::matrix\_ledger.column\_trace}; +the same block declares \texttt{forbidden\_seeds\_painted}, +\texttt{falsifier\_2\_clause}, and the downstream \texttt{unblocks} +list (lanes L-C6, L-C7, and Appendix~B Falsifier-2 closure-gate). The +ledger is the JSONL substrate that feeds Appendix~B falsifier records +when the Neon \texttt{bpb\_samples} DDL (\texttt{trios-railway\#62}) +is provisioned. + \subsection*{Operator notes} The defense package (lane LD of trios\#265) does not require this stub