Fixed-Shift Möbius Nonvanishing

A Lean 4 / mathlib package and research paper on a positive fixed-shift Möbius nonvanishing phenomenon, its sharp Chebyshev constant, and restricted parity obstructions arising in twin-prime sieve architectures. For the twin-prime application, “fixed shift” means the literal pair $p,p+2$: the project shift is $h=2$ throughout.

Author: Chisora
License: CC BY 4.0
Lean toolchain: v4.30.0
Project status: all Lean material is contained under lean/. The minimal Paper A core is lean/PaperA.lean; rc21 and rc22 append the audited exact OSTT error ledger to that file. The two independent theorem files are stored beside it, and the default Lake target builds all three source files. The rc21 standalone source was observed to elaborate in the user's editor; a fresh repository-wide Lake build remains required. This repository does not prove the twin-prime conjecture.

Main mathematical content

For the rough fixed-shift rank polynomial

M_beta(X,z)
  = sum_r (-1)^r N_r(X;beta) z^(r-1),

the rank-one and rank-two mass is

C_beta(X) = N_1(X;beta) + N_2(X;beta)
          = M_beta'(X,0) - M_beta(X,0).

At beta = 1/12, the degree is at most 11, and the endpoint Markov–Chebyshev inequality gives

sup_(0<z<=1) |M_(1/12)(X,z)|
  >= C_(1/12)(X) / 243.

The constant

243 = 1 + 2*11^2

is sharp in the alternating nonnegative rank cone, with shifted Chebyshev witness T_11(2z-1).

Using the published lower constant 1.2759 in Runbo Li's 2026 almost-prime twin theorem, together with the source-reconstructed Cai--Li rough-restriction lemma, gives

sup_(0<z<=1) |M_(1/12)(X,z)|
  >= (0.00525061728... + o(1)) Pi_2(X).

The restriction lemma is combinatorial: Cai's proof of the weighted inequality uses elementary counting inequalities and Buchstab identities, all of which commute with restriction to the rough subset. The displayed right-hand terms are unchanged up to the single exceptional value p = 2. See the non-Lean resolution audit. Neither nonvanishing statement determines the useful sign, isolates the rank-one mass, or proves infinitely many twin primes.

Current canonical research state

fixed shift: h=2
unconditional twin-prime theorem: NO
unconditional proof credit: 0
unique open gate: OSTT-TWIN2
minimal open coordinate: R2-OSTT(1/12,3/7)

The current exact finite driver is

delta*z*Pi - z*A - E - z^2*H.

Paper B, OSTT, old Variant II, and the mu_3 jet are coordinate forms of one gate, not independent inputs. The Stage317 tail estimate removes the old condition z*log(X) -> 0. The Li--Liu printed constant 0.042 is rejected as a theorem constant; the rebuilt value is diagnostic only. Canonical state and replay files are in canonical/.

Lean source organization

The GitHub repository root contains no Lean source or Lean project configuration files. Everything is under:

lean/
├─ PaperA.lean
├─ RankOneRigidity_OpenOnly.lean
├─ SupportMatchedOSTT_OpenOnly.lean
├─ lakefile.lean
└─ lean-toolchain

PaperA.lean is the minimal single-file Paper A core. Its exact declaration surface is listed in docs/formalization.md.

The two _OpenOnly.lean files sit in the same directory. They import only Mathlib and are not imported by PaperA.lean. The Lake library declares all three modules as roots, so lake build checks all of them.

Revision rc22 preserves the earlier compiler corrections and adds the audited RC21/RC22 state ledger:

• add_le_add_left was replaced by add_le_add_right in the two rank-one tradeoff steps;
• the OSTT finite theorem now targets Lean's normalized product order N1 * (1 + z);
• the half-gap theorem no longer rewrites nested divisions and instead clears the positive denominator directly.

The sorryAx entries shown in the failed rc6 check were consequences of the unresolved goals, not declared project axioms.

The corrected rank-one file contains

C <= V*B + (1+V)*N1
max(0, (C - 154*B)/155) <= N1

from the explicit zero-endpoint derivative interface. The threshold lemma includes the necessary assumption 0 <= V.

The OSTT file formalizes

M = -N1 + z*N2 + R
|R| <= z^2*H
c*Pi2 <= N1+N2
M <= (c-delta)*z*Pi2

implying

(delta*z*Pi2 - z^2*H)/(1+z) <= N1,

together with its half-gap and cofinal-unboundedness forms.

