diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index 8ba89497e3..197e0a5bea 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -5045,3 +5045,78 @@ had not. reach for while using it**, and those are where a wrong list quietly becomes a wrong plan. The tell was the classification coming out nonsensical — zero training assertions in a file that is mostly training assertions. + +## 125. "The most recent N" cannot answer "has X happened since T" + +I opened an issue asserting a repository-wide CI outage: *required checks have +not fired since 2026-08-24 11:06; every PR since is permanently BLOCKED.* It had +a measurement, a five-row table of refuted hypotheses, and a sharp closing +observation. **It was wrong.** The checks had not started yet. Twenty minutes +later both branches showed 30+ checks. + +Two instrument errors compounded, and neither was visible from inside the +conclusion. + +### `gh run list --limit N` is a recency window + +The last 10, then 60, runs were dominated by two workflows that fire on every +push. I read *"the only workflows running are NotebookLM"* off a list that had +simply not reached back far enough. The API's own filter says otherwise: + +``` +gh api "repos/…/actions/runs?created=>2026-08-25" → 103 runs + pull_request: 39 push: 31 schedule: 14 issues: 10 +``` + +**A query that returns the most recent N cannot answer a question about a time +range.** It answers "what is newest", and if something noisy is newest, +everything else is invisible at any N you are willing to read. + +### I queried the wrong workflow and believed the answer + +`--workflow=now-sync-gate.yml` returned runs ending 08-24, which I took as *"the +required check stopped firing"*. The required context `check-now-freshness` is +produced by **two** files, and the run that satisfies it displays as +**"Check Now Freshness"** — a name I never searched for, because I had gone +looking by filename. + +One file answered honestly. The check came from somewhere else. + +### The shape of the error + +Every row of my "what is NOT the cause" table was **correct**. Actions enabled, +workflows active, files present, no branch filter, no path filter, identical +trigger on a workflow that did run. I eliminated hypotheses carefully and +thoroughly — around a premise I never tested. + +**A well-run elimination over a false premise produces more confidence than a +sloppy one.** The table was what made the issue persuasive, including to me. + +### What would have caught it, and it is embarrassing + +Waiting. The difference between "has not started" and "will never start" is +time, and nothing else. I had already written §116's lesson — *prefer the answer +with more structure* — and the structured answer here was available the whole +time: `created=>` returns a range, `--limit` returns a window. + +The check that costs nothing: **before reporting an absence, ask the same +question with a different instrument.** Not a second opinion on the conclusion — +a second instrument for the observation. + +### One thing in it was true and worth keeping + +`gh pr checks` on a PR whose checks have not started shows a short **green** +list: two successes, zero failures, indistinguishable at a glance from a PR that +passed thirty-three gates. Both of the workflows I wrongly accused carry a +comment saying exactly that — *"An absent check is not a passing check"* — which +is why the outage reading was plausible enough to write down. + +The hazard is real. The outage was not. **A true observation is not evidence for +the theory it made you think of.** + +### Withdrawal is cheap; a standing wrong issue is not + +Closed within the hour with the correction as the closing comment, because the +issue named an owner action that did not exist. The campaign rule stands: a +finding that survives a genuine attempt to kill it is worth acting on, and I +never attempted to kill this one — I only attacked its alternatives. diff --git a/.trinity/icarus-baselines/specs/scratch/w743_bench_module_305x2p6_aos_var_call_write.json b/.trinity/icarus-baselines/specs/scratch/w743_bench_module_305x2p6_aos_var_call_write.json deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w744_bench_module_307x2p6_aos_var_call_write.json b/.trinity/icarus-baselines/specs/scratch/w744_bench_module_307x2p6_aos_var_call_write.json deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w745_bench_module_309x2p6_aos_var_call_write.json b/.trinity/icarus-baselines/specs/scratch/w745_bench_module_309x2p6_aos_var_call_write.json deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w746_bench_module_311x2p6_aos_var_call_write.json b/.trinity/icarus-baselines/specs/scratch/w746_bench_module_311x2p6_aos_var_call_write.json deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w747_bench_module_313x2p6_aos_var_call_write.json b/.trinity/icarus-baselines/specs/scratch/w747_bench_module_313x2p6_aos_var_call_write.json deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w748_bench_module_315x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w748_bench_module_315x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w749_bench_module_317x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w749_bench_module_317x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w750_bench_module_319x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w750_bench_module_319x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w751_bench_module_321x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w751_bench_module_321x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w752_bench_module_323x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w752_bench_module_323x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w753_bench_module_325x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w753_bench_module_325x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w754_bench_module_327x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w754_bench_module_327x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w755_bench_module_329x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w755_bench_module_329x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w756_bench_module_331x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w756_bench_module_331x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w757_bench_module_333x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w757_bench_module_333x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w758_bench_module_335x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w758_bench_module_335x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w759_bench_module_337x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w759_bench_module_337x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w760_bench_module_339x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w760_bench_module_339x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w761_bench_module_341x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w761_bench_module_341x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w762_bench_module_343x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w762_bench_module_343x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/.trinity/icarus-baselines/specs/scratch/w763_bench_module_345x2p6_aos_var_call_write.t27.baseline b/.trinity/icarus-baselines/specs/scratch/w763_bench_module_345x2p6_aos_var_call_write.t27.baseline deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/G2_ALPHA_S_PHI_FRAMEWORK_V0.9.out b/G2_ALPHA_S_PHI_FRAMEWORK_V0.9.out deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/anstream-c1e9c0c395f80442/lib-anstream b/bootstrap/target/release/.fingerprint/anstream-c1e9c0c395f80442/lib-anstream deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/anstyle-parse-160e2b59465bf648/lib-anstyle_parse b/bootstrap/target/release/.fingerprint/anstyle-parse-160e2b59465bf648/lib-anstyle_parse deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/block-buffer-5afc0003f14d9ddc/lib-block_buffer b/bootstrap/target/release/.fingerprint/block-buffer-5afc0003f14d9ddc/lib-block_buffer deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/chrono-49af8085456de354/lib-chrono b/bootstrap/target/release/.fingerprint/chrono-49af8085456de354/lib-chrono deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/clap_builder-64f70f2ab4de4a3a/lib-clap_builder b/bootstrap/target/release/.fingerprint/clap_builder-64f70f2ab4de4a3a/lib-clap_builder deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/crypto-common-13f10a8487e4fc9a/lib-crypto_common b/bootstrap/target/release/.fingerprint/crypto-common-13f10a8487e4fc9a/lib-crypto_common deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/digest-8a6dfe029a140daa/lib-digest b/bootstrap/target/release/.fingerprint/digest-8a6dfe029a140daa/lib-digest deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/generic-array-5bf520dd5d207bca/lib-generic_array b/bootstrap/target/release/.fingerprint/generic-array-5bf520dd5d207bca/lib-generic_array deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/num-traits-a7b530d9de63d080/lib-num_traits b/bootstrap/target/release/.fingerprint/num-traits-a7b530d9de63d080/lib-num_traits deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/bootstrap/target/release/.fingerprint/zmij-af2b6cfa8862edd8/lib-zmij b/bootstrap/target/release/.fingerprint/zmij-af2b6cfa8862edd8/lib-zmij deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/chips/euler b/chips/euler deleted file mode 160000 index 73b9f0a050..0000000000 --- a/chips/euler +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 73b9f0a050902300a3c29208ac2d493ebc642213 diff --git a/chips/gamma b/chips/gamma deleted file mode 160000 index a90a3d04bc..0000000000 --- a/chips/gamma +++ /dev/null @@ -1 +0,0 @@ -Subproject commit a90a3d04bc50943949b1e77469069b55f4bc6118 diff --git a/chips/phi b/chips/phi deleted file mode 160000 index f5456685c3..0000000000 --- a/chips/phi +++ /dev/null @@ -1 +0,0 @@ -Subproject commit f5456685c3593665153fe2765c85bb1f46ec14c2 diff --git a/docs/now/2026-08-27-a-well-run-elimination-over-a-false-premise.md b/docs/now/2026-08-27-a-well-run-elimination-over-a-false-premise.md new file mode 100644 index 0000000000..dd0d05119d --- /dev/null +++ b/docs/now/2026-08-27-a-well-run-elimination-over-a-false-premise.md @@ -0,0 +1,10 @@ +# NOW -- A well-run elimination over a false premise (2026-08-27) + +## A well-run elimination over a false premise (Refs #2161) + +- Refs #2161. I opened an issue asserting a repository-wide CI outage -- required checks not fired since 2026-08-24, every PR permanently BLOCKED -- with a measurement and a five-row table of refuted hypotheses. It was WRONG. The checks had not started yet; twenty minutes later both branches showed 30+ checks. Closed within the hour +- Two instrument errors compounded. `gh run list --limit N` is a RECENCY WINDOW, not a census: the last 60 runs were all NotebookLM, which fires on every push, so everything else was invisible at any N I was willing to read. The API `created=>` filter returns 103 runs over the same span, 39 of them pull_request +- And I queried by FILENAME. `--workflow=now-sync-gate.yml` returned runs ending 08-24; the required context check-now-freshness is produced by two files, and the run that satisfies it displays as "Check Now Freshness" -- a name I never searched for. One file answered honestly; the check came from elsewhere +- EVERY ROW of my "what is NOT the cause" table was correct. Actions enabled, workflows active, files present, no filters, identical trigger on a workflow that did run. I eliminated hypotheses carefully around a premise I never tested -- and a well-run elimination over a false premise produces MORE confidence than a sloppy one. The table is what made it persuasive, including to me +- The cheap check: before reporting an ABSENCE, ask the same question with a different instrument. Not a second opinion on the conclusion -- a second instrument for the observation. A query returning "the most recent N" cannot answer "has X happened since T" +- One thing in it was true and worth keeping: `gh pr checks` on a PR whose checks have not started shows a short GREEN list, indistinguishable at a glance from a PR that passed 33 gates. Both workflows I wrongly accused carry the comment "An absent check is not a passing check". The hazard is real; the outage was not. A true observation is not evidence for the theory it made you think of diff --git a/proofs/gravity/dl_bounds.vok b/proofs/gravity/dl_bounds.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/gravity/dl_bounds.vos b/proofs/gravity/dl_bounds.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/sacred/gamma_phi3.vok b/proofs/sacred/gamma_phi3.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/sacred/gamma_phi3.vos b/proofs/sacred/gamma_phi3.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/sacred/l5_identity.vok b/proofs/sacred/l5_identity.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/sacred/l5_identity.vos b/proofs/sacred/l5_identity.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/AlphaPhi.vok b/proofs/trinity/AlphaPhi.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/AlphaPhi.vos b/proofs/trinity/AlphaPhi.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Archive_Conjectural.vok b/proofs/trinity/Archive_Conjectural.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Archive_Conjectural.vos b/proofs/trinity/Archive_Conjectural.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_Gauge.vok b/proofs/trinity/Bounds_Gauge.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_Gauge.vos b/proofs/trinity/Bounds_Gauge.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_LeptonMasses.vok b/proofs/trinity/Bounds_LeptonMasses.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_LeptonMasses.vos b/proofs/trinity/Bounds_LeptonMasses.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_Masses.vok b/proofs/trinity/Bounds_Masses.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_Masses.vos b/proofs/trinity/Bounds_Masses.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_Mixing.vok b/proofs/trinity/Bounds_Mixing.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_Mixing.vos b/proofs/trinity/Bounds_Mixing.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_QuarkMasses.vok b/proofs/trinity/Bounds_QuarkMasses.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Bounds_QuarkMasses.vos b/proofs/trinity/Bounds_QuarkMasses.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/CKMCPViolation.vok b/proofs/trinity/CKMCPViolation.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/CKMCPViolation.vos b/proofs/trinity/CKMCPViolation.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/CKM_PMNS_Matrices.vok b/proofs/trinity/CKM_PMNS_Matrices.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/CKM_PMNS_Matrices.vos b/proofs/trinity/CKM_PMNS_Matrices.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/ConsistencyChecks.vok b/proofs/trinity/ConsistencyChecks.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/ConsistencyChecks.vos b/proofs/trinity/ConsistencyChecks.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/CorePhi.vok b/proofs/trinity/CorePhi.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/CorePhi.vos b/proofs/trinity/CorePhi.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/CosmologicalConstant.vok b/proofs/trinity/CosmologicalConstant.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/CosmologicalConstant.vos b/proofs/trinity/CosmologicalConstant.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/DarkMatterPhi.vok b/proofs/trinity/DarkMatterPhi.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/DarkMatterPhi.vos b/proofs/trinity/DarkMatterPhi.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/DerivationLevels.vok b/proofs/trinity/DerivationLevels.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/DerivationLevels.vos b/proofs/trinity/DerivationLevels.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/ExactIdentities.vok b/proofs/trinity/ExactIdentities.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/ExactIdentities.vos b/proofs/trinity/ExactIdentities.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/FormulaEval.vok b/proofs/trinity/FormulaEval.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/FormulaEval.vos b/proofs/trinity/FormulaEval.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/H4Derivations.vok b/proofs/trinity/H4Derivations.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/H4Derivations.vos b/proofs/trinity/H4Derivations.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/H4GaugeEmbedding.vok b/proofs/trinity/H4GaugeEmbedding.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/H4GaugeEmbedding.vos b/proofs/trinity/H4GaugeEmbedding.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/H4Lagrangian.vok b/proofs/trinity/H4Lagrangian.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/H4Lagrangian.vos b/proofs/trinity/H4Lagrangian.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/HiggsFromSpectralAction.vok b/proofs/trinity/HiggsFromSpectralAction.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/HiggsFromSpectralAction.vos b/proofs/trinity/HiggsFromSpectralAction.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/HiggsPotentialH4.vok b/proofs/trinity/HiggsPotentialH4.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/HiggsPotentialH4.vos b/proofs/trinity/HiggsPotentialH4.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/HiggsPrediction.vok b/proofs/trinity/HiggsPrediction.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/HiggsPrediction.vos b/proofs/trinity/HiggsPrediction.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/INV6_H4_Constraint.vok b/proofs/trinity/INV6_H4_Constraint.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/INV6_H4_Constraint.vos b/proofs/trinity/INV6_H4_Constraint.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Koide.vok b/proofs/trinity/Koide.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Koide.vos b/proofs/trinity/Koide.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/NeutrinoMasses.vok b/proofs/trinity/NeutrinoMasses.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/NeutrinoMasses.vos b/proofs/trinity/NeutrinoMasses.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/SMLagrangian.vok b/proofs/trinity/SMLagrangian.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/SMLagrangian.vos b/proofs/trinity/SMLagrangian.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/SpectralAction600Cell.vok b/proofs/trinity/SpectralAction600Cell.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/SpectralAction600Cell.vos b/proofs/trinity/SpectralAction600Cell.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Summary.vok b/proofs/trinity/Summary.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Summary.vos b/proofs/trinity/Summary.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/ThreeGenerations.vok b/proofs/trinity/ThreeGenerations.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/ThreeGenerations.vos b/proofs/trinity/ThreeGenerations.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Tolerances.vok b/proofs/trinity/Tolerances.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Tolerances.vos b/proofs/trinity/Tolerances.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Uniqueness.vok b/proofs/trinity/Uniqueness.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Uniqueness.vos b/proofs/trinity/Uniqueness.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Unitarity.vok b/proofs/trinity/Unitarity.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/Unitarity.vos b/proofs/trinity/Unitarity.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/YukawaConstant.vok b/proofs/trinity/YukawaConstant.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/YukawaConstant.vos b/proofs/trinity/YukawaConstant.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/search_lemma.vok b/proofs/trinity/search_lemma.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/search_lemma.vos b/proofs/trinity/search_lemma.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/search_lemma2.vok b/proofs/trinity/search_lemma2.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/search_lemma2.vos b/proofs/trinity/search_lemma2.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_assert.vok b/proofs/trinity/test_assert.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_assert.vos b/proofs/trinity/test_assert.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_assert2.vok b/proofs/trinity/test_assert2.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_assert2.vos b/proofs/trinity/test_assert2.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_debug_bounds.vok b/proofs/trinity/test_debug_bounds.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_debug_bounds.vos b/proofs/trinity/test_debug_bounds.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_debug_bounds7.vok b/proofs/trinity/test_debug_bounds7.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_debug_bounds7.vos b/proofs/trinity/test_debug_bounds7.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_debug_bounds8.vok b/proofs/trinity/test_debug_bounds8.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_debug_bounds8.vos b/proofs/trinity/test_debug_bounds8.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_debug_bounds9.vok b/proofs/trinity/test_debug_bounds9.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_debug_bounds9.vos b/proofs/trinity/test_debug_bounds9.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_field_exp.vok b/proofs/trinity/test_field_exp.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_field_exp.vos b/proofs/trinity/test_field_exp.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_field_phi3.vok b/proofs/trinity/test_field_phi3.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_field_phi3.vos b/proofs/trinity/test_field_phi3.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_interval_direct2.vok b/proofs/trinity/test_interval_direct2.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_interval_direct2.vos b/proofs/trinity/test_interval_direct2.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_interval_loose.vok b/proofs/trinity/test_interval_loose.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_interval_loose.vos b/proofs/trinity/test_interval_loose.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_interval_pos.vok b/proofs/trinity/test_interval_pos.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_interval_pos.vos b/proofs/trinity/test_interval_pos.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_ratio_loose.vok b/proofs/trinity/test_ratio_loose.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_ratio_loose.vos b/proofs/trinity/test_ratio_loose.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_sm_bounds.vok b/proofs/trinity/test_sm_bounds.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/proofs/trinity/test_sm_bounds.vos b/proofs/trinity/test_sm_bounds.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/research/toda_derivation.json b/research/toda_derivation.json deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/research/trinity-pellis-paper/G2_TRINITY_V1.0_FRAGRANCE.out b/research/trinity-pellis-paper/G2_TRINITY_V1.0_FRAGRANCE.out deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/Avs96Safe.vok b/trios-coq/Physics/Avs96Safe.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/Avs96Safe.vos b/trios-coq/Physics/Avs96Safe.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/ClockGating.vok b/trios-coq/Physics/ClockGating.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/ClockGating.vos b/trios-coq/Physics/ClockGating.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/DataRetention.vok b/trios-coq/Physics/DataRetention.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/DataRetention.vos b/trios-coq/Physics/DataRetention.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/EmergencyShutdown.vok b/trios-coq/Physics/EmergencyShutdown.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/EmergencyShutdown.vos b/trios-coq/Physics/EmergencyShutdown.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/FreqThrottle.vok b/trios-coq/Physics/FreqThrottle.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/FreqThrottle.vos b/trios-coq/Physics/FreqThrottle.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/Hysteresis.vok b/trios-coq/Physics/Hysteresis.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/Hysteresis.vos b/trios-coq/Physics/Hysteresis.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/NullorReversible.vok b/trios-coq/Physics/NullorReversible.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/NullorReversible.vos b/trios-coq/Physics/NullorReversible.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/PowerCapping.vok b/trios-coq/Physics/PowerCapping.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/PowerCapping.vos b/trios-coq/Physics/PowerCapping.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/PowerState.vok b/trios-coq/Physics/PowerState.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/PowerState.vos b/trios-coq/Physics/PowerState.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/PurkinjeThermal.vok b/trios-coq/Physics/PurkinjeThermal.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/PurkinjeThermal.vos b/trios-coq/Physics/PurkinjeThermal.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/SleepGating.vok b/trios-coq/Physics/SleepGating.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/SleepGating.vos b/trios-coq/Physics/SleepGating.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/SparsityMask.vok b/trios-coq/Physics/SparsityMask.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/SparsityMask.vos b/trios-coq/Physics/SparsityMask.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/SpeculativeExit.vok b/trios-coq/Physics/SpeculativeExit.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/SpeculativeExit.vos b/trios-coq/Physics/SpeculativeExit.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/ThermalGuard.vok b/trios-coq/Physics/ThermalGuard.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/ThermalGuard.vos b/trios-coq/Physics/ThermalGuard.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/ThrottleSlew.vok b/trios-coq/Physics/ThrottleSlew.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/ThrottleSlew.vos b/trios-coq/Physics/ThrottleSlew.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/VoltageGuard.vok b/trios-coq/Physics/VoltageGuard.vok deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/trios-coq/Physics/VoltageGuard.vos b/trios-coq/Physics/VoltageGuard.vos deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/vscode-trinity-swe/test_highlight.t27 b/vscode-trinity-swe/test_highlight.t27 deleted file mode 100644 index e69de29bb2..0000000000