Skip to content

Wave-9c: Expand 5 thinnest PhD chapters to ≥1000 LoC #796

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
gHashTag wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Wave-9c: Expand 5 thinnest PhD chapters to ≥1000 LoC #796

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
209 changes: 209 additions & 0 deletions docs/phd/artifacts/coq_citation_map.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,209 @@
{
"_metadata": {
"schema_version": "1.0.0",
"created_by": "Wave-9c thin-chapter expansion",
"anchor": "phi^2 + phi^-2 = 3 (INV-22)",
"zenodo_doi": "10.5281/zenodo.19227877",
"defense_date": "2026-06-15",
"description": "Maps theorems proved in the Wave-9c chapter expansions to their Coq counterparts in t27/proofs/canonical/"
},
"entries": [
{
"id": "FA00_INV22",
"chapter": "flos_00",
"chapter_number": 0,
"latex_label": "fa_00:thm:trinity-identity-prologue",
"statement": "phi^2 + phi^{-2} = 3",
"coq_file": "trinity-clara/proofs/igla/lucas_closure_gf16.v",
"coq_lemma": "INV22_trinity_identity",
"proof_status": "Qed",
"runtime_invariant": "INV-22",
"runtime_check": "crates/trios-igla-race/src/invariants.rs",
"wave": "wave-9c",
"r14_note": "Pre-existing invariant INV-22; documented in flos_00 expansion"
},
{
"id": "FA00_CLOSURE_SQUARING",
"chapter": "flos_00",
"chapter_number": 0,
"latex_label": "fa_00:lem:closure-squaring",
"statement": "For any n + m*phi in Z[phi], (n+m*phi)^2 in Z[phi]",
"coq_file": "trinity-clara/proofs/igla/lucas_closure_gf16.v",
"coq_lemma": "lucas_ring_closure_sq",
"proof_status": "Qed",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "New theorem documented in flos_00 expansion; no new runtime invariant"
},
{
"id": "FA00_LUCAS_FIB",
"chapter": "flos_00",
"chapter_number": 0,
"latex_label": "fa_00:lem:lucas-fibonacci",
"statement": "L_n = F_{n-1} + F_{n+1} for all n >= 0",
"coq_file": "trinity-clara/proofs/igla/lucas_closure_gf16.v",
"coq_lemma": "lucas_fib_sum",
"proof_status": "Admitted",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Standard identity; Admitted pending full Coq proof"
},
{
"id": "FA00_POWER_SUM",
"chapter": "flos_00",
"chapter_number": 0,
"latex_label": "fa_00:prop:power-sum",
"statement": "phi^n + psi^n = L_n for all integers n",
"coq_file": "trinity-clara/proofs/igla/lucas_closure_gf16.v",
"coq_lemma": "phi_power_sum_lucas",
"proof_status": "Admitted",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Binet-formula corollary; Admitted pending Coq Reals library extension"
},
{
"id": "CH31_TMAC_OVERFLOW",
"chapter": "flos_65",
"chapter_number": 31,
"latex_label": "ch31:thm:tmac-overflow",
"statement": "|TMAC(w, x)| <= d*B < 2^15 for d<=256, B<=127",
"coq_file": "t27/proofs/canonical/hw/tmac_spec.v",
"coq_lemma": "tmac_overflow_bound",
"proof_status": "Qed",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Part of hw/ family (35 Qed). No new runtime invariant."
},
{
"id": "CH31_ENCODING_LOSSLESS",
"chapter": "flos_65",
"chapter_number": 31,
"latex_label": "ch31:thm:encoding-lossless",
"statement": "dec(enc(w)) = w for all w in {-1,0,+1}",
"coq_file": "t27/proofs/canonical/hw/trit_encoding.v",
"coq_lemma": "trit_enc_dec_id",
"proof_status": "Qed",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Part of hw/ family. Documented in flos_65 expansion."
},
{
"id": "CH31_PIPELINE_LATENCY",
"chapter": "flos_65",
"chapter_number": 31,
"latex_label": "ch31:lem:pipeline-latency",
"statement": "TMAC depth-8 pipeline produces output exactly 8 cycles after input",
"coq_file": "t27/proofs/canonical/hw/tmac_spec.v",
"coq_lemma": "pipeline_latency_inv",
"proof_status": "Qed",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Part of hw/ family. Documented in flos_65 expansion."
},
{
"id": "CH32_FRAME_BOUNDARY",
"chapter": "flos_66",
"chapter_number": 32,
"latex_label": "ch32:thm:frame-boundary",
"statement": "Spurious 0xAA bytes in payload cannot cause premature IDLE transition",
"coq_file": "t27/proofs/canonical/hw/uart_v6.v",
"coq_lemma": "uart_v6_frame_boundary_unique",
"proof_status": "Admitted",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Admitted; formal Coq model of UART automaton is future work (Ch.32 \u00a7Future)"
},
{
"id": "CH32_ZERO_DRIFT",
"chapter": "flos_66",
"chapter_number": 32,
"latex_label": "ch32:prop:zero-drift",
"statement": "phi-sync maintains zero exponent drift under no frame errors",
"coq_file": "t27/proofs/canonical/hw/uart_v6.v",
"coq_lemma": "phi_sync_zero_drift",
"proof_status": "Admitted",
"runtime_invariant": "phi_exponent_sync",
"runtime_check": "crates/trios-igla-race/src/invariants.rs",
"wave": "wave-9c",
"r14_note": "New runtime invariant: phi-exponent synchronisation. Added to coq_citation_map by Wave-9c per R14."
},
{
"id": "CH32_PERIOD_OPTIMAL",
"chapter": "flos_66",
"chapter_number": 32,
"latex_label": "ch32:thm:period-optimal",
"statement": "phi-sync period P=3 minimises drift subject to overhead <= 1/3",
"coq_file": "t27/proofs/canonical/hw/uart_v6.v",
"coq_lemma": "phi_sync_period_optimal",
"proof_status": "Admitted",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Mathematical optimality result; no runtime invariant added."
},
{
"id": "CH33_FXLOAD_TRANSITION",
"chapter": "flos_67",
"chapter_number": 33,
"latex_label": "ch33:thm:fxload-transition",
"statement": "flash_no_sudo.sh transitions cable from PID 0x0013 to 0x0008 in 1.3+-0.2 s",
"coq_file": "none",
"coq_lemma": "none",
"proof_status": "empirical",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Hardware procedure; no Coq proof required. Documented for completeness."
},
{
"id": "CH33_NO_KEXT",
"chapter": "flos_67",
"chapter_number": 33,
"latex_label": "ch33:prop:no-kext",
"statement": "BLK-001 resolution requires no kernel extension or SIP modification",
"coq_file": "none",
"coq_lemma": "none",
"proof_status": "empirical",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Operational claim; no Coq formalisation required."
},
{
"id": "CH34_3000X",
"chapter": "flos_68",
"chapter_number": 34,
"latex_label": "ch34:thm:3000x",
"statement": "DARPA IGTC task-normalised ratio >= 3000 for Trinity vs A100",
"coq_file": "none",
"coq_lemma": "none",
"proof_status": "empirical",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Empirical claim backed by hardware measurement + DARPA IGTC normalisation. No Coq invariant."
},
{
"id": "CH34_ZERO_ABSORPTION",
"chapter": "flos_68",
"chapter_number": 34,
"latex_label": "ch34:lem:zero-absorption",
"statement": "w_i * x_i = 0 for w_i = 0, all x_i in Z",
"coq_file": "t27/proofs/canonical/kernel/trit_mul_zero_l.v",
"coq_lemma": "trit_mul_zero_l",
"proof_status": "Qed",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "Pre-existing KER-8 Qed. Documented in flos_68 expansion."
},
{
"id": "CH34_ENERGY_SPARSITY",
"chapter": "flos_68",
"chapter_number": 34,
"latex_label": "ch34:thm:energy-sparsity",
"statement": "Dynamic power <= (1 - s(w)) * P_dense for sparsity s(w)",
"coq_file": "none",
"coq_lemma": "none",
"proof_status": "semi-formal",
"runtime_invariant": "none",
"wave": "wave-9c",
"r14_note": "CMOS power model argument; not formalisable in Coq without hardware model."
}
]
}
Loading
Loading