Two dyadic floor sequences

../

evidence/: Finite data of the Problem 354 reconstructions rechecked by one entry point: the Yu--Chen mask certificate and the Salem polynomial evaluations of Geneson's Theorem 9.

fan_remark_4_1_reconstruction: Reconstructs the example showing one element per dyadic interval does not suffice: the set of numbers one more than a power of two has divergent distance sums and is incomplete, so the sharp dyadic threshold is at least two; combined with Corollary 1.2 it lies between two and five.

fan_remark_4_2_reconstruction: Reconstructs the reduction of Hegyvári's two-ray conjecture to the sharp dyadic threshold: the nonzero dyadic floors of two reals with ratio not a power of two, one of them not a dyadic rational, have two elements in every large dyadic interval and divergent distance sums.

geneson_corollary_12_reconstruction: Reconstructs the two-coefficient example at the Salem base of Theorem 9: both floor sequences are entirely even, the coefficient ratio is not a rational multiple of a power of the base, so the ratio is irrational, neither sequence is a tail of the other, and the interleaving is incomplete.

geneson_theorem_9_reconstruction: Reconstructs the sign adjustment of Dubickas's fractional-part theorem and its application to one Salem number between 6/5 and 13/10, giving arbitrarily large coefficients whose floor sequence is entirely even and hence incomplete.

yu_chen_bg_reconstruction: Reconstructs the final counting argument: on a sparse window, exact layers are dense, every nontrivial return between exact layers costs many events by compactness of ratios of sparse binary sums, and a geometric chain of returns exceeds the event budget.

yu_chen_db_reconstruction: Reconstructs the window lemma (a represented interval wide enough against a good rational approximant of the ratio forces completeness) and the digit-budget inequality it yields for incomplete sequences.

yu_chen_fe_reconstruction: Reconstructs the estimate that the number of unrepresented positions below the next weight decays exponentially in the number of events, through a boundary-variation bound at nonzero conversions and a two-step potential, and the contiguous-run lower bound it implies.

yu_chen_lemma_2_1_reconstruction: Reconstructs the cyclic-run identity: adjoining the one-step translate of a nonempty residue set shortens its longest missing run by exactly one.

yu_chen_lemma_2_2_reconstruction: Reconstructs the mesh lemma: a finite integer set whose span is at least the added weight keeps its gap bound and grows its span by that weight, hence indefinitely under weights growing by at most doubling.

yu_chen_lemma_2_3_reconstruction: Reconstructs the projection lemma: an integer mesh of gap at most k and span at least m leaves no run of k or more missing residues modulo m.

yu_chen_normalization_reconstruction: Reconstructs the dyadic rescaling to interlaced tails with N < M < 2N, the digit recurrences, the infinitude of events, the fixed prefix bounds, and the reduction of strong completeness to completeness of the tails.

yu_chen_theorem_5_1_reconstruction: Reconstructs the exact-block mesh construction, the finite coefficient certificate it needs, and the theorem that a long exact doubling block followed by a nonzero conversion lowers the modular gap invariant of every later layer by one.

yu_chen_theorem_reconstruction: Reconstructs the assembly of the strong-completeness theorem: normalize, derive bounded event spacing from permanent descent under incompleteness, contradict it with the sparse-window counting, and transfer completeness of the tails back to the original set minus any finite deletion.

yu_chen_windows_reconstruction: Reconstructs the construction, for an incomplete normalized pair with irrational ratio, of arbitrarily long layer windows on which the events are logarithmically few, a low-height rational approximates the ratio, and the approximation residues stay below a power of two.

---

This folder holds author-recorded reconstructions of the source proofs that bear on Problem 354, whose dated assessment lives on that page. Each page names its held artifact with physical pages and result labels, restates the result with its hypotheses, and writes out the essential deductions in the corpus's own words, labeling what is imported and what is omitted. None of the pages is an independent review; none changes a status or assigns a tier.

The Yu--Chen manuscript (unrefereed, 13 September 2026), which claims strong completeness of the nonzero dyadic floors of two reals with irrational ratio, is reconstructed section by section. Read the theorem page first; it assembles the argument from the normalization and reduction, the three finite lemmas (2.1, 2.2, 2.3), the exact-block and permanent-descent Theorem 5.1 with its finite certificate, the finite-event decay, the digit budget, the sparse windows and the bounded-spacing contradiction. The Fan preprint's Remark 4.2 and Remark 4.1 at base two and the Geneson preprint's Theorem 9 and Corollary 12 are reconstructed on their own pages. The evidence rechecks the two finite inputs: the Yu--Chen mask certificate and the Salem polynomial evaluations.

