bibkey: hu2026vgptrsi authors: Zhixin Hu; Tao Xu; Xiaodian Sun; Li Jin; Momiao Xiong year: 2026 title: VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization doi: null url: https://arxiv.org/abs/2606.15096v1 claim: “The preprint reports checked finite RH-adjacent certificates and explicitly leaves the global Lagarias tail, the full Lagarias equivalence, and any colossally abundant reduction beyond the finite cutoff unresolved; it supplies no transport from a FIB affine family to that tail.” strata_touched: [] license: citation-only triage: anchor
VGPT-RSI finite certificates and the remaining global tail
The source is arXiv:2606.15096v1, submitted 13 June 2026. This card records the abstract-level scope and is not a peer-review, Coq replay, or Lean verification.
The preprint describes two finite certification tasks: an interval-arithmetic certificate for a parameterized safe boundary curve and a Coq-checked finite Lagarias inequality. It explicitly lists three unresolved steps: formalizing the global Lagarias equivalence, proving the tail beyond every finite cutoff, and possibly reducing counterexamples to colossally abundant or related extremal integers.
These certificates therefore do not establish Robin’s inequality for all integers and do not provide a pointwise bound on the affine Fibonacci family
In particular, they do not estimate the same-candidate complete divisor weight or the signed residual required after the single-candidate reduction in §233.5 of the FIB theory. The source is useful as a current frontier boundary, not as a new FIB/RH bridge.