Skip to content

PROGRAM_STATUS.md

Latest commit

 

History

History
810 lines (663 loc) · 45.4 KB

PROGRAM_STATUS.md

File metadata and controls

810 lines (663 loc) · 45.4 KB
Raw

PROGRAM_STATUS

Correction — 2026-09-28: constants 17 and 18 are refuted

This correction supersedes the historical “17 is live” claims below. Collatz.Strategy.LogBlockRecord kernel-checks the published seed n = 1008932249296231: its first accelerated descent occurs at step 886, while Nat.log2 n = 49 and 18 * 49 = 882. Thus every integer constant C ≤ 18 in LogBlockDescentWithin C is false. The proposed tail hypothesis above 3998720 is also false for those constants; its conditional implication to Collatz remains logically valid. No bound with constant 19 is proved here.

The seed and stopping time are prior art: Eliahou and Simonetto, arXiv:2107.11160v2, Table 3, and Roosendaal's glide table. The earlier attribution below to O. Rozier is incorrect for this paper. Their jump lengths are recomputed at each jump; their falling-time bound is related to, but not definitionally identical to, a fixed multiple of the initial binary logarithm.

See the attempt report for scope and checks.

Ledger for the seven-program brief. open | refuted | partial | closed.

Repo facts that constrain every entry, checked this session:

  • No Mathlib. lakefile pulls no dependency; core Lean 4 only. by_contra, interval_cases, norm_num, ring, push_neg, set, Nat.find do not exist.
  • No sorry, no added axioms, anywhere in Collatz/. Every theorem below is propext/Quot.sound only.
  • Verified range is 1 086 464, kernel-proved (verified_1086464). Not 2^68. Barina's 704·2^60 is present only as the clearly-marked hypothesis BarinaVerified; results using it are conditional and labelled so.
  • The untracked stubs Collatz/ProgramA…G.lean import Mathlib, carry sorry, and contain placeholder definitions (local_height = 0, S n = n, a theorem proving x = x by rfl). They do not compile and are not built on.

A — Adelic filter on ghosts — refuted (height route)

Strongest result: the hoped inequality h(σ) ≥ κ·disc(σ), κ > 0, is false.

Certificate: exhaustive at L = 16. Of 6848 primitive words with negative realizer, 652 have reduced height strictly below log|2^E − 3^L|. Example: word 0010111111111101, denominator 465905, reduces to −320596/42355 — a collapse of 0.37 nats. The all-ones word gives λ_σ = −1 exactly, for every length.

Obstruction — ghost. The height of λ_σ is governed by gcd(C(σ), 2^E − 3^L), which is uncontrolled. These are degree-1 points, so Lehmer/Dobrowolski give nothing, and the only available lower bound is saturated by λ = −1, a genuine ghost. The {2,3,∞}-restricted adelic norm was also computed along orbits: it equals the part of n coprime to 6, is neither conserved nor monotone.

D — Sturmian / mechanical wall — refuted

Strongest result: the congruence tower is never empty. L₀(ε) does not exist for any ε, so "every mechanical word with β ≤ α − ε dies by length L₀(ε)" is false for every ε.

Certificate: enumerating odd n < 2^18, every valuation word (v₁,…,v_L) of small total occurs — missing 0 of 8, 64, 350, 941 at L = 1,2,3,4. This is the Terras/Everett bijection: the first L valuations depend only on n mod 2^E, and every word is realised by a residue class.

Obstruction — Mersenne bypass, general form. The brief already forbids emptying residue classes mod 2^M; the same holds one level up, for valuation words themselves. Nothing dies at any length.

F — Lexicographic vector height — refuted as templated

Strongest lemma (new, Lean, Strategy/DensitySaturation):

no_bounded_block_descent : 0 < B → B < j → 2^j - 1 < acceleratedOrbit B (2^j - 1)
no_uniform_block         : ∀ B, 0 < B → ∃ n, 0 < n ∧ n < acceleratedOrbit B n

resting on

orbit_pow_pred : i ≤ m → acceleratedOrbit i (3^k * 2^m - 1) = 3^(k+i) * 2^(m-i) - 1

so T^B(2^j − 1) = 3^B·2^(j−B) − 1 > 2^j − 1, since 2^B < 3^B.

Certificate: the same for Syracuse. With n = 2^(B+3) − 1, bit length over a block of B steps moves +3, +5, +10, +19, +38 for B = 4, 8, 16, 32, 64; all valuations are 1 throughout.

Obstruction — ghost/Mersenne. A height whose leading coordinate is the magnitude of n, decreasing over a block of length bounded uniformly in n, cannot exist: the family 2^j − 1 trades one 2 for one 3 per step and grows over any fixed number of steps. Since a block length that is "a function of n mod 2^M" takes finitely many values, it is bounded, and the brief's template is dead as specified.

Escape hatch, not excluded: a block length depending on an unbounded statistic of n — v₂(n+1) is the natural one, since it is exactly the run length. That is the next lemma below.

B — Discrete stochastic localization — open; the kill boundary is now drawn

Expected reduction to A stands: κ positive exactly on the ghosts. Note the repo already refutes the pointwise/block Lyapunov family and excursion-peak potentials (Φ(159487) ≈ 53930, unbounded), so any drift inequality must be genuinely new.

That warning is now a set of theorems — Strategy.DriftSurvivors. The schema is

BlockDescent B := ∀ n, 1 < n → acceleratedOrbit (B n) n < n