Where things stand

Reviewed. Each reconstruction page was independently reviewed, as it stood at 2026-09-28T05:03:27Z, by a focused review filed under evidence/verify/, with a distinct grade of the fourteen reviews. As the grade records them, the verdicts are: Fan Remark 4.1, fidelity faithful with corrections C1 and C2 and argument sound; Fan Remark 4.2, fidelity faithful and argument sound with correction C3; Geneson Corollary 12, fidelity faithful with correction C5 and argument sound; Geneson Theorem 9, fidelity faithful with correction C4 and argument sound; the Yu--Chen bounded-spacing contradiction, fidelity faithful with correction C9 and argument sound; the digit budget, fidelity faithful and argument sound with corrections C7 and C8; the finite-event decay, fidelity faithful and argument sound; Lemma 2.1, fidelity faithful and argument sound; Lemma 2.2, fidelity faithful and argument sound; Lemma 2.3, fidelity faithful and argument sound; the normalization, fidelity faithful and argument sound; Theorem 5.1, fidelity faithful and argument sound with correction C6; the theorem page, fidelity faithful and argument sound with correction C10; the sparse windows, fidelity faithful and argument sound. All fourteen reviews were graded pass; none was graded void. The corrections C1--C10 were applied, so the current text differs from the reviewed text at the places the grade names: the Source paragraph of the Remark 4.1 page (C1, C2); Step 1 of the Remark 4.2 page (C3); the Scope paragraph of the Theorem 9 page (C4) and of the Corollary 12 page (C5); Step 4 of the Theorem 5.1 page (C6); Steps 1 and 3 of the digit-budget page (C7, C8); the three step headings of the bounded-spacing page (C9); and Step 4 of the theorem page (C10). No tier is assigned and the problem's status is unchanged. After the review, line wrapping was normalized on the reconstruction pages; no formula or sentence changed.

First question (base 2). The problem page records the first question as answered yes on a bounty site's accepted Lean proof, with the stated qualifications. The Yu--Chen manuscript claims the stronger conclusion that the value set stays complete after every finite deletion. Its argument is now written out here at the author-recorded level, with one external input (Dirichlet's approximation theorem, imported on the windows page) and one finite input (the Appendix A certificate, rechecked by the evidence). Where the source states a step without proof (the interlacing of the normalized tails, the phase mesh and window overlap in the digit budget, the arc covering in the decay estimate, the descent bookkeeping in the event-spacing step) the pages supply the deduction; the reconstruction closed every step it examined, which is an author-recorded finding and not a review verdict. The source's Lean formalization was neither built nor read. Nothing here changes the problem's status.

Second question (base $\gamma\in(1,2)$). Its reading, "for some" or "for every" $\gamma$, is still unfixed. Under "for every $\gamma$", Geneson's Corollary 12 (reconstructed) answers no at one Salem base in $(6/5,13/10)$: both floor sequences are entirely even, so no odd integer is a sum; the coefficients exist by Dubickas's fractional-part theorem (imported, its paper not held) and are not explicit. What that reading still needs is acceptance evidence for the preprint and, mathematically, nothing more. Under "for some $\gamma$", what is needed is one base in $(1,2)$ at which every pair with irrational ratio gives a complete interleaving; the only candidate on the problem page is an unreviewed Lean claim at $\gamma=\sqrt\varphi$ in which the single sequence $\lfloor\gamma^n\alpha\rfloor$ is already complete for every $\alpha$, and it needs review. The rational-ratio cases of Hegyvári's base-2 conjecture remain untouched by every source here; Remark 4.2 shows they would follow from the sharp threshold $M_2^*=2$, and the reconstructed Remark 4.1 gives only $2\le M_2^*\le5$.

Mechanism. The Yu--Chen mechanism has two scales: a modular gap invariant on the subset sums modulo $\gcd(a_n,b_n)$ that a long exact doubling block followed by a nonzero digit lowers permanently (a finite certificate of six-weight representations makes the descent uniform in the layer), and a potential argument showing the count of unrepresented positions decays exponentially in the number of digit events, which together with Dirichlet approximation of the ratio and the compactness of ratios of sparse binary sums turns bounded event spacing into a contradiction.