38.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

13 declarations, 5 contain sorry, 0 declared as axioms

Green's Open Problem 38

References:

100 open problems
[La79] Lovász, László. "On the Shannon capacity of a graph." IEEE Transactions on Information theory 25.1 (1979): 1-7.
[Po20] Polak, Sven. "New methods in coding theory: Error-correcting codes and the Shannon capacity." arXiv preprint arXiv:2005.02945 (2020).
[IRCR26] Itty, Nathaniel and Rosin, Christopher D. and Carstensen, Chase and Reichman, Daniel. "Improved lower bounds for the Shannon capacity of odd cycles." arXiv:2607.21517 (2026).
[Ga26] Gao, Yu. "A recursive construction improving the lower bound on the Shannon capacity of $C_7$." arXiv:2607.27869 (2026).
[BPZ26] Buys, Pjotr and Polak, Sven and Zuiddam, Jeroen. "Lean-verified lower bounds for the Shannon capacity of odd cycles." arXiv:2607.29681 (2026). Lean formalisation: https://github.com/spectra-research/shannon-capacity-lean

Imports (1)

FormalConjecturesUtil

def Green38.IntersectsOnlyAtZero $A - A$ intersects $\{-1, 0, 1\}^n$ only at $0$ line 47 source
Source documentation
$A - A$ intersects $\{-1, 0, 1\}^n$ only at $0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, 𝔽₇
Proof uses: Membership.mem, HSub.hSub, Fin, ZMod, OfNat.ofNat, Insert.insert, Neg.neg, Singleton.singleton, Eq
32 instances, coercions and auxiliary constants left out.
```
def IntersectsOnlyAtZero {n : ℕ} (A : Finset (𝔽₇ n)) : Prop :=
…
```
Mentions: 𝔽₇
def Green38.ValidCardinalities The set of cardinalities of all subsets A where A - A intersects {-1, 0, 1}^n only at 0 line 51 source
Source documentation
The set of cardinalities of all subsets A where A - A intersects {-1, 0, 1}^n only at 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: Set.ofPred, Exists, Finset, 𝔽₇, Green38.IntersectsOnlyAtZero, Eq, Finset.card
```
def ValidCardinalities (n : ℕ) : Set ℕ :=
…
```
theorem Green38.green_38.test_n1_lower {0, 2, 4} is a valid independent set in C_7, giving cardinality 3 line 56 source
Source documentation
{0, 2, 4} is a valid independent set in C_7, giving cardinality 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Nat, Set, Green38.ValidCardinalities, OfNat.ofNat
Proof uses: Exists.intro, Finset, 𝔽₇, Exists, Green38.IntersectsOnlyAtZero, Eq, Finset.card, Insert.insert, Fin, Nat.succ, ZMod, Matrix.vecCons, Matrix.vecEmpty, Singleton.singleton, HSub.hSub, Eq.mpr, Neg.neg, Or, id, implies_congr and 62 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem green_38.test_n1_lower :
    3 ∈ ValidCardinalities 1 := by
…
```
Mentions: Green38.ValidCardinalities
def Green38.LargestAdmissibleCardinality The largest subset $A \subset \mathbb{F}_7^n$ for which $A - A$ intersects $\{-1, 0, 1\}^n$ only at $0$ line 73 source
Source documentation
The largest subset $A \subset \mathbb{F}_7^n$ for which $A - A$ intersects $\{-1, 0, 1\}^n$ only at $0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: SupSet.sSup, Green38.ValidCardinalities
3 instances, coercions and auxiliary constants left out.
```
noncomputable def LargestAdmissibleCardinality : ℕ → ℝ := fun n ↦
…
```
def Green38.C₁ The lower bound constant $C_1 \approx 3.2578$ from [Po20] line 77 source
Source documentation
The lower bound constant $C_1 \approx 3.2578$ from [Po20].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HPow.hPow, OfNat.ofNat, Inv.inv
7 instances, coercions and auxiliary constants left out.
```
noncomputable def C₁ : ℝ := (367 : ℝ) ^ (5⁻¹ : ℝ)
```
def Green38.C₂ The upper bound constant $C_2 \approx 3.3177$ from [La79] line 80 source
Source documentation
The upper bound constant $C_2 \approx 3.3177$ from [La79].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, HMul.hMul, OfNat.ofNat, Real.cos, Real.pi, HAdd.hAdd
12 instances, coercions and auxiliary constants left out.
```
noncomputable def C₂ : ℝ := (7 * Real.cos (Real.pi / 7)) / (1 + Real.cos (Real.pi / 7))
…
```
theorem Green38.green_38.lower Can we improve the lower bound? sorry line 93 source
Source documentation
Can we improve the lower bound? The answer sequence must be eventually nonnegative, since =O compares norms.
Yes. Itty, Rosin, Carstensen and Reichman [IRCR26] found a valid set of size $134753$ in $\mathbb{F}_7^{10}$ (an independent set in the tenth strong power of $C_7$). Taking products gives valid sets of size $134753^{\lfloor n/10 \rfloor}$ in $\mathbb{F}_7^n$, see green_38.variants.lower_itty_rosin_carstensen_reichman, so the growth rate is at least $134753^{1/10} > 3.258020 > C_1$ (note $134753 > 367^2 = 134689$). Gao [Ga26] and then Buys, Polak and Zuiddam [BPZ26] improved the rate further, to $3.258789\ldots$ and $3.2588\ldots$ respectively; the latter is formalised in Lean. The exact growth rate remains open.

depends on sorry what this means
Statement uses: Nat, Real, HPow.hPow, OfNat.ofNat, HDiv.hDiv, And, Filter.Eventually, LE.le, Filter.atTop, Filter.EventuallyLE, Green38.LargestAdmissibleCardinality, Exists, GT.gt, Green38.C₁, Asymptotics.IsBigO
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_38.lower :
    let ans := (answer(fun n : ℕ ↦ (134753 : ℝ) ^ (n / 10)) : ℕ → ℝ)
…
```
theorem Green38.green_38.upper Can we improve the best upper bound? sorry line 102 source
Source documentation
Can we improve the best upper bound? The base c must be positive, since =O compares norms.