and exists_blockDescent_iff shows (∃ B, BlockDescent B) is exactly FiniteStoppingTime, hence a restatement of the conjecture: all content is in the shape of B. What is refuted:

  • no_bounded_blockDescent — any B with a ceiling, via the Mersenne family;
  • no_constant_blockDescent, no_modular_blockDescent — corollaries, covering the constant-block and mod 2^M families in one line each;
  • no_runLength_blockDescent — B n = r(n) + s(r(n)), from RunLengthAny.no_tail_at_any_run_length; not a boundedness consequence.

What survives: B growing with the size of n. LogBlockDescentWithin C is BlockDescentWithin (fun n => C * Nat.log2 n); logBlock_unbounded proves the boundedness kill cannot apply to it and collatz_of_logBlockDescentWithin proves it would settle the conjecture. This is standing problem G3 with an explicit function in place of "a proved function of n".

The reduction, stated exactly. The verified range and the C = 17 range are now the same number, so the brief's pattern (C) is statable with nothing hidden:

collatz_of_logBlock17_above :
  (∀ n ≥ 3 998 720, ∃ k ≤ 17 · ⌊log₂ n⌋, T^k(n) < n) → CollatzConjecture

The finite part is discharged in the kernel; the hypothesis is a stopping-time bound on numbers above a range this repository has verified, with the constant pinned between the refuted 16 and the heuristic ceiling 19.98. collatz_of_logBlock17_above_of takes the range as a parameter, so extending it moves the threshold with no new proof.

The ⌊log₂ n⌋ factor is forced, not stylistic. no_constant_above_threshold (B N) produces, for every bound B and every threshold N, an n > N that has not dropped at any step up to B. So the natural weakening of G3 — "a constant block suffices for all n past some N₀" — is refuted, and the block length has to grow with n.

The heavy-window machinery does not bear on the reduction. Frontier14187.heavy_window_8950 constrains never-droppers in exactly the same regime, so it is the natural thing to try, but heaviness bounds the shape of the first j steps (RunAlgebra.heavy_even_bound: more than 17/27 odd) and never j itself — the heavy language is nonempty at every length by ValuationDensity.Enum_pos, with the all-ones word explicit at every scale. Heaviness is also scale-free: it is a statement about the valuation word, with no information about the size of n. The certificate stack does bring size in, but only in the direction n large ⟹ heavy. Nothing there bounds σ(n) against log₂ n.

Nor does the affine identity (Strategy.AffineObstruction, Round LXXV.19). no_drop_forces extracts everything affine_exact says about a window with no descent — n · 2 ^ j ≤ 3 ^ a · n + affineC j n — and affine_vacuous_of_heavy proves that same inequality from heaviness alone, with no descent hypothesis. So the identity's entire content about non-descent is light_caps_start: light windows cap n, which is the certificate already in the repository. On heavy windows it says nothing new, and heavy windows exist at every length.

The shared obstruction, named once. Both routes are scale-free in the length: every inequality they produce is satisfied by taking the window heavy, and heaviness is available at every j. Bounding σ(n) against log₂ n requires a statement that forces a light window after a controlled number of steps, and neither the heavy-window theorems nor the affine identity contains one. A future proposal can be checked against affine_vacuous_of_heavy: if its inequality follows from heaviness alone, it is this one again.

And the missing ingredient is not a smaller lemma. Round LXXV.20 asked whether "force a light window on a schedule" could be obtained separately, as G1 in sieve-testable form. It cannot, because descent and lightness are the same event: AffineObstruction.light_of_drop shows a drop at step j forces the window light with no hypothesis at all, and drop_iff_light_and_gap gives the exact converse — T^j(n) < n iff the window is light and affineC j n < n · (2 ^ j − 3 ^ a). Structure.Density.accOrbit_lt_of_light already had one direction; what was missing is that it runs both ways.

So a theorem forcing light windows on a log₂ n schedule is collatz_of_logBlock17_above's hypothesis, not a prerequisite for it. Any plan treating it as a stepping stone is circular. Three routes to that hypothesis are now closed with named obstructions, and the third closes the local search rather than leaving it open.

Two corrections to the first version of this entry. (i) The schema must read "drops within B n steps", not "at exactly step B n" — an orbit that has already descended can come back up, and 27 does exactly that (σ(27) = 59 but T^60(27) = 35). BlockDescentWithin is the faithful form; the boundedness kill survives it unchanged, because no_bounded_block_descent gives a rise at every step below j. (ii) The stated open window 2 ≤ C ≤ 12 was wrong at both ends. not_logBlockDescentWithin_fourteen refutes C ≤ 14 using 27 alone, and the ≤ 12 came from MersenneDescent, which bounds σ on the Mersenne family only — not globally. C ≥ 15 is open and no upper bound is known.

Prior art (Round LXXV.27). This whole line is a renormalisation of O. Rozier, Is the Syracuse falling time bounded by 12? (arXiv:2107.11160). His falling time sft(n) counts jumps of ⌊log₂ n⌋ + 1 Syracuse steps; LogBlockDescentWithin C is sft(n) ≤ C up to the change of unit. He conjectures sft uniformly bounded and records ft(12 235 060 455) = 14 — the integer rediscovered here in LXXV.11. 63 728 127 (LXXV.10) is the known longest-total-stopping-time record below 10 ^ 8. The schema, the conjecture and both witnesses are prior art; the formalisation is not. The repository already cited Rozier for a different paper, so this was a search failure.

C ≤ 16 is refuted and C = 17 is the live candidate.

Correction (Round LXXV.25). Rounds LXXV.15–24 each reported the [10 ^ 12, 10 ^ 13) scan as "running, no record yet, workers checked". That scan was killed and produced zero output — no sub-range completed, all six files empty. The absence of records was never evidence: the scanner emitted nothing until a record or a finished sub-range, so an empty file was equally consistent with "no record found" and "barely started". The decade [10 ^ 12, 10 ^ 13) is not cleared and nothing was learned from that run. scripts/ratio_pscan2.c now emits a PROGRESS cleared_to= line every 2 · 10 ^ 10, so partial coverage survives a kill.

