(git-record date, not publication date)
completed
kernel-checked
primary investigation
verified
The two numerator fields answer differently: reNum encloses Re num unconditionally, while imNumOverY encloses Im num / y only for y != 0 and encloses the removable limit at y = 0, and both identifications are proved with zero sorrys and instantiated at the first recorded o9boxes box.
hunts/r_938ab4 (Record 33 of 98 in chronological sequence)
Guiding Question
Do the reals enclosed by reNum_mem and imNumOverY_mem equal Re num and Im num / y, and under what hypotheses?
Method & Verification
O9NumShape.lean identifies the computed interval shapes with Re num and Im num / y under the stated hypotheses, then qreIv_mem_phi2 and rIv_mem_phi2 read the compositions back against Phi2 itself.
Lineage & Relationships
Primary Sources (at pin 8fa46e134)
Editorial Notes
Case-log status is settled, and the two fields answer differently. Disposition maps settled to completed. The dead-weight retirement of r_comp_mem and rIv_mem is a verdict recorded here and executed in r_88dc5e.
Date Provenance
commit 8789d2295539b5064cef7418696bfbae9efac723, hunts/r_938ab4/RESULTS.md, author 2026-08-17T22:19:08Z