Improve C_3a lower bound to 1.21418 via two-temperature cyclic compression - #148
Improve C_3a lower bound to 1.21418 via two-temperature cyclic compression#148carson-olaf wants to merge 2 commits into
Conversation
teorth
commented
Aug 23, 2026
#146 is now merged, so this branch conflicts with Two other things while you are in there. The arithmetic I can check does check out: I get Also, the description says the PR is deliberately opened as a draft, but it is currently marked ready for review. Worth converting it back if you still want it held. Recent progress bullet: please use |
d780d35 to
62a01c5Comparecarson-olaf
commented
Aug 24, 2026
Thanks — done. I rebased onto current |
Summary
This PR records the lower bound
The construction introduces a two-temperature cyclic-quotient theorem: the difference family uses one Gibbs tilt while the sum-family upper bound is optimized with a separate tilt. For
exact rational reconstruction certifies
The proof and verification package is available here:
Source repository · ZIP release asset
ZIP SHA-256:
8e84a693a41c8fe211b67bcdd3539691b35ba409e6d3a0910875925b4a2d4ffbChanges
1.21418*row toconstants/3a.md, conservatively marked as a limit value because the written theorem remains unverified.[K2026b]row and appends[O2026]after it in chronological order.3aREADME cell to the certified/limit pair1.19102809 (1.21418*)and adds the Recent progress entry.Verification
I ran the complete
./reproduce.shworkflow on macOS with Homebrew GMP:SHA256SUMSand ZIP integrity check: PASS.The arithmetic package checks the finite combinatorial reconstruction, numerical hypotheses, and finite-size correction. It does not formally verify the new two-temperature theorem, the method-of-types estimate, Bertrand's postulate, or the GHR finite-set lemma. The proof is not yet externally refereed or Lean-formalized, so independent review remains invited.
During review, @teorth independently reproduced both displayed numerical values: the fixed-rate exponent
1.2141808960977856and the gapless specialization1.213560298642605.Relationship to earlier work
This follows the earlier
1.2060candidate discussed in #134 and incorporates the statement and exposition corrections identified by @kleinwaks. The gapless specialization of the new theorem equals1.213560298642605..., matching the independent1.21356construction announced there; the structured alphabet above crosses that baseline.#146 is now merged and provides an independently replayed Lean formalization of the controlled-carry result. This branch preserves its chronological rows and updates the README's certified/limit pair to
1.19102809 (1.21418*).AI-use disclosure
I used ChatGPT extensively to explore constructions, formulate the two-temperature argument, draft and revise the proof, generate the verification programs, and audit the resulting package. I selected the research direction, ran and reviewed the verification outputs, and am the human contributor responsible for this submission. References and externally sourced claims were checked against the cited sources.
Agent note: Repository changes and submission packaging were prepared with OpenAI Codex (GPT-5 family) in the Codex desktop harness.