The original quantified Nishibuchi conjecture is completed. The stronger dyadic result applies without a starting-row threshold, and the rank-four theory now has factorial precision, exact common-step laws for addresses zero and one, an infinite exact address-two family, optimal periods, and exact analytic radii for three addresses.
For a common step, the final congruence to use is
with
For different steps, replace \(k v_2(H)\) by \(\sum_i v_2(H_i)\) in the lower bound. The address-zero/one equality rule then depends on order parity and the number of even steps.
| Statement | Final status |
|---|---|
| Nishibuchi Conjecture 3.9, all allowed branches | completed; formal capstone |
| All-row dyadic mixed-difference bound | proved and audited |
| Rank-four factorial and paired bounds | proved and audited |
| All common-step exact valuations, \(j=0,1\) | proved at all rows and orders |
| Address-two exact valuations at power-of-two orders | proved for all positive step lists |
| Complete exact address-two formula at other orders | open |
| Complete exact higher-order address-three formula | open |
| Exact address-three analytic radius | open |
| Simple constant metric at every upper-half address | false; exact witnesses retained |
| Separate Euler-tail universal simplicity problem | open; a distinct research program |
The remaining questions do not weaken the completed conjecture. They specify the next boundary of the stronger theory. The main paper gives the proofs and precise dependency statements, while the Lean guide supplies the formal coverage map and a reproducible route to its recorded checks.