Verify factor-four root-gap constant propagation

[SamPetkov]

Summary

This is a clean follow-up to PR #30, created directly from current main. It isolates the arithmetic and asymptotic propagation from the manuscript's phase-resolved root displacement (5.11) to the final theorem constant.

The central conclusion is that the midpoint construction retains

(q^2/8) * (q - D_4(delta_n))

as the coefficient of n/(log n)^3. Integer rounding costs only N+3, and the amplification theorem subtracts only o(n/N^3). Neither step causes an additional fixed halving.

Conditional on the canonical inputs and their asserted phase-uniformity, the existing entropy certificate therefore supports

(q^2/8) * log(200/153)

instead of the currently displayed

(q^2/32) * log(200/153).

This is a factor-four constant propagation. No witness profile, overlap estimate, canonical manuscript, PDF, or Lean source is changed.

Files

• 625/proofs/ROOT_GAP_CONSTANT_PROPAGATION.md
• 625/audits/ROOT_GAP_CONSTANT_PROPAGATION_AUDIT.md
• 625/experiments/root_gap_constant_supercheck.py
• .github/workflows/erdos625-root-gap-constant-supercheck.yml

Exact rounding lemma

For real x>y and L>=0,

floor(x) - ceil(L) - ceil((x+y)/2)
  > (x-y)/2 - L - 3.

Applied with x=r_+, y=r_4^co, and L=log n, the additive loss is negligible because

(N+3) / (n/N^3) = (N+3)N^3/n -> 0.

The same note records a general placement inequality for

ceil(y + theta(x-y)),

but non-midpoint placement remains experimental until all later constants are replayed.

Local verification

The standard-library checker currently reports:

ERDOS 625 ROOT-GAP CONSTANT SUPERCHECK: PASS
  exact rounding cases: 55296
  largest observed additive rounding deficit: 2.816666666667 (< 3)
  current displayed coefficient: 0.0040219839622420045...
  factor-four propagated coefficient: 0.016087935848968018...

It also:

• verifies the coefficient ratio exactly in high-precision Decimal arithmetic;
• scans the canonical equation tags when run in the repository;
• runs under python -O with explicit exceptions rather than assert;
• performs a diagnostic limiting-phase scan, clearly labelled as non-proof evidence.

The phase scan suggests min A(delta) approx 0.520701335491 on a 1001-point grid, corresponding to an approximate phase coefficient 0.031271565748. This value is not promoted as a theorem or replacement constant.

Scope boundary

This PR does not independently verify:

• equation (5.11) or its uniform o(1);
• Lemma 5.1 and the finite-to-limiting entropy translation;
• Proposition 9.2;
• the amplification theorem;
• Erdos625Statement.

It verifies the deterministic rounding and coefficient propagation once those canonical inputs are accepted. The PR should remain a review artifact until the continuity/uniform-slack and event-intersection steps receive independent line-by-line review.

[SamPetkov]

Focused verification status: PASS within the stated dependency boundary. The root-gap workflow completed successfully, including bytecode compilation, normal execution, execution under python -O, and the canonical equation-tag scan. The repository artifact-synchronization workflow also passed. The remaining review question is mathematical rather than operational: confirm the uniform slack in Lemma 5.1 and the uniformity inherited from equation (5.11).

[SamPetkov]

Independent companion PR #32 now supplies a stronger exact four-support entropy certificate. If both reviews are accepted, the combined explicit coefficient is (log 2)^2 log(1000/639)/8 = 0.026896409808379.... PR #31 itself remains limited to the /8 propagation and does not depend on the new certificate.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 3a4e41399e

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Include the canonical manuscript in path filters

When a PR only changes 625/proofs/COMPLETE_PROOF_SELF_CONTAINED.md, this workflow will not start because pull_request.paths is restricted to these four files, yet source_tag_check() explicitly reads that canonical manuscript and this proof note depends on those equation tags. That lets canonical equation-tag regressions merge without the new supercheck running; add the canonical source path, or broaden the filter to the relevant proof files.

Useful? React with 👍 / 👎.

[chatgpt-codex-connector]

Check every canonical input tag

source_tag_check() says it guards the canonical equations used by the note, but this tuple omits several listed inputs, including the chromatic lower integer from (4.1), the entropy certificate (5.3), and the amplification definition (10.12). If any of those prerequisites are renumbered or removed in a PR that does run this workflow, the checker still prints PASS, so the regression gate does not actually cover the proof dependencies it claims to protect.

Useful? React with 👍 / 👎.

[chatgpt-codex-connector]

Fail when the canonical source is absent

If the canonical manuscript is renamed, deleted, or this checker is run in a checkout where it is missing, the verification still exits successfully and prints the overall PASS banner with only a SKIPPED note. Because this script is meant to guard the equations the new proof note depends on, absence of that source should be a hard failure rather than a successful supercheck.

Useful? React with 👍 / 👎.

[SamPetkov]

Review-sequence coordination is now documented in PR #33. The roadmap records the exact coefficient ledger and makes the dependency explicit: this PR supplies the /8 propagation independently of the stronger entropy certificate in #32.