rc21 audited OSTT error ledger

The authenticated rc19 paper and documentation are retained in full. RC21 adds the exact conditional normal form

M = z*C - (1+z)*N1 + R

and the complete finite lower-bound driver

N1 >= (delta*z*Pi - z*A - E - z^2*H)/(1+z).

The exact two-rank specialization and the cofinal-unbounded family theorem are included. The arithmetic estimate OSTT-TWIN2 remains an explicit open input. See docs/ostt-rc21-theory.md and docs/verification-rc21.md.

The algebra is structurally Chen-like: a wider almost-prime container is combined with a one-sided selector bound to isolate rank-one mass. The package does not formalize Chen switching and does not claim a new parity breakthrough.

Repository layout

lean/                         All Lean source and project configuration
docs/paper.md                 Complete paper
docs/paper.tex                LaTeX source generated from the Markdown paper
docs/paper.pdf                Rendered 35-page paper
canonical/                    Current state, claim ledger, and audits
docs/formalization.md         Theorem-to-Lean map and verification boundary
docs/source-audit.md          Li/Cai rough-support audit
docs/research-status.md       Proven, external, computational, and open claims
docs/library-and-github-audit-2026-07-22.md
                              Full Library and rc17/rc18 consistency ledger
docs/nonlean-resolution-audit-2026-07-22.md
                              Cai--Li `(LS)` closure and general certificate
docs/retractions.md           Withdrawn or restricted claims
docs/ostt-rc21-theory.md      Exact RC21 OSTT ledger and open gate
docs/verification-rc21.md     RC21 editor/kernel evidence boundary
docs/verification-rc22.md     Current paper/package synchronization audit
docs/ai-use.md                Claude and ChatGPT disclosure
CITATION.cff                  Citation metadata
LICENSE                       Full CC BY 4.0 legal code
NOTICE                        Copyright and attribution notice

Build

cd lean
lake update
lake exe cache get
lake build

The author reported successful editor/kernel checks under Lean v4.30.0. The recorded axiom output contains only Lean/mathlib's standard foundations (propext, Classical.choice, and Quot.sound) for the classical real-polynomial results. There are no sorry placeholders and no project-specific axiom declarations. See docs/verification-rc19.md for the distinction between the historical author-side checks and the local release audit.

Formalization boundary

When built, the package asks Lean's kernel to verify the statements actually present in all three source files. The historical verification record and the rc19 local-audit boundary are kept separate. In particular:

• lean/PaperA.lean contains the minimal UMN/obstruction core in one file.
• umn_243 proves the endpoint-gap inequality from the explicit EndpointMarkovBound interface.
• The same file contains zero-column and nonlinear non-recovery lemmas, parity-coordinate identities, the corrected two-scale theorem, and quartic rank responses.
• The shifted-Chebyshev witness and exact eleven-node certificate are in RankOneRigidity_OpenOnly.lean, not in PaperA.lean.
• The support-matched finite, half-gap, and cofinal OSTT declarations are in SupportMatchedOSTT_OpenOnly.lean.
• The existence and signature of mathlib's general Chebyshev extremal theorem are documented in the source audit, but no theorem probe is included in lean/PaperA.lean.
• The final affine normalization and sign-symmetrization adapter deriving EndpointMarkovBound is not yet included.
• Li's analytic lower bound, the source-reconstructed rough-restriction lemma, and future rough upper-sieve constants are not Lean declarations in this release; they remain external mathematics documented in the paper.

See docs/formalization.md for the exact map.

rc9 zero-endpoint certificate update

The zero-endpoint program now has three distinct formal statuses.

1. ZeroEndpointMarkovBound is defined in lean/RankOneRigidity_OpenOnly.lean.
2. The deduction from that interface to the rank-one tradeoff (D-Lean) was editor-verified with only standard Lean/mathlib axioms.
3. rc9 appends an exact eleven-point rational certificate intended to close the practical theorem V_11 < 154. This new certificate section requires the reported author-side editor verification.

The exact finite arithmetic has also been reproduced independently with Python Fraction:

small-denominator certificate norm = 153.814471786822... < 154
precision appendix certificate norm = 153.800124372430... < 153.8004

The precision certificate is retained only in the paper appendix and is not the current Lean input. The LSV primary-source audit now identifies the sharp nonformalized value

$$ V_{11}=11\cot(\pi/44)=153.800096506163\ldots. $$

