Definition is a well-formed non-degenerate Prop (two-sided window, N-truncated subtraction coherent); mathlib names only, type-checks.

Referee-commissioned independent blind review (Fable-5). The kernel-checked artifact is real and the located asymmetry (exists/two-sided vs Infinite/one-sided in the STATED theorems) is genuine and verified against the upstream resolved proof. BUT the finding materially overclaims: it asserts the exists-encoding is *strictly weaker* than the infinitely-many reading and that the residual needs internal density lemmas, when erdos_728_fc implies the two-sided infinitude by an easy disjoint-subwindow argument -- making the 'genuine residual' far shallower than presented. Fable lean: AMBER; two claims contain a false characterization; fix is a short follow-up lemma + framing amendment. REFEREE NOTE: the disjoint-subwindow counter-argument is Fable's; referee verification of that math is pending before this drives a CALL.