What stands is unaffected: the [10 ^ 10, 10 ^ 12) sweep completed — eight workers, whole interval, exactly one record — so over every odd n < 10 ^ 12, σ(n) / ⌊log₂ n⌋ ≤ 16.5758. logBlockDescentWithin_17_below_3998720 verifies C = 17 in the kernel for every 2 ≤ n < 3 998 720 — the whole verified range, at no kernel cost beyond the sweep Search.VerifiedRung14187 already performs. Above 40 000, n either survives the level-10 sieve, in which case Search.drops_all_3905 gives dropsWithin 224 n and 224 ≤ 17 · 15 ≤ 17 · ⌊log₂ n⌋; or it does not, and exists_le_drop_of_not_survives gives a drop within 10 steps. Below 40 000 it is the five logCheckC chunks of logBlockDescentWithin_17_below_100000, which stands.

Against the Class 2 prediction 1/γ ≈ 19.98: observed maximum 16.58 at 10 ^ 12, so if the prediction holds the convergence is slow and three more integer values of C remain for search to knock out. The scan neither confirms nor contradicts it.

The four records of σ(n) / ⌊log₂ n⌋:

n σ ⌊log₂ n⌋ ratio
3 4 1 4
27 59 4 14.75
63 728 127 376 25 15.04
12 235 060 455 547 33 16.58

not_logBlockDescentWithin_of_witness makes each one a one-decide instantiation, so raising the refuted C costs a search, not a proof. logBlockDescentWithin_16_below_20000 still holds — C = 16 fails globally but not on the first 20 000.

Where the ratio is heading. The count of n < N with σ(n) > k is heuristically N · 2^(−γk) with γ = 1 − H(log₃ 2) = 0.05004…, which CLOSURE.md already identifies as the constant of Class 2. If so, sup σ(n)/⌊log₂ n⌋ = 1/γ ≈ 19.98, making C = 20 the critical constant: every C ≤ 19 refutable by a large enough scan, C ≥ 20 the only possibly-true range. Not proved — γ is a density statement and this is a pointwise supremum, exactly the "almost all, therefore all" gap. But it turns refuting any C ≤ 19 into a search with a predicted stopping point.

A proposed drift hypothesis can now be checked against no_bounded_blockDescent mechanically rather than against a remembered caution — the same service GapBarriers.exists_realizer performs for the reachability warning.

C — Carry cocycle / substitution automaton — open, not started

Warning from D: since every valuation word is realised by an integer residue class, "no infinite path with empirical v₂-mean < log₂ 3 is reachable from an integer bitstream" is false for every finite prefix. Any non-reachability statement must be about infinite paths only, and must not follow from prefix reachability.

The warning is now a theorem, not an observation. Strategy.GapBarriers.exists_realizer: for any (a₀, …, a_{L−1}) with every a i ≥ 1 there is an odd n₀ whose first L valuations are exactly those. With traj_congr (determinacy) this is parity_vector_correspondence — valuation vectors of length L correspond exactly to residue classes mod 2^(K+1). So prefix reachability is not merely unrefuted but universal: every finite valuation word is realised, with no exceptions to hunt for. A proposed non-reachability argument can therefore be rejected outright the moment it consumes a finite prefix, and this is now checkable against a theorem rather than against a remembered caution.

E — Hybrid isolation of the residual Cantor set — open, blocked on A/D

A and D were to supply the minimising words. A's minimiser is the all-ones word, whose realiser is −1 exactly; D has no minimiser because nothing dies. Related measurement already made: nested realisers x_k ∈ [0,2^k) of aperiodic high-density words wander over the whole of (0,1) to k = 3200 at densities 0.63…0.9, with leading-bit agreement never exceeding about 4 digits. No linear barrier is visible.

G — Function-field certificate extraction — open, method conflict

The brief asks for WouldBeProofZ.lean carrying a single sorry. The repository forbids sorry outright. The equivalent that fits: state the failing step as an explicit hypothesis Prop and carry it as an argument, which is exactly what this repo already does with HalbeisenHungerbuhler.HHExtremal — and that Prop was later discharged (HHLemmaFive.hhExtremal_holds). That pattern is available and keeps the kernel clean.