The rational certificates remain valid but nonoptimal.

rc19 also includes a non-Lean arbitrary-degree generator:

python3 scripts/zero_endpoint_certificate_general.py \
  --degree 11 --denominator 20000 --expect-lt 384501/2500

It reproduces the precision certificate exactly and verifies all moment identities with rational arithmetic.

License scope

The author selected CC BY 4.0 for both documentation and original Lean source. Creative Commons generally recommends software-specific licenses for software; this repository records that recommendation in docs/license-and-attribution.md but retains the author's requested CC BY 4.0 release policy.

Documentation

Start with docs/index.md. The full article is docs/paper.md.

AI disclosure

Claude and ChatGPT were used as interactive research and drafting tools. Their use, limitations, and the author's responsibility are documented in docs/ai-use.md. They are not listed as authors.

rc11 zero-endpoint certificate verification

The small-denominator eleven-point certificate is now kernel-verified in the author's Lean v4.30.0 editor environment. The closed theorem chain is

ZeroEndpointMarkovBound
  -> smallCertificate154_reproduce
  -> zeroEndpointMarkovBound154
  -> rank_one_tradeoff_154_closed
  -> rank_one_lower_bound_154_closed

The exact appendix certificate with norm below 153.8004 remains separate. The LSV audit shows that the exact optimum is 11 * cot(pi / 44) = 153.800096506163...; the appendix certificate is near-sharp but nonoptimal.

AI-assisted development disclosure

Both ChatGPT (OpenAI) and Claude (Anthropic) were used as interactive research, drafting, code-generation, and debugging tools. They are not listed as authors. Chisora selected the claims, required corrections, reviewed the repository, and accepts responsibility for the published content. The detailed disclosure is in docs/ai-use.md.

Author's note

rc8 Lean verification update

The independent rank-one and OSTT files passed the editor check with no errors and no sorryAx. In rc11 the eleven-node certificate chain also passes: smallMoment154, smallWeight154_abs_sum_lt, smallCertificate154_reproduce, zeroEndpointMarkovBound154, rank_one_tradeoff_154_closed, and rank_one_lower_bound_154_closed all report only propext, Classical.choice, and Quot.sound.

rc12 LSV primary-source audit

The 1979 paper of Lachance, Saff, and Varga has now been audited at the theorem-text level. Its initial unit-circle constant $\lambda_n$ is not the project constant. The relevant material is Problem III and Theorem 2.5, which give an explicit one-sided weighted Chebyshev extremal.

After the affine change from $[0,1]$ to $[-1,1]$, the exact endpoint constant is

$$ V_n=n\cot\frac{\pi}{4n}. $$

For degree eleven,

$$ V_{11}=11\cot\frac{\pi}{44} =153.800096506163\ldots. $$

The Lean development still proves only the rational certificate <154; the sharp trigonometric formula has not been formalized. Full details are in docs/lsv-primary-source-audit.md.

rc13 prior-art boundary

The Lachance 1984 chapter's public abstract concerns derivative inequalities under the curved majorant $(1-x^2)^{\lambda/2}|p(x)|\le1$. Its full theorem text was not publicly accessible, so no claim is made that the chapter contains no endpoint-zero corollary.

Current mathlib already formalizes standard Chebyshev extremal derivative properties. This repository therefore claims neither a new sharp Markov inequality nor the first Lean formalization of Chebyshev extremality.

The verified project-specific result is the exact rational eleven-point certificate proving the degree-eleven zero-endpoint bound <154, together with the D-Lean arithmetic adapter.

rc14 analytic-input boundary

After freezing the approximation branch, the project returned to the number-theoretic input required by OSTT.

The current literature audit distinguishes three powerful but insufficient inputs:

• almost-all-shift Hardy--Littlewood asymptotics;
• fixed-shift positive Titchmarsh divisor asymptotics;
• large-modulus distribution with factorable sieve weights.

None directly gives the signed support-matched one-sided estimate at the already fixed twin shift $h=2$. The next target is therefore the OSTT-TWIN2 signed support-matched estimate, not another improvement of the polynomial constant.

rc15 target-alignment correction

The fixed-shift analytic obstruction has two distinct direct architectures.

1. OSTT uses the one-sided prime--semiprime / shifted-Möbius state.
2. FSO4 uses the both-composite overlap in the bounded-rank survivor identity.

The four-prime determinant $qv-py=2$ is directly relevant to FSO4, but it does not directly instantiate OSTT. No transference theorem between the two has been proved.

