(git-record date, not publication date)
completed
kernel-checked
primary investigation
verified
Six of seven boxParts fields already had zero-sorry enclosure lemmas; Retention.imNum_mem now supplies the seventh, so both O9 composition lemmas instantiate at a box, and discharging them exposed that O9Seam.r_comp_mem writes the wrong denominator and is vacuous at every box in the table.
hunts/r_6c7d6a (Record 31 of 98 in chronological sequence)
Guiding Question
Can every numerator-side boxParts field of the O9 two-dimensional checker be given a zero-sorry enclosure lemma, so that the qreIv and rIv composition lemmas can be instantiated at a box?
Method & Verification
imNum_mem is the product of imNumOverY and Y with the component left abstract, then every hypothesis of qreIv_mem and rIv_mem is discharged at one box, which is what exposed the denAbs2 mismatch in r_comp_mem.
Lineage & Relationships
Primary Sources (at pin 8fa46e134)
Editorial Notes
Case-log status is settled, and one defect found on the way. Disposition maps settled to completed. The brief's premise that the numerator side was missing was stale: commit 6f81078 had already landed reNum_mem and imNumOverY_mem.
Date Provenance
commit 32ac356e281391318e901ce17fbfdda3ce1485c2, hunts/r_6c7d6a/RESULTS.md, author 2026-08-17T01:43:38Z