Acceptance criteria

  • (P1) no nontrivial cycles — NOT met. The number is small because the kernel-verified range is small, not because the method is weak. Eliahou (1993) proved any nontrivial cycle has at least 17 087 915 elements; Simons–de Weger (2005) excluded all m-cycles for m ≤ 68.

    Correction to the LXXV.28 wording, made LXXV.29. That entry called 14187 "about 1/1200 of Eliahou's bound, by the same tool", which mis-attributes the gap. The two numbers sit at different verified ranges — 3 998 720 here against Eliahou's 2 ^ 40 — and the ladder's price is superlinear. At equal range this route is competitive: RESEARCH.md's Round LXXIV closed form gives price(17 087 915) = 2.124 × 10 ^ 14, matching Halbeisen–Hungerbühler's reported m = 2.12 × 10 ^ 14 and reproducing their L_max = 102 225 496, derived here without reference to the paper. The rungs are the convergent numerators of log₂ 3 — …, 125 743, 301 994, 17 087 915, 102 225 496, … — and StairLower.range_gt_492286389612 prices 301 994 at 4.9 × 10 ^ 11.

    So the honest statement is: this formalisation kernel-checks a range of 3 998 720, and that is what caps its frontier at 14187. The method reaches Eliahou's rung at a range of 2.1 × 10 ^ 14, which nothing here has verified.

    Strongest unconditional result here is Frontier14187.length_ge_14187, on the verified range 3 998 720 (Search.VerifiedRung14187); it supersedes RealizableFrontier6809.length_ge_6809 by seven risers. Round LXXV.12 exhausted the originally banked table, LXXV.14 banked cert_8951 past it, and LXXV.15 supplied its range — so the ladder is again fully unconditional, one rung further out. Each additional rung now costs a fresh certificate and a fresh range. Round XLIV proved the paying route cannot reach further: the verified range needed to kill the k-th ladder rung is ≈ a_k·a_{k+1}/(6 ln 2), which diverges, so no finite verified range excludes all cycle lengths. Climbing two rungs does not touch that conclusion — an independent check at Barina's 704·2^60 puts the reach there at only ~7·10^10 odd steps, still finite and still not all lengths. Rungs to frontier 13133 are banked in Strategy.PreCertified and need only the corresponding ranges; Strategy.FrontierParametric.length_ge_of_cert makes each a one-line instantiation. None of the original seven remain conditional: 13133 was the last, and Search.VerifiedRung13133 supplies its range. Round LXXV.14 banked the next rung — PreCertified.cert_8951 and pow_gap_8951 at threshold 3 997 765, frontier 14187 — using a routine that reproduces all seven earlier thresholds exactly, so the arithmetic is cross-checked and not merely asserted. Round LXXV.15 supplied the range (Search.VerifiedRung14187), so 14187 is now unconditional too. The marginal rung cost 616 448 of verified range for 1054 of frontier.

    Round XLIV's divergence claim is now a theorem, not a measurement. Strategy.RouteCap.cert_reach_le: any certificate reaching odd-step budget A at range c forces A ≤ 6c; hence RouteCap.frontier_le_of_route gives F ≤ fexp (6c) + 1, and RouteCap.route_misses_a_length exhibits, for every c, a cycle length the route cannot reach. The proof is two collisions: 2 ^ fexp a ≤ 3 ^ a turns the certificate into Bcap a < 3 ^ a · c, and 3 ^ i < 2 · 2 ^ fexp i turns the a summands of Bcap a into a · 3 ^ a ≤ 6 · Bcap a. The constant 6 is far from tight — at c = 2 010 160 it allows A < 12 060 960 against the actual 6291 — because it discards how closely 3 ^ a approaches 2 ^ (fexp a + 1), which is the Diophantine content of the measured a_k · a_{k+1} / (6 ln 2) law and is not proved here. Finiteness is proved; the rate is not.

    The price of each rung is now proved too, rung by rung. RouteCap.reach_sharp keeps the gap instead of discarding it: a · 3 ^ a < 6c · (2 · 2 ^ fexp a − 3 ^ a). Measured against the seven known thresholds this is tight to within a factor 1.22, so essentially all of the slack in a < 6c was the one crude step. RouteCap.range_gt_of_reach turns it into a kernel-checkable lower bound on c at any chosen index, and five rungs are checked: reaching past a = 8286, 9616, 10946, 12276, 14271 needs ranges above 2 770 233, 3 897 857, 5 633 687, 8 651 415, 22 543 234. The last is the useful one — frontier 22619 costs more than six and a half times the range of frontier 13133 for less than twice the frontier, and the gap is still shrinking.

    Correction to the previous entry. That entry said the growth law was Diophantine. Within one staircase run it is not. Strategy.StairGap proves

    gapAt (a + 665) + 3 ^ a · (3 ^ 665 − 2 ^ 1054) = 2 ^ 1054 · gapAt a

    as an exact integer identity (gap_step) whenever fexp advances by 1054 across the rung — it is 2 · 2 ^ (F+1054) = 2 ^ 1054 · (2 · 2 ^ F) rearranged, nothing more. So the normalised gap loses at least (3 ^ 665 − 2 ^ 1054) / 3 ^ 665 ≈ 4.365 · 10⁻⁵ per rung, and run_bound gives k · δ · 3 ^ a ≤ gapAt a · 3 ^ 665: a staircase run is finite with an explicit length bound. At a = 4296 that reads k ≤ 17.42, and no_run_18 turns it into the unconditional ¬ StairRun 4296 18 — three kernel comparisons, no evaluation of fexp along the run. The true run length is 17, breaking at a = 16266, so the bound is off by less than one rung.

    The break is elementary too. StairGap.fexp_step_of_noBreak / fexp_step_of_break prove that the fexp increment is decided by the gap itself: it is 1054 exactly when 3 ^ a · δ < 2 ^ 1054 · gapAt a, and 1055 otherwise — the same quantity gap_step subtracts. So no fexp hypothesis survives anywhere, and gap_break gives the other branch exactly: gapAt (a+665) = 2 ^ 1055 · gapAt a + 3 ^ a · (2 ^ 1055 − 3 ^ 665). The gap resets from at most δ / 2 ^ 1054 ≈ 4.4 · 10⁻⁵ back to just over 1.

    The cliff, located and proved. The break point is where the gap is smallest, hence where reach_sharp bites hardest. break_at_15601 proves 15601 is a break (fexp_16266 : fexp 16266 = fexp 15601 + 1055), and range_gt_142907493 proves a certificate reaching past 15601 needs a verified range above 142 907 493 — forty-two times the 3 380 808 that reaches 8286, for less than twice the reach.

    The recursion is real, and it is not a sign reversal. Strategy.StairGeneric states the whole development over a pair (m, n) with 2 ^ n < 3 ^ m < 2 ^ (n+1) — the only two facts the algebra ever used. The previous entry predicted the next level would need the signs swapped. It does not. The convergent denominators of log₂ 3 alternate sides, and the two sides play different roles:

    • the ones approaching from below — 665, 31867 — are the staircase steps, with δ / 3 ^ m = 4.365 · 10⁻⁵ and 7.265 · 10⁻⁶;
    • the ones approaching from above — 15601, 79335 — are the break points, where the gap is extremal and the ladder's price jumps.

    Step 665 1054 recovers StairGap verbatim; Step 31867 50508 continues past its cliff. The level-2 run is 15601 → 47468 → 79335, then break_at_79335. fexp at 47468 and 79335 is derived from the recurrence, never computed: no 125 743-bit comparison is made to establish it.

    New cliffs, proved. range_gt_723837160 (reach past 47468) and range_gt_3608044635 (reach past 79335). Against the 3 380 808 that reaches 8286: a thousandfold range for less than ten times the reach.

    The steps are generated too. The previous entry said each level needs its own Step instance from a kernel comparison on an ever-larger literal. That is no longer so. Strategy.StairLower runs the same kind of recurrence on the dual quantity lgapAt a = 3 ^ a − 2 ^ (fexp a), and its core is unconditional:

    3 ^ (a+M) + 2 ^ (fexp a) · gapAt M
    = 2 ^ (fexp a) · (2 · 2 ^ (fexp M)) + lgapAt a · 3 ^ M

    — true for all a and M, no hypothesis (key_identity). Reading it one way gives lower_step and lgap_step; the other way gives lower_break.

    The two staircases interlock. gap_step drains gapAt under a step and where it exhausts is the next cliff; lgap_step drains lgapAt under a cliff and where it exhausts is the next step:

    lgap, M = 15601 :   665 → 16266 → 31867,  exhausts      (steps)