The immediate FSO4 task is to book the smooth, one-centered, and double-centered rank-$(2,2)$ contributions and determine the allowed double-centered error. The OSTT-direct one-sided scalar remains the primary minimal gate.

rc16 FSO4 centered-ledger stop

The finite ideal FSO4 margin is 0.0115757408626948... * N V(z), corresponding to an allowed negative rank-$(2,2)$ defect of about 5.3652% of the observed cell.

This does not produce an asymptotic theorem. The published Bettin--Chandee determinant corollary directly fits only the fully smooth centered component. The one-centered components require a separate three-prime determinant estimate, and the double-centered component requires the four-prime covariance. The dimension-two and marginal sieve constants are also not booked.

FSO4 is therefore retained as a bounded-rank identity and diagnostic but frozen as a main analytic route. The direct OSTT scalar remains the primary gate.

rc17 twin-shift normalization and consistency audit

For the twin-prime application the project pair is defined as $p,p+2$. The project shift is therefore $h=2$ from the outset and is not a free parameter.

A variable $h$ is retained only when describing external theorems that average over many shifts. Importing such a theorem would require a separate SHIFT-AVERAGE-TO-TWIN2 result proving that the already fixed shift $2$ is not exceptional.

The active analytic gate is now named OSTT-TWIN2. FSO4 remains frozen as a main analytic route; its exact identity and diagnostics are retained. The package status was also reconciled with the reported Lean checks:

PaperA.lean:                       EDITOR_VERIFIED
RankOneRigidity_OpenOnly.lean:    KERNEL/EDITOR_VERIFIED
SupportMatchedOSTT_OpenOnly.lean: EDITOR_VERIFIED
sorryAx:                          none

No theorem statement or proof term changed in rc17. One stale source comment and the status documentation were corrected.

rc18 release-consistency repair

rc18 reconciles the public package with the files it actually ships:

• lean/PaperA.lean is described as the minimal core, not as the older modular theorem surface;
• all three Lean modules are roots of the default lake build;
• GitHub Actions runs the official Lean action in the lean/ subproject;
• all Markdown mathematics uses GitHub-compatible dollar delimiters;
• docs/paper.tex is regenerated with Pandoc 3.1.11.1;
• Section 15 kept the main-order statement explicitly conditional on (LS) at the rc18 audit boundary; rc19 supersedes that status after the source reconstruction;
• the FSO4 snapshot is fully reproduced from a separate CSV input;
• metadata, references, static audit, and checksum coverage are synchronized;
• the full Library and rc17/rc18 five-state research audit is included under docs/.

The rc18 packaging environment did not contain Lean. Historical author-side kernel/editor checks remain recorded, and the included GitHub CI build must pass before a final release tag.

rc19 non-Lean source closure

rc19 changes no Lean file. It:

• reconstructs Cai's complete combinatorial proof path for the weighted inequality cited by Li;
• discharges the former subset-stability assumption (LS);
• makes the 1.2759/243 rough-support nonvanishing constant unconditional relative to Li's published theorem;
• adds an arbitrary-degree exact rational certificate generator;
• records a current-source check of recent twin-prime proof claims; and
• leaves OSTT-TWIN2 as the sole unresolved joint gate and claims no unconditional twin-prime theorem.

Lean was not available in the rc19 packaging environment. The existing three Lean files are byte-identical to rc18 and still require the included GitHub CI build before a final release tag.

rc21 full-package integration

RC21 is built from the authenticated rc19 archive identified in docs/verification-rc21.md. It preserves the complete rc19 paper and docs, adds the audited general OSTT algebra to lean/PaperA.lean, and records the 13-theorem editor axiom audit. The former rc20 R2 algebra is represented by the stronger PaperARC21.r2_* specialization rather than a separate PaperARC20 namespace.

The open arithmetic gate remains OSTT-TWIN2; unconditional proof credit is zero.

RC20 lineage note

The RC20 patch was not mechanically applied to this archive because its application contract requires an RC20-PAPERA-INPLACE-UPDATE base marker. This package instead starts from the authenticated rc19 base, integrates the stronger RC21 specialization directly, and restores the separate RC20 Li--Liu source-audit material under canonical/. Therefore the mathematical content is retained, but this release does not claim that the RC20 patcher was executed in the provenance chain.

The release remains a pre-release until the repository-wide GitHub Actions Lean build is green.

Soli Deo gloria