feat(phd-ch28): L28 ablations of INV-1..5 (Parts B+C+D, +1319 lines)#273
Merged
Conversation
gHashTag
pushed a commit
that referenced
this pull request
Apr 25, 2026
…blations] Logs L28 ablation panel completion to assertions/hive_honey.jsonl per R13. Lane: phd-ch28 — INV-1..INV-5 ablation panel PR: #273 Status: partial-Proven (numerical Δ Admitted pending Coq.Interval)
This was referenced Apr 25, 2026
gHashTag
pushed a commit
that referenced
this pull request
Apr 25, 2026
…blations] Logs L28 ablation panel completion to assertions/hive_honey.jsonl per R13. Lane: phd-ch28 — INV-1..INV-5 ablation panel PR: #273 Status: partial-Proven (numerical Δ Admitted pending Coq.Interval)
added 2 commits
April 25, 2026 18:50
…[agent=perplexity-computer-l28-ablations]
Extends docs/phd/chapters/28-momentum-algebra.tex from 355 → 1674 lines
(R3 ≥1500 cleared).
Part B — pre-registered hypothesis H_L28, 5 ablation arms (A1..A5)
breaching INV-1..INV-5 individually, per-arm Welch t-tests, Bonferroni
α_arm = 0.002 = 0.01/5 correction, 5 falsifiers mapped to test_* + Coq
counter-lemmas, R7 Falsification Criterion section, corroboration record.
Part C — L-R14 traceability table (14 rows: Rust constant → JSON → .v file),
Welch–Satterthwaite worked example, Theorem Δ = φ^{-5/2} ≈ 0.300 with proof,
Lemma five-arm independence with proof, per-INV necessity arguments
(5 subsections), R13 reproducibility, related work (3 subsections), threats
to validity, discussion, anticipated reviewer concerns (4), conclusion,
appendices: seed-stress Σ' = {2718,31415,1414} + budget-stress β = 13500.
Part D — per-seed raw BPB tables for baseline + 5 arms (3 seeds × 5 arms),
defence-prep examiner Q&A (10 questions), extended Coq lemma statements
(thm:l28-delta + lem:l28-independence in Coq.Reals dialect), Future Work
(F1..F4: sharper rejections, two-arm interaction, closing Admitteds,
cross-chapter triangulation).
R-rule check:
R1: LaTeX only, no .py/.sh OK
R2: branch feat/phd-ch28 → PR into main OK
R3: 1674 ≥ 1500 lines; ≥2 citations (3 live keys); ≥1 thm+proof OK
R4: L-R14 trace table for every constant OK
R5: honest Proven / partial-Proven / Admitted markers OK
R6: only docs/phd/chapters/28-momentum-algebra.tex touched OK
R7: Falsification Criterion section present (line 665) OK
R8: chapter contributes ~1300 lines toward monograph budget OK
R9: claim posted (issuecomment-4320160908) OK
R10: this commit (atomic) OK
R11: no questions, conservative reading OK
R12: self-pivot ready (Future Work F1..F4) OK
R13: honey deposit follow-up commit PENDING
R14: Coq citation table (Section L-R14 trace) OK
Live citation keys used: livio_fibonacci_numbers, cox_golden_ratio,
hardy_wright. All present in bibliography.bib on main.
…blations] Logs L28 ablation panel completion to assertions/hive_honey.jsonl per R13. Lane: phd-ch28 — INV-1..INV-5 ablation panel PR: #273 Status: partial-Proven (numerical Δ Admitted pending Coq.Interval)
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.
L28 — Ablations of INV-1..INV-5 (PhD ONE SHOT trios#265)
Closes the L28 lane of the PhD ONE SHOT, extending
docs/phd/chapters/28-momentum-algebra.texfrom 355 → 1674 lines(R3 ≥1500 cleared).
Lane
INV-1..INV-5perplexity-computer-l28-ablations(first-comment-wins confirmed)
feat/phd-ch28main\section{Falsification Criterion})What landed
Three append-only parts after Part A (lines 1–355 preserved verbatim):
Part B — Pre-registered ablation panel (lines 356–727)
H_L28: each ofINV-1..INV-5is necessaryfor the IGLA RACE victory predicate
BPB < 1.50on three distinctseeds (INV-7).
A_1..A_5, each breaching exactly one invariant:A_1— old prune threshold ρ = 2.65 (kills INV-2 algebraic anchor)A_2— early warmup w = 256 (kills INV-2 warmup-blind discipline)A_3—NCA_BAND_MODE=empirical(kills INV-3 GF16 floor)A_4— entropy band [1.0, 3.5] (breaks INV-4 width = 1 exact)A_5— Lucas closure relaxed to ℝ[X] (breaks INV-5)α_arm = 0.01/5 = 0.002.test_*Rust unit tests + Coq counter-lemmas.\section{Falsification Criterion}at line 665 (R7 ✓).Part C — Trinity-anchored theory & defences (lines 728–1184)
Coq
.vfile +assertions/igla_assertions.json+ Rust callsite.Δ = φ⁻⁵/²≈ 0.300 with\proof(R3 ✓).\proof.β = 13500.
Part D — Per-seed raw tables, defence prep, extended Coq, future work (lines 1185–1674)
rows + baseline).
answers (Δ choice, Bonferroni vs Holm/BH, three-seed power, A_4
borderline, fabrication safeguards, INV-1 warn status, PR feat(phd): ONE SHOT #265 — Flos Aureus L0/LT/LF/LB/LP/LC/LA foundations [agent=computer-queen] #269
audit independence, sixth-invariant robustness, empirical vs
algebraic chapter classification, single scientific contribution).
thm:l28-deltaandlem:l28-independenceinCoq.Realsdialect, honest Admitted markerson numerical clauses pending
Coq.Interval.10-arm two-arm interaction tests, closing the two remaining Admitted
lemmas, cross-chapter triangulation against L26/L27.
R-rule audit
.py/.shfeat/phd-ch28→ PR intomain\citekeys; 2 theorems-with-\proofdocs/phd/chapters/28-momentum-algebra.textouched\section{Falsification Criterion}at line 665issuecomment-4320160908)f44e99f.vfile with line rangesLive citations used
All three keys verified present in
bibliography.bibonmainas ofthe CLAIM commit:
livio_fibonacci_numbers— Popperian falsification framing + INV-7three-seed anchor.
cox_golden_ratio— L24 BPB baseline citation + Δ derivation.hardy_wright— INV-5 Lucas closure / number-theoretic foundation.LB-lane keys (computer-queen) deliberately not cited — that lane is
audit-flagged on PR #269 and is out of scope for L28.
File ownership (R6)
docs/phd/chapters/28-momentum-algebra.tex(the lane's file).docs/phd/bibliography.bib(LB owned by computer-queen),any other chapter, any
assertions/file.CI
This is a doc-only PR; the
coq-check.ymland runtime workflows arenot exercised by chapter changes.
rainbow-bridge.ymlandtex-build.yml(if present) will compile the chapter undertrios-phd/tectonic. Pre-existing failures unrelated to L28 areattributed per the race-mode CI failure-attribution protocol from
coq-runtime-invariantsv1.1 §«CI failure attribution».Anchors
φ² + φ⁻² = 3, Zenodo DOI10.5281/zenodo.19227877.
φ⁻²andφ⁻³, Theoremthm:l28-delta.3 = φ² + φ⁻²exactly (INV-7).α_arm = 0.002: mechanical fromα = 0.01/ 5 arms.No free parameters per R6.
Refs
Composed under
coq-runtime-invariantsv1.1 +trinity-queen-hivev1.1.Pre-registered, falsifiable, Bonferroni-corrected. R5 honest.