gap,  m = 31867 : 15601 → 47468 → 79335,  exhausts      (cliffs)
lgap, M = 79335 : 31867 → 111202,         exhausts      (steps)
                          ↳ 190537 is the next cliff

    Every fexp in that diagram is derived. step_31867 re-derives StairGeneric.step2 from the recurrence, and fexp_190537 = 301993 is obtained from lower_break with no comparison at 301 994 bits.

    Level-3 cliff: range_gt_492286389612 — a certificate reaching past 190537 needs a verified range above 4.9 · 10¹¹.

    Scale, honestly. These cliffs are still far inside what a Barina-scale range (704 · 2^60 ≈ 8.1 · 10²⁰) would support; an independent check puts the reach there at ~7 · 10¹⁰ odd steps. What is proved is the shape of the cost curve — superlinear, jumping exactly at the from-above convergents — not that the ladder dies at these indices. RouteCap.cert_reach_le remains the statement that it dies eventually.

    The certificate is now bounded on both sides in closed form. RouteCap.reach_sharp gave the necessary direction — a certificate at a forces a · 3 ^ a < 6c · gapAt a. Round LXXV.21 adds the sufficient one: CertClosedForm.cert_of_gap_bound proves that i · 3 ^ i < 3c · gapAt i for every i < A implies the certificate to A, with no kernel evaluation. The factor of two between them is exactly the slack between CertClosedForm.three_Bcap_le (3 · Bcap a ≤ a · 3 ^ a) and RouteCap.six_Bcap_ge (a · 3 ^ a ≤ 6 · Bcap a).

    Checked at every threshold the ladder uses — (1 086 055, 4296), (2 010 160, 6291), (3 380 808, 8286), (3 997 765, 8951) — the bounds bracket the true reach in all four, a rung or two either side. No frontier moves; the banked certificates are sharper.

    Correction (Round LXXV.23). The previous entry said the cert computations "were never logically necessary". The statement is true and the implicature wrong: cert_of_gap_bound's hypothesis is a condition at every i < A, and evaluating gapAt at every i < A is a computation of the same order as cert. The closed form does not save the computation — it explains it, by pinning the certificate between two explicit inequalities.

    Measured cost: the closed form needs a 39 % larger range for the same reach (4 685 313 vs 3 380 808 at A = 8286, and the same ratio at 8951 and 9616), not a factor of two. The ratio is a · 3 ^ a / (3 · Bcap a), which CertClosedForm.Bcap_sandwich confines to [1, 2] and which appears to tend to 2 ln 2 = 1.386 because Bcap averages 2 ^ (−θ_i) over fractional parts and ∫₀¹ 2 ^ (−θ) dθ = 1/(2 ln 2) — a heuristic, recorded as one.

    The threshold for the next rung, A = 9616, is 4 733 176 (frontier 15241), from the routine that reproduces all eight known thresholds exactly. Not banked as a cert.

    The cycle side's bottleneck is Q, not the gap. Round LXXV.22 bridged the cycle equation to the staircase: a cycle is necessarily light, so CycleGapBridge.gapAt_le_of_light gives gapAt a ≤ 2 ^ E − 3 ^ a, and cycle_min_gap_le gives m · gapAt a ≤ Q unconditionally — no verified range, no certificate.

    Rearranged this caps m by Q / gapAt a, and turning that into a number needs an upper bound on Q; the only one available is affineC_le_Bcap, which is the certificate.

    The L-free form (Round LXXV.24). Strategy.Bootstrap's header describes "a staircase rather than a bootstrap" — the gap is a function of the odd count alone — but could not state it, because G(a) = 2 ^ (fexp a + 1) − 3 ^ a is StairGap.gapAt a and StairGap postdates that file. CycleGapBridge.cycle_min_cap states it:

    3 · m · gapAt a  ≤  a · 3 ^ a,      `a = oddCount m L`,

    for a cycle with every prefix heavy. No L appears. So the cycle minimum is capped by a / (3 h_a) with h_a = gapAt a / 3 ^ a, a quantity StairGap and StairLower compute exactly. range_cap_of_cycle reads it as a floor on the verified range, arriving at RouteCap.reach_sharp's inequality from the cycle side instead of from the certificate. So the chain reproduces the frontier in closed form and stops in the same place. The useful content is where it stops: gapAt a is now known exactly and contributes no slack, while Q ≤ Bcap a is an estimate over all admissible words that ignores which word the cycle has. Sharpening 2 ^ E − 3 ^ a further buys nothing; effort on this side belongs on Q.

    The alternation is unconditionally live. The previous entry listed stalling as the open problem and guessed it needed log₂ 3's continued fraction. It does not. Writing n = fexp m, so that StairGeneric.delta m n and lgapAt m are the same number, the two chains' entry conditions are

    gap chain advances from `M`  ⟺  3 ^ M · lgapAt m < 2 ^ (fexp m) · gapAt M
