You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
exhaustive universal-quotient test over all 162 small models: PASS;
independent C++20/GMP reconstruction: PASS;
finite-size correction: PASS;
five reconstructed certificate files agree byte-for-byte;
complete reproduction: PASS;
package SHA256SUMS and 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.2141808960977856 and the gapless specialization 1.213560298642605.
Relationship to earlier work
This follows the earlier 1.2060 candidate discussed in #134 and incorporates the statement and exposition corrections identified by @kleinwaks. The gapless specialization of the new theorem equals 1.213560298642605..., matching the independent 1.21356 construction 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.
#146 is now merged, so this branch conflicts with main in both README.md and constants/3a.md. Could you rebase along the lines you already proposed in the PR description — keep the [K2026b] row, append your row after it, and set the README cell to 1.19102809 (1.21418*)? Note that the certified half of that pair is now un-asterisked: the Lean formalization in #146 was independently replayed, so 1.19102809 no longer carries the asterisk.
Two other things while you are in there.
The arithmetic I can check does check out: I get 1 + (rho - sigma)/log R = 1.2141808960977856 from your stated rho, sigma and R, and the gapless specialization 2 - log 2 / log(1 + sqrt 2) = 1.213560298642605 matches your figure exactly. What is not checked is the part your own verification section is candid about — the two-temperature theorem, the method-of-types estimate, Bertrand's postulate and the GHR finite-set lemma. The asterisk is doing the right work here, and the conservative "limit value" framing is the right call, so I am happy for the row to go in on that basis once it is rebased.
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 **improved lower bound (limit value):** to match the two entries already there for this constant, rather than "candidate limit value".
carson-olaf
changed the title
Improve C_3a candidate lower bound to 1.21418 via two-temperature cyclic compression
Improve C_3a lower bound to 1.21418 via two-temperature cyclic compression
Aug 24, 2026
Thanks — done. I rebased onto current main, kept [K2026b] and appended [O2026], set the README cell to 1.19102809 (1.21418*), and changed the Recent progress wording to “improved lower bound (limit value).” I also removed the stale draft language and left the PR ready for review. The branch is now conflict-free and mergeable. Appreciate the independent numerical check.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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.