Implications

A dependency records which declarations a proof uses: the map and the “uses” lists show those, read from the code. An implication edge records what one result could establish about another, even when the released proof goes another way. It is a claim, so each one keeps its contract: the declarations it starts from and reaches, the exact hypotheses, the conclusion it derives, the commit the statements were read at, and how far it has been checked. The edges are curated beside the project, not written by its authors.

Besides these curated edges, the discovery pipeline checked 100 implications in Lean (14 connections): the catalogue. What it tried and did not establish, and the suggestions still without a Lean check: notes.

The kinds of edge, and what each status means
Strengthens
From the sources and the hypotheses, the conclusion follows, and the conclusion gives the target's statement with more: an explicit constant, a weaker hypothesis, a wider range.
Composes with
The sources together give the conclusion, and it needs each of them.
Specializes to
The target's statement is the source's general statement with particular values or in a narrower setting; the hypotheses say which.
Supports an executable construction
The sources justify a computable definition, the target, and the conclusion says what it computes.
proposed
Proposed: someone suggested it. No argument is recorded, and nothing has checked it.
argued
Argued: the argument is written out below. Lean has not checked it.
proved
Proved in Lean: the bridge declaration states the hypotheses and the conclusion, and proves them.
refuted
Refuted: the evidence below shows it does not hold as stated.
proved, not checked here
The edge file says a bridge proves it, and no Lean check of it ran in this build or was recorded.
kernel-checked
Lean's kernel checked the bridge against the contract with no sorry and no extra axioms: either in this build, or in a recorded check this build compared with the contract, the bridge file, the commit and the corpus files it read. The card says which.
check is stale
A check was recorded, but of another contract, bridge file, commit or corpus file than this build has: it says nothing now.
stale
The edge was read at another commit than the one this site shows: the statements may have changed.

Strengthens (1)

From the sources and the hypotheses, the conclusion follows, and the conclusion gives the target's statement with more: an explicit constant, a weaker hypothesis, a wider range.

OAI.DirichletCharacter.LFunction_ne_zero_of_seven_eighths_lt_re → OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap

kernel-checked (recorded) Lean's kernel checked seven_eighths_gap against this contract on 2026-10-10T22:56:22Z (Lean (version 4.34.1, x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release), Mathlib d13f23b723b8, corpus fd4aeeb2ee4f; axioms: propext, Classical.choice, Quot.sound). This build did not run Lean: it shows that record, after comparing the contract, the bridge file and the commit with it, and the corpus files it read.

Hypotheses
(q : ℕ) [NeZero q] (hq : 3 ≤ q)
(χ : DirichletCharacter ℂ q)
(β : ℝ) (hβ : β < 1)
(hzero : χ.LFunction (β : ℂ) = 0)
Conclusion
Real.log 3 / 8 ≤ (1 - β) * Real.log (q : ℝ)
The exact contract, as Lean states it
(∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {s : ℂ},
    7 / 8 < s.re → ¬(χ = 1 ∧ s = 1) → DirichletCharacter.LFunction χ s ≠ 0) →
  ∀ (q : ℕ) [inst : NeZero q],
    3 ≤ q →
      ∀ (χ : DirichletCharacter ℂ q),
        ∀ β < 1, DirichletCharacter.LFunction χ ↑β = 0 → Real.log 3 / 8 ≤ (1 - β) * Real.log ↑q
Each source is a hypothesis: the bridge proves this, and the kernel checked that it does.
What it adds to the target
An explicit constant, c = log 3 / 8, where the target says only that some c > 0 exists; and fewer hypotheses: the contract needs none of the target's χ primitive, χ ≠ 1, χ real-valued or 0 < β.
Argument (in words; Lean checked the bridge, not these words)
Suppose 7/8 < β. Take s = β: its real part is β > 7/8, and s ≠ 1 because β < 1, so the pole exception ¬(χ = 1 ∧ s = 1) holds whatever χ is. The source theorem then gives χ.LFunction β ≠ 0, against hzero. So β ≤ 7/8, and 1 − β ≥ 1/8 > 0. Since q ≥ 3, log q ≥ log 3 > 0. Multiplying, (1 − β) · log q ≥ (1/8) · log q ≥ (log 3)/8. This is the target's statement with c = (log 3)/8 ≈ 0.137 > 0, and it uses none of the target's hypotheses that χ is primitive, that χ ≠ 1, that χ is real-valued, or that 0 < β. Argued by Claude (Opus 5.5), 2026-10-10; the bridge in bridges/SevenEighthsGap.lean is the proof Lean checked.
Bridge
seven_eighths_gap in bridges/SevenEighthsGap.lean
Relation to the target
seven_eighths_gap_gives_absolute_gap proves that the contract gives the target's statement. The contract concludes Real.log 3 / 8 ≤ (1 - β) * Real.log ↑q; the target concludes ∃ c, 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q], 3 ≤ q → ∀ (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ≠ 1 → (∀ (a : ZMod q), (χ a).im = 0) → ∀ (β : ℝ), 0 < β → β < 1 → DirichletCharacter.LFunction χ ↑β = 0 → c ≤ (1 - β) * Real.log ↑q.
Recorded check
2026-10-10T22:56:22Z: checked; Lean (version 4.34.1, x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release); Mathlib d13f23b723b8; corpus fd4aeeb2ee4f; environment 362897e7c89fc6ed2d1c; imports ComparatorChallenges.DirichletSevenEighths, ComparatorChallenges.SiegelZeros; bridge file SHA-256 8b56c323c7e21dee…; run as: python -m lean4_explainer_implications.pipeline contracts --workspace oai-ws --corpus e2e/work/oai/lean --run implications-run --edges E:/lean4-explainer/packages/corpus-oai/src/lean4_explainer_corpus_oai/implications.toml --revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb
Read at commit
fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb: LFunction_ne_zero_of_seven_eighths_lt_re, exists_absolute_real_zero_gap
Origin
Suggested by ChatGPT as “7/8 nonvanishing supplies an explicit real-zero constant”, relayed by the lean4-explainer maintainer, 2026-10-10.
Note
The target gives no value of c: “No explicit value of $c$ is given.” (lean/docs/003.md, line 16). Its released proof applies SiegelZerosAwei.W50.uniform_exclusion_of_local_isolated_bezout. The bridge is checked against the statements in ComparatorChallenges/DirichletSevenEighths.lean and ComparatorChallenges/SiegelZeros.lean, the copies openai/math's comparator checks the released proofs against. The released modules were not built here (the source's import closure is 2,924 files), so that each copy states the same proposition as its released theorem is the comparator's claim, not checked here.

Candidates

Suggested edges with no contract yet: what they would connect, in their proposer's words, and what is missing. They are not claims.

Composes with: OAI.BalancedTransport.balanced_three_stack_realization and OAI.SingleFold.main

Suggested as
“Fluid halting detection plus single-fold representation”
Origin
Suggested by ChatGPT, relayed by the lean4-explainer maintainer, 2026-10-10.
Missing
A stated conclusion, and the link between two models of computation. The fluid theorem says the particle that starts at fixedLabel reaches the observer exactly when Halts M w, for a FiniteMachine M and an input w. SingleFold.main gives every set of natural-number tuples that is REPred (Mathlib's recursively enumerable) a polynomial with exactly one witness on each member and none off it. Composing them needs an encoding of (M, w) as a tuple of natural numbers and a proof that Halts is REPred under it; neither file states one (the fluid proof uses an inputCode internally). With both, the composite would read: the particle reaches the observer exactly when one integer polynomial in the encoded (M, w) has a natural-number solution, and that solution is unique.

The same edges as data: implications.json.