Reciprocal Mersenne Subseries

Observation 5.17 (Exact low-row values). At row $n=14$: $\mathrm{rem}(14)=392$, with take set $D_{14}=\{2,3,6,7\}$. At row $n=15$: $\mathrm{rem}(15)=34333$. At row $n=32$: $\mathrm{rem}(32)=3865046005$ and ${\mathrm{\Delta }}_{32}=-429921291$.
Source: the values at rows $14$–$31$ are proved in Lean by direct evaluation (Theorem 6.10), which uses them to verify the band-escape condition for reset indices $13\le d\le 30$ seamUpperResetDyadicBandEscape_through_thirty. The two ranges differ by one: the remainder used for reset $d$ is at row $d+1$. The take set $D_{14}$, $\mathrm{rem}(32)$ and ${\mathrm{\Delta }}_{32}$ are exact integer computations with the greedy rule of Section 5.4.

Observation 5.18 (Depths of the reported computations). The quotient identity (Theorem 5.14) is verified at rows $6\le n\le 200$ with zero mismatches (saved run), and the quotient-greedy orbit itself is certified row by row to row $2500$ (saved run) and through the exact branch recursion to row $\mathrm{200,000}$ (saved run; branch counts $\mathrm{R}:\mathrm{M}:\mathrm{U}=100197:49899:49898$, the target inequality failing at exactly one reset row $6\le r\le \mathrm{200,000}$, namely $r=7$).

Observation 5.19 (Four computations side by side). Four related computations are reported, with different targets or integer representations, at the following ranges: truncation rung $J=3,\dots ,22$ (all $20$ rungs proved to survive, not merely computed); quotient row $6\le n\le 2500$ (Theorem 5.14 and the branch data underlying Theorem 5.16); integer margin scan to $m_c=5\times {10}^5$ (an exploratory scan, which is not certified); sharp tail margin, ranks $2$ through $3000$ (no fatal skip at any rank; take fraction $0.4992$; tightest certified take-margin $0.0340$ bits at rank $7$, the near-tie $1/126\ge 1/127$).
Use: truncated weights define a different greedy problem, and the quotient-row construction uses integer weights rather than the original real weights. These are not automatically four readings of the same decision stream. Their relevance to full-weight membership comes from the approximation, limit, or identification theorems cited for each construction. A certificate at one range does not transfer to another without such a theorem, and these reports do not decide the universal problem.