Conversation
PR #629 (`feat(trios-mesh): Trinity Node E2E Quality`) added a tree entry at `.parameter-golf/parameter-golf` with mode 160000 and sha `06e32ab...` but did NOT register a matching submodule URL in `.gitmodules`. Every CI job that calls `actions/checkout@v4` with `submodules: recursive` therefore fails at submodule init with fatal: No url found for submodule path '.parameter-golf/parameter-golf' in .gitmodules The process '/usr/bin/git' failed with exit code 128 R7 witness: the failure is upstream of the actual proof-checking step, so checks like `Verify IGLA-INV-001..005` and `Coq Proof Verification (INV-1..5)` print their summary blocks for free but report FAILURE because the runner exited 128 during checkout. This silently blocked the KAT залп (#584 / #591 / #593) for the entire IGLA marathon \u2014 the Coq theorems themselves were not the regression, the phantom gitlink was. The current `.gitmodules` only declares the four `crates/trios-*/vendor/ zig-*` submodules. `parameter-golf` was never tracked as a submodule, so removing the orphan entry from the tree is sufficient \u2014 nothing in the workspace, build, or test paths depends on it. Closes #634 Refs: #584, #591, #593, #629 Anchor: phi^2 + phi^-2 = 3 \u00b7 DOI 10.5281/zenodo.19227877
This was referenced May 9, 2026
gHashTag
pushed a commit
that referenced
this pull request
May 9, 2026
Same fix as PR #635 (already merged into main as e123aa8). 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
gHashTag
pushed a commit
that referenced
this pull request
May 9, 2026
Same fix as PR #635 (already merged into main as e123aa8). 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
gHashTag
pushed a commit
that referenced
this pull request
May 9, 2026
Same fix as PR #635 (already merged into main as e123aa8). 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
gHashTag
pushed a commit
that referenced
this pull request
May 9, 2026
cleanup 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
gHashTag
pushed a commit
that referenced
this pull request
May 9, 2026
cleanup 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
gHashTag
pushed a commit
that referenced
this pull request
May 9, 2026
cleanup 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
gHashTag
added a commit
that referenced
this pull request
May 10, 2026
…atch (#584) * feat(phd-kat-rw): ch_27 §8 Related Work — KART structural analogy (salvage) [agent=perplexity-computer-kat] 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 <admin@t27.ai> * fix(submodules): drop orphan .parameter-golf gitlink (matches #635) Same fix as PR #635 (already merged into main as e123aa8). 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 * fix(submodules): drop opencode/* and tri orphan gitlinks — finishes #635 cleanup 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 --------- Co-authored-by: Dmitrii Vasilev <admin@t27.ai>
gHashTag
added a commit
that referenced
this pull request
May 10, 2026
…nessed n<=4) (#591) * feat(phd-kat-12): Coq stub kart_gf16_isomorphism.v (Admitted) [agent=perplexity-computer-kat] L-KAT-12 — Theorem 12.7 KART-GF(16) isomorphism, Coq side. - New file: trinity-clara/proofs/igla/kart_gf16_isomorphism.v (169 LOC) - Theorem kart_gf16_exact: finite-field analogue of Kolmogorov-Arnold superposition over GF(16) Trinity cells — STATED, NOT PROVEN. Status: Admitted (R5-honest comment names the missing finite-field Besov bound that blocks the Qed). - Two sanity Qed theorems land green: kart_gf16_empty (n=0 trivial) kart_gf16_threshold_zero (theta=0 boundary) - Brute-force witness for n in {2,4} lives in the Rust crate (separate commit) — Coq side stays declarative. R5: status remains Admitted. No flip to Proven. R6: only constants used are {phi, n in Z}, theta = ceil(n*phi^-1). R14: theorem maps to assertions/igla_assertions.json on the L-COQ-* sweep. Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877 * feat(phd-kat-12): Rust witness kart_gf16_witness.rs (n=2 default, n=4 ignored) [agent=perplexity-computer-kat] L-KAT-12 — falsification witness for Theorem 12.7 (KART-GF(16) isomorphism). - New file: crates/trios-golden-float/tests/kart_gf16_witness.rs (187 LOC) - 4 tests: test_kart_gf16_empty — n=0 boundary (default) test_kart_gf16_threshold_zero — theta=0 boundary (default) test_kart_gf16_n2_exhaustive — n=2: 16^4 = 65,536 pairs, default test_kart_gf16_n4_exhaustive — n=4: 16^8 ~ 4.3e9 pairs, #[ignore] - Witness checks the structural KART decomposition holds for every (x, x') in GF(16)^n x GF(16)^n at the chosen seed. - Sanctioned seeds only: F_17..F_21, L_7, L_8 (no forbidden 42/43/44/45). - Sigma threshold theta = ceil(n * phi^-1) per R6. R5 honest: - n=2 runs by default (~65k pairs, sub-second). - n=4 is #[ignore]'d because exhaustive enumeration is conjectural-only evidence, not a proof; documented in test docstring. - n>4 is structurally infeasible to brute-force (16^16 ~ 1.8e19) — the Coq theorem stays Admitted in honest agreement with this gap. R1: pure Rust, no .py/.sh. R6: zero free parameters; only {phi, n in Z}. Forward-references: docs/phd/chapters/ch_12.tex sec.5.2 (next commit). Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877 * feat(phd-kat-12): ch_12 sec.5 Theorem 12.7 KART-GF(16) isomorphism [agent=perplexity-computer-kat] L-KAT-12 — LaTeX side of Theorem 12.7 (KART-GF(16) isomorphism). - docs/phd/chapters/ch_12.tex: replaced 'No Coq theorems' stub with full section 5 (+95 lines), under R12/Lee proof style. - Sec 5.1 Statement: structural isomorphism between Kolmogorov-Arnold superposition (\\cite{kolmogorov1957superposition,arnold1963superposition}) and Trinity GF(16) cells (\\cite{liu2024kan} for KAN context bridge). - Sec 5.1 Proof sketch in Lee/GVSU 'we' pronoun, qed-closed at the decomposition level; finite-field Besov bound deferred. - \\admittedbox{kart_gf16_exact} pointing at trinity-clara/proofs/igla/kart_gf16_isomorphism.v with R5-honest reason. - \\coqcite{kart_gf16_exact}{trinity-clara/proofs/igla/kart_gf16_isomorphism.v} {1-169}{Admitted} — feeds appendix F regenerator. - Sec 5.2 Falsifier: cites the Rust witness crates/trios-golden-float/tests/kart_gf16_witness.rs lines 1-187, with explicit n=2 default + n=4 ignored disclosure (R5-honest). - Sec 5.3 0-DSP discipline: shows the GF(16) tensor product compiles to XOR + popcount, mirrors INV-3 (trinity-clara/proofs/igla/gf16_precision.v). - All 3 \\cite keys land in docs/phd/bibliography.bib (added on feat/phd-kat-rw, PR #584): kolmogorov1957superposition, arnold1963superposition, liu2024kan. R3: section is additive (~95 lines into existing ch_12.tex which already clears 1500-line floor) — no new chapter floor regression. R4: every numeric constant traces back to assertions/igla_assertions.json via the kart_gf16_exact entry the L-COQ-* sweep will register. R5: theorem stays Admitted (matches Coq state); Lee/GVSU 'we' kept. R6: zero free parameters — only {phi, n=4, theta = ceil(n * phi^-1)}. R12: Lee/GVSU style throughout; \\theorem / \\proof / \\qed structure. R14: \\coqcite line lets phd-monograph-auditor LC lane pick it up. Forward-references PR #584 (L-KAT-RW, ch_27 Related Work) for the KAN vs Trinity GF(16) memory comparison Table 27.4 (literal 4x). Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877 * fix(submodules): drop orphan .parameter-golf gitlink (matches #635) Same fix as PR #635 (already merged into main as e123aa8). 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 * fix(submodules): drop opencode/* and tri orphan gitlinks — finishes #635 cleanup 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 --------- Co-authored-by: Dmitrii Vasilev <admin@t27.ai>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Removes the orphan gitlink at
.parameter-golf/parameter-golf(mode160000, sha06e32abbc2a3da3dccdef908e050d783fe87b832) that has no matching entry in.gitmodules. Introduced by PR #629 (feat(trios-mesh): Trinity Node E2E Quality, HEAD2b6bb33).Closes #634.
Symptom (R7 witness)
Every PR / push using
actions/checkout@v4withsubmodules: recursivefails the submodule init step:Concrete failures attributable to this regression:
Verify IGLA-INV-001..005❌ on PR feat(phd-kat-12): Theorem 12.7 KART-GF(16) isomorphism (Admitted, witnessed n<=4) #591 (sha506cccf) — run 25569125604.Coq Proof Verification (INV-1..5)❌ on PR feat(phd-kat-12): Theorem 12.7 KART-GF(16) isomorphism (Admitted, witnessed n<=4) #591 — run 25569125688.30a13ee).Constitutional Enforcement❌ on PRs feat(phd-kat-rw): L-KAT-RW — KART × KAN × Trinity GF16 Related Work patch #584 / feat(phd-kat-12): Theorem 12.7 KART-GF(16) isomorphism (Admitted, witnessed n<=4) #591 / feat(phd-kat-35): Theorem 35.13 Trinity MRU as KART forward-pass (Admitted) + Popper Clause F-5 #593 (downstream — checkout exits 128 before guards run).The KAT залп (#584 L-KAT-RW, #591 L-KAT-12, #593 L-KAT-35) is not a Coq regression — it is a phantom submodule.
Fix
No
.gitmoduleschange required — the path was never declared. The four legitimatecrates/trios-*/vendor/zig-*submodules remain untouched.Acceptance
Verify IGLA-INV-001..005on PRs feat(phd-kat-12): Theorem 12.7 KART-GF(16) isomorphism (Admitted, witnessed n<=4) #591 and feat(phd-kat-35): Theorem 35.13 Trinity MRU as KART forward-pass (Admitted) + Popper Clause F-5 #593 → green.Coq Proof Verification (INV-1..5)on feat(phd-kat-12): Theorem 12.7 KART-GF(16) isomorphism (Admitted, witnessed n<=4) #591 and feat(phd-kat-35): Theorem 35.13 Trinity MRU as KART forward-pass (Admitted) + Popper Clause F-5 #593 → green.REVIEW_REQUIRED.git submodule statusafter fresh recursive checkout reports only the four declaredcrates/trios-*submodules.R-rules compliance
.vfiles touched; this is an infra fix.fb0a997.Anchor:
phi^2 + phi^-2 = 3· DOI 10.5281/zenodo.19227877.