lgap chain advances from `m` ⟺  2 ^ (fexp m) · gapAt M ≤ lgapAt m · 3 ^ M

    — literal negations of each other. StairLower.alternation_live is Nat.lt_or_ge after unfolding and depends on no axioms at all. StairLower.progress combines it with the two strict-decrease lemmas: for every m ≥ 1 and every M, one chain advances and strictly decreases its normalised quantity.

    The only arithmetic input the whole apparatus needs is StairLower.lgapAt_pos: 3 ^ a is never a power of two, for a ≥ 1. That is parity, one line. StairLower.step_self then shows every m ≥ 1 is a valid Step — 665 and 31867 are not structurally special, they are merely where delta / 3 ^ m is small.

    Still open, and now the only thing: the rate. progress gives strict decrease but no bound on how fast the normalised gaps shrink, so the cliff prices are known only at the checked instances (1.43 · 10⁸, 3.61 · 10⁹, 4.92 · 10¹¹). A rate would need the partial quotients of log₂ 3, which is where the continued fraction genuinely does enter — and nowhere earlier, which is what five rounds of wrong guesses eventually established.

  • (P2) no divergence — NOT met. F refuted as templated; A, D, E blocked.

  • Verdict: neither half is closed. Cycles are not excluded; divergence is not excluded.

Next smallest lemma — ANSWERED (negative)

Resolved. The refined reading — may the tail depend on the run length? — is false, and Strategy.RunLengthUnbounded.no_tail_at_run_length_two proves it: for every B there is an n ≡ 3 (mod 8), hence with r(n) = 2 exactly, whose orbit has still not descended after B steps. So no s : ℕ → ℕ satisfies T^(r(n) + s(r(n)))(n) < n for all odd n > 1.

The construction: for n = 8a + 3, T³(n) = 9a + 4, so choosing 9a + 5 = 2^k lands the orbit exactly on 2^k − 1, and ScaleLadder.climb carries it to 3^k − 1. Solvable iff k ≡ 5 (mod 6), giving a₀ = 3, a_{j+1} = 64a_j + 35 and the family 27, 1819, 116507, 7456539, ….

Where the obstruction is not. The 2^j − 1 family this question proposed as the first test does not refute the shape: Strategy.MersenneDescent checks that it descends within 12j for 2 ≤ j ≤ 200, with the ratio σ/j peaking at 11.2 on the small case j = 5 and staying under 4.34 past j = 30. The obstruction is at small fixed run length instead.

Where the run length does work. r(n) = 1 is genuinely different: σ = 2 for every n ≡ 1 (mod 4), already in Structure.CycleMinClass.two_step_descent. So j = 1 is the sole exception.

Now proved at every run length. Strategy.RunLengthAny.no_tail_at_any_run_length generalizes the construction to every j ≥ 2: take n = 2^j·d − 1 with 3^j·d = 2^(k+1) − 1, which is solvable whenever 2·3^(j−1) ∣ k+1. That divisibility is Strategy.LiftExponentThree.two_pow_three_pow, the p = 3 lift, which this repository previously lacked (LiftExponent covers p = 2 only). The construction's one inequality, n < 2^k − 1, reduces exactly to 2^(j+1) < 3^j — true precisely for j ≥ 2, which is why j = 1 is a genuine exception rather than an artefact.

So the run length controls the descent time only at j = 1.

But it does bound it from below, everywhere. Strategy.MersenneLower.sigma_gt_run_half: for every odd n, no iterate falls below n within r + r/2 steps, i.e. σ(n) > (3/2)·r(n) — no parity assumption. Sharpened at 12 ∣ r to σ(n) > (19/12)·r(n) by sigma_gt_nineteen_twelfths, using the convergent 19/12 of log₂ 3. That is within 0.1% of log₂ 3 itself, which is the ceiling no argument of this shape can pass: the run lifts n by exactly (3/2)^r and a Terras step halves at best. The whole content is 8^m ≤ 9^m, i.e. 2^(3m) ≤ 3^(2m): the run lifts n by (3/2)^r, and a Terras step can at best halve. Measured over all odd n < 200 000 of even run length the bound never fails and its worst-case slack is 6.7%.

So r(n) bounds the descent time from below but not from above — which is the precise sense in which the original question's shape was the wrong one.

Next smallest lemma, statable cold

Let r(n) = v₂(n+1), which by Terras is exactly the number of consecutive odd accelerated steps from odd n. Decide whether

∀ odd n > 1, n > T^(r(n) + s(n))(n) for some explicit s(n)