depends on sorry what this means
Statement uses: Nat, Real, sorryAx, Bool.false, And, Filter.EventuallyLE, Filter.atTop, Green38.LargestAdmissibleCardinality, Exists, LT.lt, OfNat.ofNat, Green38.C₂, Asymptotics.IsBigO, HPow.hPow
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_38.upper :
    let ans := (answer(sorry) : ℕ → ℝ)
…
```
theorem Green38.green_38.variants.best_lower The lower bound $(C_1 - o(1))^n \leqslant |A|$ where $C_1 = 367^{1/5} \approx 3.2578$, from a valid set of size $367$ in $\mathbb{F}_7^5$ [Po20, Section 9.1] sorry line 113 source
Source documentation
The lower bound $(C_1 - o(1))^n \leqslant |A|$ where $C_1 = 367^{1/5} \approx 3.2578$, from a valid set of size $367$ in $\mathbb{F}_7^5$ [Po20, Section 9.1]. This was the best known bound when Green's list was written; it has since been improved, see green_38.lower.

depends on sorry what this means
Statement uses: Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Green38.C₁, Filter.Eventually, Nat, LE.le, HPow.hPow, HSub.hSub, Green38.LargestAdmissibleCardinality, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_38.variants.best_lower :
    ∀ ε ∈ Set.Ioo (0 : ℝ) C₁, ∀ᶠ n in atTop, (C₁ - ε) ^ n ≤ LargestAdmissibleCardinality n := by
…
```
Mentions: Green38.C₁, Green38.LargestAdmissibleCardinality
theorem Green38.green_38.variants.lower_itty_rosin_carstensen_reichman Itty, Rosin, Carstensen and Reichman [IRCR26] found a valid set of size $134753$ in $\mathbb{F}_7^{10}$ sorry line 122 source
Source documentation
Itty, Rosin, Carstensen and Reichman [IRCR26] found a valid set of size $134753$ in $\mathbb{F}_7^{10}$. Products of copies of it, padded with zero coordinates, give $134753^{\lfloor n/10 \rfloor} \leqslant |A|$ in $\mathbb{F}_7^n$.

depends on sorry what this means
Statement uses: Nat, LE.le, Real, HPow.hPow, OfNat.ofNat, HDiv.hDiv, Green38.LargestAdmissibleCardinality
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_38.variants.lower_itty_rosin_carstensen_reichman (n : ℕ) :
    (134753 : ℝ) ^ (n / 10) ≤ LargestAdmissibleCardinality n := by
…
```
Mentions: Green38.LargestAdmissibleCardinality
theorem Green38.green_38.variants.best_upper The current best upper bound is $|A| \leqslant (C_2 + o(1))^n$ where $C_2 = \frac{7 \cos(\pi/7)}{1 + \cos(\pi/7)} \approx 3.3177$ [La79, Corollary 5] sorry line 129 source
Source documentation
The current best upper bound is $|A| \leqslant (C_2 + o(1))^n$ where $C_2 = \frac{7 \cos(\pi/7)}{1 + \cos(\pi/7)} \approx 3.3177$ [La79, Corollary 5].

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, Green38.LargestAdmissibleCardinality, HPow.hPow, HAdd.hAdd, Green38.C₂, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_38.variants.best_upper :
    ∀ ε > 0, ∀ᶠ n in atTop, LargestAdmissibleCardinality n ≤ (C₂ + ε) ^ n := by
…
```
Mentions: Green38.LargestAdmissibleCardinality, Green38.C₂
theorem Green38.green_38.test_zero_mem_validCardinalities 0 is a valid cardinality, since the empty set vacuously satisfies the condition line 135 source
Source documentation
0 is a valid cardinality, since the empty set vacuously satisfies the condition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Green38.ValidCardinalities, OfNat.ofNat
Proof uses: Exists.intro, Finset, 𝔽₇, Exists, Green38.IntersectsOnlyAtZero, Eq, Finset.card, EmptyCollection.emptyCollection, of_eq_true, HSub.hSub, Fin, ZMod, Insert.insert, Neg.neg, Singleton.singleton, Eq.trans, True, congrArg, funext, eq_self and 9 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem green_38.test_zero_mem_validCardinalities {n : ℕ} :
    0 ∈ ValidCardinalities n := by
…
```
Mentions: Green38.ValidCardinalities
theorem Green38.green_38.test_bound_above The set of valid cardinalities we take the supremum over is bounded above line 142 source
Source documentation
The set of valid cardinalities we take the supremum over is bounded above.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, BddAbove, Green38.ValidCardinalities
Proof uses: Exists.intro, Membership.mem, Set, upperBounds, HPow.hPow, OfNat.ofNat, Finset, 𝔽₇, Exists, Green38.IntersectsOnlyAtZero, Eq, Finset.card, LE.le, Trans.trans, Fintype.card, Fin, ZMod, rfl, Finset.card_le_univ, of_eq_true and 13 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem green_38.test_bound_above {n : ℕ} :
    BddAbove (ValidCardinalities n) := by
…
```
Mentions: Green38.ValidCardinalities