— i.e. whether a block whose length is the run length itself plus an explicit tail descends. This is the one shape no_uniform_block does not refute, because r(n) is unbounded. Refute it, or find the s that works.

First test: n = 2^j − 1 gives r = j, T^j(n) = 3^j − 1, which is larger than n. So s must be large enough to undo (3/2)^j growth — at least j·log₂3 further even steps. Determine whether that many are available, as a function of j, or exhibit the family where they are not.

Standing problem G6 — inverse-tree coverage — attacked; kernel-checked 7/10; computer-verified (twice) 0.8520, above the published 0.84

Round LXXIX correction. 0.84 (Krasikov–Lagarias 2003, Acta Arith. 109, Theorem 6.1, level k = 11) is still the refereed record — confirmed against Lagarias's 2010 overview, Tao 2022, and two 2026 preprints. It is not the frontier of the method: unrefereed 2026 Lean-formalised preprints (Mazur / ProofAtlas) report 0.88 at level 15 and 0.90 at level 18 from the same Krasikov–Lagarias linear program, with the same (P3) min-over-three-lifts and the same 4m child map. This repository has not verified them. The honest reading of the 0.8520 here is that it clears the published record and sits where a level-13 continuation of K–L's Table 2 should sit — it does not clear the field.

Before Round LXXVI: nothing proved. Papers/KrasikovLagarias2003 recorded the Krasikov–Lagarias lower bound as a proposition with no proof claimed, and that recording was itself vacuous — N ^ p ≤ count · N ^ q holds at p = q because 1 reaches 1. RESEARCH.md's early inverse-tree analysis (Agent C, "CEILING — inverse-tree counting saturates at exponent exactly 1") is a heuristic ceiling, not a bound.

Now (Strategy.TreeCount):

two_pow_le_count : 22 ^ k ≤ N → 2 ^ k ≤ reachesOneUpToCount N
count_pow_five   : 1 ≤ N → N < 22 * reachesOneUpToCount N ^ 5
krasikovLagariasLowerBound_holds : krasikovLagariasLowerBound   -- p/q = 1/5

The count is the repository's own computable one — integers in [1, N] reaching 1 within N accelerated steps — so no classical decidability is smuggled in.

Mechanism. Every odd a prime to 3 has odd preimages (2 ^ v a − 1)/3 at every v in one parity class; over three consecutive such v the residue of 2 ^ v a modulo 9 runs through 1, 4, 7, and the child is prime to 3 unless that residue is 1. So each fertile node has two fertile children below 22 a, (a, v) ↦ child is injective, and level k of the tree is 2 ^ k distinct reachers at most 22 ^ k. Novelty tag: FORMALIZATION-OF-KNOWN (Crandall 1978; the literature's exponent is 0.84, Krasikov–Lagarias 2003).

Second pass (Strategy.TreeBranching, same round). Every fertile child charged its own size. The i-th fertile child of a (i ≥ 0) has valuation at most tmpl i = 4, 6, 10, 12, 16, 18, … (fval_le_tmpl), because the infertile valuations are exactly one residue class of j modulo 3 (fval_admissible, from 4 ^ j mod 9 cycling through 1, 4, 7). With a disjoint-family counting principle (family_count) this gives the exact recursion

NF_rec : 64 ≤ X → Σ_{i<6} NF (3X / 2 ^ tmpl i) ≤ NF X

for the fertile count NF. On the lattice {2 ^ k, 3 · 2 ^ k} a joint induction with ratio 13/10 — two integer inequalities checked by decide (I1, I2) and base cases from NF ≥ 1 — certifies

count_pow_eight : 1 ≤ N → N ^ 3 < 8 · 10 ^ 16 · (reachesOneUpToCount N) ^ 8.

The scalar is 3/8 = 0.375. The recursion's true root is ≈ 0.388; 13/10 ≥ 2 ^ (3/8) is what the rational certificate reaches.

Third pass (Strategy.TreeHalf, Round LXXVI.5–6): the Krasikov–Lagarias residue-class system at classes modulo 81. The children's residues modulo 27 are decided by the parent modulo 81 (ClassChild.fch_mod_27); the class-uniform subtree counts of Subtree (S a Y, recursion S_rec over the six fertile children with disjoint subtrees) are bounded below by a double induction — strong in the scale index y, and for fixed y strong in the root — whose per-class constants are the generated integer certificate TreeCertificate (ratio 71/50, 108 inequalities and the lift bounds closed by decide, axioms [propext]). The child whose class is known only modulo 27 is charged the minimum of the constants over its three lifts, which is the K–L device (their (P3)). Result:

count_sqrt : 1 ≤ N → N < 2 · 10 ^ 21 · (reachesOneUpToCount N) ^ 2

The scalar is 1/2. The scheme was refereed by three adversarial passes before formalisation (they found one threshold error, y₀ = 18 → 23, fixed); the constant 2 · 10 ^ 21 is what the trivial base case S ≥ 1 costs and is not optimised. Literature at this level: Krasikov 1989 0.43 (mod 9), Wirsching 0.48 (mod 27); the double-induction scheme certifies 0.53 at mod 81 and 0.557 at mod 729, against 0.84 for K–L's eliminated system at mod 3^11.

Fourth pass (Strategy.TreeTwoThirds, Round LXXVI.7): induction on the absolute bound. TreeHalf inducts on the scale index and so cannot use a child's claim at a larger index — the "advanced" terms that Krasikov–Lagarias eliminate by back-substitution. Inducting instead on the absolute bound 2^y a / 3·2^y a makes every child claim available (its bound is always strictly below the parent's), so the H-step can take the child at v = 1 up to 2^(y+2) c. Measured on the certificate's map this is worth 0.53 → 0.66 at classes mod 81 and 0.695 at mod 243. With classes mod 243, children mod 81, ratio 8/5, 324 decide-checked inequalities:

count_cube : 1 ≤ N → N ^ 2 < 4 · 10 ^ 29 · (reachesOneUpToCount N) ^ 3

The scalar is 2/3. The continuous system's value at this level is 0.73; the literature's record 0.84 uses classes mod 3^11.

Fifth pass (Strategy.TreeSevenTenths, Round LXXVI.8): the same proof at classes mod 729, children mod 243, ratio 13/8 ((13/8)^10 ≥ 2^7), certificate TreeCertificate3 (972 inequalities, decide in 3 min, [propext]):

count_ten : 1 ≤ N → N ^ 7 < 1.28 · 10 ^ 99 · (reachesOneUpToCount N) ^ 10

The scalar is 7/10. Every proof is the TreeTwoThirds proof with the constants substituted; the scheme is parametric in the tables.

Beyond the kernel (Round LXXVI.9–10). The same scheme with twelve scale types and classes modulo 3^12 — 4.25 million inequalities, verified with Python integers, scripts/kl_certify.py / kl_verify.py, Devices/AbsoluteBound.md for the proof — certifies

#{ n ≤ N : n reaches 1 } ≥ (627 / 10^15) · (359/200)^y   for 10 · 2^y ≤ N,

exponent log₂(359/200) = 0.8439, above Krasikov–Lagarias's 0.84 (their level 11; my implementation reproduces 0.8418 there). Independently re-verified by scripts/kl_verify.py: 4 251 528 inequalities, 0 violations. Level 13 (12 754 584 inequalities, λ = 361/200) closes at exponent 0.8520, independently re-verified (0 violations).

Obstruction to the scalar now. The continuous system's values 0.7608, 0.7826, 0.8032, 0.8168, 0.8295, 0.8418, 0.8531 at levels 6…12 rise by a shrinking ≈ 0.012 per level; the limit is unknown and conjectured below 1. Positive density — the statement that would matter — is open in the literature; Tao's almost-all theorem does not imply it.

Class 4 sharpened — local blindness at 2 and 3 — theorem (Round LXXVI.3)

Strategy.LocalBlindness.local_blindness: for every parity word of length L ≥ 1 with an odd step and 3 ^ a ≤ 2 ^ L, and for every k, there is an odd d ≡ 1 (mod 6 ^ k) and a positive x that is a period-L cycle point of x ↦ (3x + d)/2, x/2 with exactly that word (same odd count, same accumulator). local_blindness_two_three reads it at each prime: d ≡ 1 (mod 2 ^ k) and d ≡ 1 (mod 3 ^ k) at once.

Consequence for every cycle-side proposal in this ledger. Any argument that consumes d only through residues modulo 2 ^ k · 3 ^ m cannot exclude a single light word, for any k, m. The d = 1-specific inputs a cycle proof may use are archimedean: the verified range (asset (a)) and |d| < 2 (asset (d)). This is CLOSURE.md Class 4 with the exact scope of the blindness stated and proved: only at 2 and 3 — at p = 5 the 3x + 5 words have denominator 5 and are not realised by any d ≡ 1 (mod 5).

Ingredients: Lagarias 1990 (rational cycles ↔ integer cycles of 3x + d, here NewModels.word_is_cycle_word), the gap 2 ^ L − 3 ^ a being prime to 6, and a modular inverse obtained without Bézout from the repository's pigeonhole on the powers of the denominator (exists_pow_one_mod). Axioms: propext, Quot.sound only. Novelty tag: NEW as a stated theorem; corollary of known results; barrier content folklore.

Backward mixing modulo 3 ^ k — theorem (Round LXXVIII)

Strategy.BackwardMixing.backward_mixing: for every odd a prime to 3 and every k, the map i ↦ child a (v₀ a + 2 i) mod 3 ^ k is a bijection of {0,…,3 ^ k − 1} onto ℤ/3 ^ k, and is 3 ^ k-periodic in i. Reading off the classes divisible by 3: the fertile children of any node, listed by increasing valuation, hit each of the 2 · 3 ^ (k−1) fertile classes modulo 3 ^ k exactly once per period.

This closes the "backward mixing" line of the Round LXXVI gap list (which asked only for injectivity) and its named first lemma, four_pow_ne_one: the order of 4 modulo 3 ^ (k+1) is exactly 3 ^ k, completing LiftExponentThree. Proof: the admissible multiples are the geometric progression 4 ^ i · base a; 4 generates the index-2 subgroup {u : u ≡ 1 (mod 3)} of (ℤ/3 ^ (k+1))ˣ; and s ↦ (s − 1)/3 carries that subgroup bijectively onto ℤ/3 ^ k. Axioms propext, Quot.sound.

Consequence for G6/G8. The 3-adic imbalance that costs Krasikov–Lagarias its exponent is a truncation effect: per period the branching is exactly equidistributed, but a period costs valuation 2 · 3 ^ k while a node below X contributes only its first O(1) children. The subtree recovers coverage far faster — measured Θ(a · M log M) in scale, M = 3 ^ k (scripts/backward_cover.py), the coupon-collector rate of a density-one equidistributed set. At k = 2 the theorem says every node's 9-slot phase sequence is a rotation of the universal word 2 0 X 1 1 X 0 2 X, counts always (2,2,2): the balance hypothesis Equi (G8) is not about which phases the tree produces. Details and the killed L^∞ route through Tao's Syracuse random variable: Devices/BackwardMixing.md. Novelty tag: NEW (structural); the group-theoretic input is classical.