57.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 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were 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 source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

104 declarations, 0 contain sorry, 0 declared as axioms

Ben Green's Open Problem 57

Reference: Ben Green's Open Problem 57

Let $G$ be a finite abelian group. Consider the space $\Phi(G)$ of all functions on $G$ which are "convex combinations" (in the sense of complex coefficients $c_i$ with $\sum |c_i| \le 1$) of functions of the form $$\phi(g) := \mathbb{E}_{x_1 + x_2 + x_3 = g} f_1(x_2, x_3) f_2(x_1, x_3) f_3(x_1, x_2)$$ with $\|f_i\|_\infty \le 1$ (where $f_i : G \times G \to \mathbb{C}$).

Let $\Phi'(G)$ be the space defined similarly, but with $f_3(x_1, x_2)$ required to be a function of $x_1 + x_2$. Do $\Phi(G)$ and $\Phi'(G)$ coincide?

Note: The "convex combination" here uses complex coefficients whose absolute values sum to at most 1 (cf. personal communication with B. Green, April 2026). Since the base sets are balanced (closed under multiplication by unit complex numbers), this absolutely convex hull equals the real convex hull of the complex-valued base set.

Motivation: $\Phi(G)$ is a 'generalised convolution algebra' as considered by Conlon–Fox–Zhao, whereas $\Phi'(G)$ consists of Tao's $\text{UAP}_2(G)$-functions.

Imports (1)

FormalConjectures.Util.ProblemImports

def Green57.tripleKernel Uniform average over pairs (x₁, x₂) in G × G, with the third variable determined by the relation x₁ + x₂ + x₃ = g line 52 source
Source documentation
Uniform average over pairs (x₁, x₂) in G × G, with the third variable determined by the relation x₁ + x₂ + x₃ = g. The functions fᵢ are complex-valued.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Fintype, Prod, Complex
Proof uses: Fintype.card, HMul.hMul, Inv.inv, HPow.hPow, Nat, OfNat.ofNat, Finset.sum, Finset.univ, Prod.mk, HSub.hSub
26 instances, coercions and auxiliary constants left out.
```
def tripleKernel (f₁ f₂ f₃ : G × G → ℂ) : G → ℂ := fun g =>
…
```
def Green57.baseΦ The generating family of functions for Φ(G) line 60 source
Source documentation
The generating family of functions for Φ(G). The functions fᵢ : G × G → ℂ are bounded by 1 in sup norm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Fintype, Set, Complex
Proof uses: setOf, Exists, Prod, And, LE.le, Real, Norm.norm, OfNat.ofNat, Eq, Green57.tripleKernel
4 instances, coercions and auxiliary constants left out.
```
def baseΦ : Set (G → ℂ) :=
…
```
def Green57.baseΦ' The generating family of functions for Φ′(G), where the third kernel depends only on x₁ + x₂ line 67 source
Source documentation
The generating family of functions for Φ′(G), where the third kernel depends only on x₁ + x₂.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Fintype, Set, Complex
Proof uses: setOf, Exists, Prod, And, LE.le, Real, Norm.norm, OfNat.ofNat, Eq, Green57.tripleKernel, HAdd.hAdd, Prod.fst, Prod.snd
9 instances, coercions and auxiliary constants left out.
```
def baseΦ' : Set (G → ℂ) :=
…
```
def Green57.Φ The space Φ(G) of "convex combinations" of kernels from baseΦ line 78 source
Source documentation
The space Φ(G) of "convex combinations" of kernels from baseΦ.
Since baseΦ G is balanced (closed under multiplication by unit complex numbers) and contains 0, the absolutely convex hull over ℂ (i.e., the set of $\sum c_i \phi_i$ with $\phi_i \in \text{baseΦ}$ and $\sum |c_i| \le 1$) coincides with the real convex hull.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Fintype, Set, Complex
Proof uses: ClosureOperator, convexHull, Real, Green57.baseΦ
31 instances, coercions and auxiliary constants left out.
```
def Φ : Set (G → ℂ) :=
…
```
def Green57.Φ' The restricted space Φ′(G) of "convex combinations" of kernels from baseΦ' line 82 source
Source documentation
The restricted space Φ′(G) of "convex combinations" of kernels from baseΦ'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Fintype, Set, Complex
Proof uses: ClosureOperator, convexHull, Real, Green57.baseΦ'
31 instances, coercions and auxiliary constants left out.
```
def Φ' : Set (G → ℂ) :=
…
```
def Green57.functional The linear functional on G → ℂ given by φ ↦ Re ∑ g, a g * φ g line 87 source
Source documentation
The linear functional on G → ℂ given by φ ↦ Re ∑ g, a g * φ g.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Complex, Real
Proof uses: Complex.re, Finset.sum, Finset.univ, HMul.hMul
13 instances, coercions and auxiliary constants left out.
```
def functional (a : G → ℂ) (φ : G → ℂ) : ℝ :=
…
```
def Green57.supportFn The support function of a set S with respect to a linear functional a: sup_{φ ∈ S} Re ⟨a, φ⟩ line 92 source
Source documentation
The support function of a set S with respect to a linear functional a: sup_{φ ∈ S} Re ⟨a, φ⟩.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Complex, Set, Real
Proof uses: SupSet.sSup, Set.image, Green57.functional
1 instances, coercions and auxiliary constants left out.
```
def supportFn (a : G → ℂ) (S : Set (G → ℂ)) : ℝ :=
…
```
lemma Green57.supportFn_convexHull line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Set, Eq, Real, Green57.supportFn, ClosureOperator, convexHull
Proof uses: id, SupSet.sSup, Set.image, Green57.functional, by_contra, Not, Eq.mpr, False, Eq.refl, Eq.mp, HSub.hSub, Finset.sum, Finset.univ, HMul.hMul, Complex.re, Complex.im, congrArg, congr, Set.image_congr, Membership.mem and 59 more
156 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def Green57.a_vec line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: Matrix.vecCons, Neg.neg, Matrix.vecEmpty
8 instances, coercions and auxiliary constants left out.
def Green57.witness_f1 line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: HAdd.hAdd, HMul.hMul, ZMod.val, ite, Eq, HDiv.hDiv, Neg.neg, Complex.I, HSub.hSub
36 instances, coercions and auxiliary constants left out.
def Green57.witness_f2 line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: HAdd.hAdd, HMul.hMul, ZMod.val, ite, Eq, HDiv.hDiv, Complex.I, HSub.hSub, Neg.neg
36 instances, coercions and auxiliary constants left out.
def Green57.witness_f3 line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: HAdd.hAdd, HMul.hMul, ZMod.val, ite, Eq, HSub.hSub, HDiv.hDiv, Complex.I, Neg.neg
36 instances, coercions and auxiliary constants left out.
lemma Green57.witness_f1_bound line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, LE.le, Real, Norm.norm, Complex, Green57.witness_f1, Prod.fst, Prod.snd
Proof uses: id, Green57.witness_f1_bound.match_1, ite, Eq, HAdd.hAdd, HMul.hMul, ZMod.val, HDiv.hDiv, Neg.neg, Complex.I, HSub.hSub, Unit, of_eq_true, Eq.trans, True, Real.sqrt, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, ite_congr, eq_true_of_decide and 72 more
160 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Green57.witness_f2_bound line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, LE.le, Real, Norm.norm, Complex, Green57.witness_f2, Prod.fst, Prod.snd
Proof uses: id, Green57.witness_f2_bound.match_1, ite, Eq, HAdd.hAdd, HDiv.hDiv, HMul.hMul, Complex.I, HSub.hSub, Neg.neg, ZMod.val, of_eq_true, Eq.trans, True, Real.sqrt, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, ite_congr, eq_true, Mathlib.Meta.NormNum.isNat_eq_true and 94 more
184 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Green57.witness_f3_bound line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, LE.le, Real, Norm.norm, Complex, Green57.witness_f3, Prod.fst, Prod.snd
Proof uses: id, Green57.witness_f2_bound.match_1, ite, Eq, HSub.hSub, HDiv.hDiv, HMul.hMul, Complex.I, HAdd.hAdd, Neg.neg, ZMod.val, of_eq_true, Eq.trans, True, Real.sqrt, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, ite_congr, eq_true, Mathlib.Meta.NormNum.isNat_eq_true and 130 more
195 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Green57.witness_phi line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: Green57.tripleKernel, Prod, Green57.witness_f1, Prod.fst, Prod.snd, Green57.witness_f2, Green57.witness_f3
10 instances, coercions and auxiliary constants left out.
lemma Green57.witness_phi_in_baseΦ line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, ZMod, OfNat.ofNat, Nat, Complex, Set, Green57.baseΦ, Green57.witness_phi
Proof uses: Exists.intro, Prod, Exists, And, LE.le, Real, Norm.norm, Eq, Green57.tripleKernel, Green57.witness_f1, Prod.fst, Prod.snd, Green57.witness_f2, Green57.witness_f3, And.intro, Green57.witness_f1_bound, Green57.witness_f2_bound, Green57.witness_f3_bound, rfl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Green57.sum_zmod3_eq_c line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Eq, Finset.sum, Finset.univ, HAdd.hAdd
Proof uses: Finset, Insert.insert, Singleton.singleton, rfl, Eq.mpr, id, congrArg, Finset.sum_insert, of_decide_eq_true, Not, Membership.mem, Bool, Decidable.decide, Bool.true, Eq.refl, Finset.sum_singleton, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast and 5 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Green57.functional_witness_phi_gt line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LT.lt, Real, HDiv.hDiv, OfNat.ofNat, Nat, Green57.functional, ZMod, Green57.a_vec, Green57.witness_phi
Proof uses: id, Complex, Eq, Finset.sum, Finset.univ, HAdd.hAdd, Green57.sum_zmod3_eq_c, Eq.mpr, Complex.re, HMul.hMul, Matrix.vecCons, Neg.neg, Matrix.vecEmpty, Inv.inv, HPow.hPow, Fintype.card, Green57.witness_f1, HSub.hSub, Green57.witness_f2, Green57.witness_f3 and 81 more
214 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Green57.baseΦ_bddAbove line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, BddAbove, Real, Set.image, Green57.functional, Green57.baseΦ
Proof uses: id, Exists.intro, Membership.mem, Set, upperBounds, setOf, Exists, And, Prod, LE.le, Norm.norm, Eq, Green57.tripleKernel, Complex.re, Finset.sum, Finset.univ, HMul.hMul, Iff.mpr, Set.forall_mem_image, Green57.baseΦ_bddAbove.match_1 and 93 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Green57.supportFn_Φ_gt_5 line 198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LT.lt, Real, HDiv.hDiv, OfNat.ofNat, Nat, Green57.supportFn, ZMod, Green57.a_vec, Green57.Φ
Proof uses: Membership.mem, Complex, Set, Green57.baseΦ, Green57.witness_phi, Green57.witness_phi_in_baseΦ, Eq, Green57.supportFn_convexHull, Eq.mpr, id, congrArg, LE.le, Green57.functional, le_csSup, Set.image, Green57.baseΦ_bddAbove, Set.mem_image_of_mem, Green57.functional_witness_phi_gt, lt_of_lt_of_le
37 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Green57.L_identity_real line 209 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, Neg.neg, HMul.hMul, OfNat.ofNat
Proof uses: Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_mul, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_mul, Int.ofNat, Eq.refl, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt and 40 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Green57.T_identity line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, HAdd.hAdd, MonoidWithZeroHom, Complex.normSq, HSub.hSub, Neg.neg, HMul.hMul, OfNat.ofNat, Nat
Proof uses: Eq.trans, Complex.re, Complex.im, Eq.mpr, id, congrArg, Complex.normSq_apply, Eq.refl, congr, MulZeroClass.zero_mul, sub_zero, add_zero, neg_mul, Eq.symm, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos and 43 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Green57.sum_UV_bound line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, LE.le, Real, Finset.sum, Finset.univ, HPow.hPow, Norm.norm, HMul.hMul
Proof uses: Eq.mpr, id, Eq, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, norm_mul, LE.le.trans, Real.sqrt, Real.sum_mul_le_sqrt_mul_sqrt, of_eq_true, Eq.trans, True, eq_true, mul_le_mul, Real.sqrt_le_sqrt, Real.sqrt_nonneg, True.intro and 9 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Green57.multilinear_bound line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Real, LE.le, Norm.norm, Finset.sum, Finset.univ, HMul.hMul
Proof uses: LE.le.trans, norm_sum_le_of_le, Membership.mem, Finset, norm_mul_le_of_le, le_refl, Eq.mpr, id, Eq, congrArg, Finset.mul_sum
53 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Green57.multilinear_fourier_identity line 227 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, HSub.hSub, Neg.neg
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Green57.U_norm_sq_identity line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, HSub.hSub, Neg.neg
Proof uses: Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.mul_eq_const, Mathlib.Tactic.LinearCombination.mul_const_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_left, Mathlib.Tactic.Ring.mul_pf_right and 41 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Green57.cyclic_sos line 245 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, HAdd.hAdd, MonoidWithZeroHom, Complex.normSq, HMul.hMul, OfNat.ofNat, Nat, Complex.re, Star.star
Proof uses: Eq.mpr, HPow.hPow, HSub.hSub, Complex.im, Neg.neg, id, congr, congrArg, Eq.trans, mul_neg, sub_neg_eq_add, two_mul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.pow_congr and 50 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Green57.two_var_bound_111 line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, LE.le, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: GE.ge, Trans.trans, HDiv.hDiv, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_right and 92 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Green57.two_var_bound line 279 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, LE.le, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: GE.ge, Trans.trans, HDiv.hDiv, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_right and 93 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Green57.tripleKernel_reindex line 302 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, Complex, Eq, Real, Green57.functional, Green57.a_vec, Green57.tripleKernel, HAdd.hAdd, Prod.fst, Prod.snd, HMul.hMul, HDiv.hDiv, Complex.re, Finset.sum, Finset.univ, Prod.mk
Proof uses: id, Fintype.card, rfl, Eq.mpr, Inv.inv, HPow.hPow, HSub.hSub, congrArg, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, Complex.im, Eq.trans, Or, congr, Finset.sum_congr and 39 more
168 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Green57.w_root line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex
Proof uses: HAdd.hAdd, HDiv.hDiv, Neg.neg, OfNat.ofNat, HMul.hMul, Complex.I, Real.sqrt, Real
16 instances, coercions and auxiliary constants left out.
lemma Green57.w_root_eq line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Complex, HAdd.hAdd, HPow.hPow, Nat, Green57.w_root, OfNat.ofNat
Proof uses: id, Real.sqrt, Real, Eq.mpr, congrArg, Eq.symm, Complex.ofReal_pow, Real.sq_sqrt, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, Complex.ofReal_ofNat, Complex.I, Neg.neg, Complex.I_sq, Trans.trans and 82 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Green57.Uhat line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, Complex
Proof uses: ite, Eq, HAdd.hAdd, Prod.mk, HMul.hMul, HSub.hSub, Neg.neg, Green57.w_root
30 instances, coercions and auxiliary constants left out.
def Green57.Vhat line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, Complex
Proof uses: ite, Eq, HAdd.hAdd, Prod.mk, HMul.hMul, HSub.hSub, Neg.neg, Green57.w_root
30 instances, coercions and auxiliary constants left out.
def Green57.What line 336 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: ite, Eq, HAdd.hAdd, HMul.hMul, Green57.a_vec, Green57.w_root, HSub.hSub, Neg.neg
32 instances, coercions and auxiliary constants left out.
lemma Green57.What_sum_sq_eq_generic line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, HAdd.hAdd, MonoidWithZeroHom, Complex.normSq, HSub.hSub, Neg.neg, HMul.hMul, OfNat.ofNat, Nat, Star.star, Complex.re
Proof uses: Eq.mpr, HPow.hPow, Complex.im, id, congr, RingHom, starRingEnd, congrArg, Eq.trans, MulZeroClass.zero_mul, sub_zero, add_zero, mul_neg, sub_neg_eq_add, neg_mul, neg_zero, neg_neg, neg_sub, neg_add_rev, Mathlib.Tactic.Ring.of_eq and 59 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Green57.normSq_eq_norm_sq line 355 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, MonoidWithZeroHom, Complex.normSq, HPow.hPow, Nat, Norm.norm, OfNat.ofNat
Proof uses: Real.sqrt, Complex.norm_def, Eq.mpr, id, congrArg, Eq.symm, Real.sq_sqrt, Complex.normSq_nonneg
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
structure Green57.Eisen line 360 source
no axioms what this means
def Green57.Eisen.toComplex line 365 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green57.Eisen, Complex
Proof uses: HAdd.hAdd, Green57.Eisen.a, HMul.hMul, Green57.Eisen.b, Green57.w_root
6 instances, coercions and auxiliary constants left out.
def Green57.Eisen.add line 368 source
no axioms what this means
Statement uses: Green57.Eisen
Proof uses: Green57.Eisen.mk, HAdd.hAdd, Int, Green57.Eisen.a, Green57.Eisen.b
2 instances, coercions and auxiliary constants left out.
def Green57.Eisen.sub line 369 source
no axioms what this means
Statement uses: Green57.Eisen
Proof uses: Green57.Eisen.mk, HSub.hSub, Int, Green57.Eisen.a, Green57.Eisen.b
2 instances, coercions and auxiliary constants left out.
def Green57.Eisen.mul line 370 source
no axioms what this means
Statement uses: Green57.Eisen
Proof uses: Green57.Eisen.mk, HSub.hSub, Int, HMul.hMul, Green57.Eisen.a, Green57.Eisen.b, HAdd.hAdd
6 instances, coercions and auxiliary constants left out.
def Green57.Eisen.star line 372 source
no axioms what this means
Statement uses: Green57.Eisen
Proof uses: Green57.Eisen.mk, HSub.hSub, Int, Green57.Eisen.a, Green57.Eisen.b, Neg.neg
3 instances, coercions and auxiliary constants left out.
def Green57.Eisen.smul line 374 source
no axioms what this means
Statement uses: Int, Green57.Eisen
Proof uses: Green57.Eisen.mk, HMul.hMul, Green57.Eisen.a, Green57.Eisen.b
2 instances, coercions and auxiliary constants left out.
def Green57.Eisen.normSq line 376 source
no axioms what this means
Statement uses: Green57.Eisen, Int
Proof uses: HAdd.hAdd, HSub.hSub, HMul.hMul, Green57.Eisen.a, Green57.Eisen.b
6 instances, coercions and auxiliary constants left out.
def Green57.Eisen.re_double line 379 source
no axioms what this means
Statement uses: Green57.Eisen, Int
Proof uses: HSub.hSub, HMul.hMul, OfNat.ofNat, Green57.Eisen.a, Green57.Eisen.b
5 instances, coercions and auxiliary constants left out.
lemma Green57.Eisen_toComplex_add line 382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green57.Eisen, Eq, Complex, Green57.Eisen.toComplex, Green57.Eisen.add, HAdd.hAdd
Proof uses: id, Eq.mpr, Int, Green57.Eisen.a, HMul.hMul, Green57.Eisen.b, Green57.w_root, congrArg, congr, Int.cast_add, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, OfNat.ofNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add and 10 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Green57.Eisen_toComplex_sub line 387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green57.Eisen, Eq, Complex, Green57.Eisen.toComplex, Green57.Eisen.sub, HSub.hSub
Proof uses: id, Eq.mpr, HAdd.hAdd, Int, Green57.Eisen.a, HMul.hMul, Green57.Eisen.b, Green57.w_root, congrArg, congr, Int.cast_sub, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, OfNat.ofNat, Mathlib.Tactic.Ring.add_congr and 27 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Green57.Eisen_toComplex_smul line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Green57.Eisen, Eq, Complex, Green57.Eisen.toComplex, Green57.Eisen.smul, HMul.hMul
Proof uses: id, Eq.mpr, HAdd.hAdd, Green57.Eisen.a, Green57.Eisen.b, Green57.w_root, congrArg, congr, Int.cast_mul, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, OfNat.ofNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add and 8 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Green57.Eisen_toComplex_mul line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green57.Eisen, Eq, Complex, Green57.Eisen.toComplex, Green57.Eisen.mul, HMul.hMul
Proof uses: id, HPow.hPow, Nat, Green57.w_root, OfNat.ofNat, HSub.hSub, Neg.neg, HAdd.hAdd, Green57.w_root_eq, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 54 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Green57.Eisen_toComplex_star line 409 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green57.Eisen, Eq, Complex, Green57.Eisen.toComplex, Green57.Eisen.star, Star.star
Proof uses: id, Green57.w_root, HSub.hSub, Neg.neg, OfNat.ofNat, Complex.ext, Eq.mpr, Real, Complex.re, HDiv.hDiv, congr, HAdd.hAdd, HMul.hMul, Complex.I, Real.sqrt, Complex.im, congrArg, Eq.trans, StarAddMonoid.star_add, star_div₀ and 93 more
178 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Green57.normSq_w_root_poly line 422 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, MonoidWithZeroHom, Complex, Complex.normSq, HAdd.hAdd, HMul.hMul, Green57.w_root, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat
Proof uses: id, Complex.re, HDiv.hDiv, Neg.neg, Complex.I, Real.sqrt, Eq.mpr, congrArg, Complex.im, Eq.trans, congr, Complex.div_ofNat_re, MulZeroClass.zero_mul, Complex.div_ofNat_im, zero_div, MulZeroClass.mul_zero, sub_self, add_zero, neg_zero, one_mul and 88 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Green57.Eisen_toComplex_normSq line 437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green57.Eisen, Eq, Real, MonoidWithZeroHom, Complex, Complex.normSq, Green57.Eisen.toComplex, Green57.Eisen.normSq
Proof uses: id, HAdd.hAdd, Green57.Eisen.a, HMul.hMul, Green57.Eisen.b, Green57.w_root, Eq.refl, Eq.mpr, Int, HSub.hSub, congrArg, HPow.hPow, Nat, OfNat.ofNat, Green57.normSq_w_root_poly, Eq.trans, Int.cast_add, congr, Int.cast_sub, Int.cast_mul and 42 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Green57.Eisen_toComplex_re_double line 448 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green57.Eisen, Eq, Real, HMul.hMul, OfNat.ofNat, Nat, Complex.re, Green57.Eisen.toComplex, Green57.Eisen.re_double
Proof uses: id, Eq.mpr, HAdd.hAdd, Green57.Eisen.a, HSub.hSub, Green57.Eisen.b, HDiv.hDiv, Complex, Neg.neg, Real.sqrt, Complex.im, Int, congr, congrArg, Eq.trans, Complex.div_ofNat_re, MulZeroClass.zero_mul, Complex.div_ofNat_im, zero_div, MulZeroClass.mul_zero and 66 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Green57.c_val line 453 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: ite, Eq, Green57.w_root, HSub.hSub, Neg.neg
23 instances, coercions and auxiliary constants left out.
lemma Green57.w_root_star line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Complex, Star.star, Green57.w_root, HSub.hSub, Neg.neg, OfNat.ofNat
Proof uses: Complex.ext, Eq.mpr, Real, Complex.re, HDiv.hDiv, id, congr, HAdd.hAdd, HMul.hMul, Complex.I, Real.sqrt, Complex.im, congrArg, Eq.trans, StarAddMonoid.star_add, star_div₀, star_neg, star_one, star_ofNat, star_mul' and 69 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Green57.w2_root_star line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Complex, Star.star, HSub.hSub, Neg.neg, OfNat.ofNat, Green57.w_root
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Green57.w_root_star, star_star, Eq.refl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Green57.w_root_normSq line 465 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, MonoidWithZeroHom, Complex, Complex.normSq, Green57.w_root, OfNat.ofNat
Proof uses: HMul.hMul, Star.star, Complex.ext, of_eq_true, HSub.hSub, Complex.re, Complex.im, Neg.neg, HAdd.hAdd, Eq.trans, True, congr, congrArg, mul_neg, sub_neg_eq_add, Complex.ofReal_add, Complex.ofReal_mul, MulZeroClass.mul_zero, sub_zero, eq_self and 102 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Green57.w2_root_normSq line 479 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, MonoidWithZeroHom, Complex, Complex.normSq, HSub.hSub, Neg.neg, OfNat.ofNat, Green57.w_root
Proof uses: HMul.hMul, Star.star, Complex.ext, of_eq_true, Complex.re, HAdd.hAdd, Complex.im, Eq.trans, True, congr, congrArg, RingHom, starRingEnd, star_sub, star_neg, star_one, neg_zero, zero_sub, sub_neg_eq_add, zero_add and 111 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Green57.c_val_normSq line 494 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Real, MonoidWithZeroHom, Complex, Complex.normSq, Green57.c_val
Proof uses: Or, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Complex.normSq_one, Eq.symm, Green57.w_root_normSq, Green57.w2_root_normSq
43 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Green57.What_eq line 501 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Eq, Green57.What, HAdd.hAdd, HMul.hMul, Green57.a_vec, Green57.c_val, Star.star
Proof uses: Or, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Green57.w_root, HSub.hSub, Neg.neg, Green57.w_root_star, Green57.w2_root_star, of_eq_true, ite, Eq.trans, True, congr, congrArg, ite_cond_eq_true, eq_self and 7 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Green57.What_eq_generic line 514 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Eq, Real, HAdd.hAdd, HPow.hPow, Norm.norm, Green57.What, HMul.hMul, Complex.re, Star.star, HSub.hSub, Green57.c_val, Neg.neg
Proof uses: MonoidWithZeroHom, Complex.normSq, Green57.What_sum_sq_eq_generic, Green57.c_val_normSq, Green57.a_vec, Green57.What_eq, Eq.symm, Green57.normSq_eq_norm_sq, Eq.mpr, id, congrArg, rfl, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast and 47 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
def Green57.branch_A line 557 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: HSub.hSub, HMul.hMul, Green57.c_val
10 instances, coercions and auxiliary constants left out.
def Green57.branch_B line 558 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: HSub.hSub, HAdd.hAdd, HMul.hMul, Neg.neg, Star.star, Green57.c_val
26 instances, coercions and auxiliary constants left out.
def Green57.branch_C line 559 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex
Proof uses: HAdd.hAdd, HSub.hSub, HMul.hMul, Neg.neg, Star.star, Green57.c_val
26 instances, coercions and auxiliary constants left out.
lemma Green57.matrix_sos_identity line 561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, HMul.hMul, OfNat.ofNat, Nat, HSub.hSub, MonoidWithZeroHom, Complex.normSq, HAdd.hAdd, Complex.re, Star.star, HPow.hPow
Proof uses: Eq.mpr, Complex.im, Neg.neg, Mathlib.Meta.NormNum.instAtLeastTwo, id, congr, RingHom, starRingEnd, congrArg, Eq.trans, neg_mul, sub_neg_eq_add, MulZeroClass.zero_mul, sub_zero, add_zero, Complex.ofReal_add, Complex.ofReal_pow, zero_sub, neg_add_rev, Mathlib.Meta.NormNum.IsNat.to_eq and 67 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Green57.matrix_sos_identity_bound line 569 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LE.le, Real, MonoidWithZeroHom, Complex.normSq, OfNat.ofNat, GT.gt, HSub.hSub, Nat, GE.ge, HPow.hPow, HMul.hMul, HAdd.hAdd, Complex.re, Star.star, HDiv.hDiv
Proof uses: Eq, Green57.matrix_sos_identity, Eq.mpr, id, congrArg, add_nonneg, mul_nonneg, le_of_lt, Complex.normSq_nonneg, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, LT.lt, mul_pos, Mathlib.Meta.NormNum.isNat_lt_true, Bool.false and 62 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
def Green57.c_val_eisen line 593 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Green57.Eisen
Proof uses: ite, Eq, Green57.Eisen.mk, Int, Neg.neg
21 instances, coercions and auxiliary constants left out.
lemma Green57.c_val_eisen_eq line 596 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Complex, Green57.Eisen.toComplex, Green57.c_val_eisen, Green57.c_val
Proof uses: Or, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, of_eq_true, HAdd.hAdd, Int, HMul.hMul, Green57.w_root, Eq.trans, True, congrArg, congr, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_intCast, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one and 48 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def Green57.branch_A_eisen line 608 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Green57.Eisen
Proof uses: Green57.c_val_eisen, Green57.Eisen.add, Green57.Eisen.smul, Int, Neg.neg
4 instances, coercions and auxiliary constants left out.
def Green57.branch_B_eisen line 614 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Green57.Eisen
Proof uses: Green57.Eisen.star, Green57.c_val_eisen, Green57.Eisen.add, Green57.Eisen.smul, Neg.neg, Int
4 instances, coercions and auxiliary constants left out.
def Green57.branch_C_eisen line 620 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Green57.Eisen
Proof uses: Green57.Eisen.star, Green57.c_val_eisen, Green57.Eisen.add, Green57.Eisen.smul, Neg.neg, Int, Green57.Eisen.mul
4 instances, coercions and auxiliary constants left out.
lemma Green57.branch_A_eisen_eq line 626 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Complex, Green57.Eisen.toComplex, Green57.branch_A_eisen, Green57.branch_A
Proof uses: id, Eq.mpr, Green57.Eisen.add, Green57.Eisen.smul, Int, Green57.c_val_eisen, Neg.neg, HSub.hSub, HMul.hMul, Green57.c_val, HAdd.hAdd, congrArg, Green57.Eisen_toComplex_add, Green57.Eisen_toComplex_smul, Green57.c_val_eisen_eq, congr, Int.cast_ofNat, Eq.trans, Int.cast_neg, Mathlib.Tactic.Ring.of_eq and 34 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Green57.branch_B_eisen_eq line 633 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Complex, Green57.Eisen.toComplex, Green57.branch_B_eisen, Green57.branch_B
Proof uses: id, Eq.mpr, Green57.Eisen.add, Green57.Eisen.smul, Neg.neg, Int, Green57.Eisen.star, Green57.c_val_eisen, HSub.hSub, HAdd.hAdd, HMul.hMul, RingHom, starRingEnd, Green57.c_val, congrArg, Green57.Eisen_toComplex_add, Green57.Eisen_toComplex_smul, Star.star, Green57.Eisen_toComplex_star, Green57.c_val_eisen_eq and 44 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Green57.branch_C_eisen_eq line 641 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Complex, Green57.Eisen.toComplex, Green57.branch_C_eisen, Green57.branch_C
Proof uses: id, Eq.mpr, Green57.Eisen.add, Green57.Eisen.smul, Neg.neg, Int, Green57.Eisen.mul, Green57.Eisen.star, Green57.c_val_eisen, HAdd.hAdd, HSub.hSub, HMul.hMul, RingHom, starRingEnd, Green57.c_val, congrArg, Green57.Eisen_toComplex_add, Green57.Eisen_toComplex_smul, Green57.Eisen_toComplex_mul, Star.star and 49 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Green57.isValidBranch line 650 source
no axioms what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Bool
Proof uses: Decidable.decide, Or, And, Ne, Eq
6 instances, coercions and auxiliary constants left out.
lemma Green57.branch_bound_int line 653 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Bool, Green57.isValidBranch, Bool.true, And, GT.gt, Int, HSub.hSub, Green57.Eisen.normSq, Green57.branch_A_eisen, GE.ge, HPow.hPow, HMul.hMul, HAdd.hAdd, Green57.branch_B_eisen, Green57.branch_C_eisen, Green57.Eisen.re_double and 2 more
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Green57.branch_bound line 658 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Bool, Green57.isValidBranch, Bool.true, And, GT.gt, Real, HSub.hSub, MonoidWithZeroHom, Complex, Complex.normSq, Green57.branch_A, GE.ge, HPow.hPow, HMul.hMul, HAdd.hAdd, Green57.branch_B and 3 more
Proof uses: Green57.Eisen.toComplex, Green57.branch_A_eisen, Eq.symm, Green57.branch_A_eisen_eq, Green57.branch_B_eisen, Green57.branch_B_eisen_eq, Green57.branch_C_eisen, Green57.branch_C_eisen_eq, Eq.mpr, id, congrArg, Green57.Eisen.normSq, Green57.Eisen_toComplex_normSq, Green57.Eisen.mul, Green57.Eisen.star, Green57.Eisen_toComplex_mul, Green57.Eisen_toComplex_star, Eq.refl, Green57.Eisen.re_double, Green57.Eisen_toComplex_re_double and 13 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Green57.What_eq_generic_branch line 682 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Eq, Real, HAdd.hAdd, HPow.hPow, Norm.norm, Green57.What, HMul.hMul, MonoidWithZeroHom, Complex.normSq, Complex.re, Star.star, Green57.branch_A, Green57.branch_B, Green57.branch_C
Proof uses: HSub.hSub, Green57.c_val, Neg.neg, Green57.What_eq_generic, Eq.mpr, id, congrArg, Eq.symm, Green57.normSq_eq_norm_sq, Complex.im, congr, Eq.trans, neg_mul, sub_neg_eq_add, MulZeroClass.zero_mul, sub_zero, add_zero, neg_zero, mul_neg, neg_neg and 47 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Green57.normSq_le_one_of_norm_le_one line 698 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LE.le, Real, Norm.norm, OfNat.ofNat, MonoidWithZeroHom, Complex.normSq
Proof uses: Eq, HPow.hPow, Nat, Green57.normSq_eq_norm_sq, Eq.mpr, id, congrArg, norm_nonneg, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, HMul.hMul, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast and 52 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Green57.SOS_identity_real line 704 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Real, HSub.hSub, HMul.hMul, MonoidWithZeroHom, Complex.normSq, Star.star, HAdd.hAdd, OfNat.ofNat, Nat, Complex.re, Eq
Proof uses: Eq.mpr, HPow.hPow, Complex.im, Neg.neg, id, congr, RingHom, starRingEnd, congrArg, Eq.trans, neg_mul, sub_neg_eq_add, two_mul, MulZeroClass.zero_mul, sub_zero, add_zero, Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_add, Complex.ofReal_pow and 69 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Green57.branch_bound_helper line 715 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Real, LE.le, MonoidWithZeroHom, Complex.normSq, OfNat.ofNat, GT.gt, HSub.hSub, HMul.hMul, GE.ge, Nat, Complex.re, Star.star, HAdd.hAdd
Proof uses: Neg.neg, Eq, Green57.SOS_identity_real, Complex.normSq_neg, of_eq_true, Complex.im, Eq.trans, True, congr, congrArg, RingHom, starRingEnd, mul_neg, neg_mul, neg_neg, star_neg, sub_neg_eq_add, neg_add_rev, eq_self, Eq.mpr and 72 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma Green57.branch_bound_int_false line 757 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Bool, Green57.isValidBranch, Bool.false, Int, ite, Green57.Eisen.normSq, Green57.branch_A_eisen, Green57.branch_B_eisen, Green57.branch_C_eisen, Green57.Eisen.re_double, Green57.Eisen.mul, Green57.Eisen.star, And, GT.gt, HSub.hSub, HMul.hMul and 1 more
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Green57.What_sum_sq_bound line 769 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, LE.le, Real, Norm.norm, HAdd.hAdd, HPow.hPow, Green57.What, HDiv.hDiv
Proof uses: dite, Eq, Bool, Green57.isValidBranch, Bool.true, HMul.hMul, MonoidWithZeroHom, Complex.normSq, Complex.re, Star.star, Green57.branch_A, Green57.branch_B, Green57.branch_C, Green57.What_eq_generic_branch, Eq.mpr, id, congrArg, And, GT.gt, HSub.hSub and 130 more
181 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
lemma Green57.What_max_bound_from_sum_sq line 831 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, LE.le, Real, Norm.norm, HAdd.hAdd, HPow.hPow, Green57.What, HDiv.hDiv, Max.max
Proof uses: Or.elim, Eq, max_choice, Eq.rec, Eq.symm
73 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Green57.Uhat_identity line 851 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, HAdd.hAdd, MonoidWithZeroHom, Complex.normSq, HMul.hMul, HSub.hSub, Neg.neg, OfNat.ofNat, Green57.w_root, Nat
Proof uses: id, Eq.mpr, HDiv.hDiv, Complex.I, Real.sqrt, HPow.hPow, Complex.re, Complex.im, Mathlib.Meta.NormNum.instAtLeastTwo, Eq.trans, congr, congrArg, Mathlib.Meta.NormNum.IsRat.neg_to_eq, Mathlib.Meta.NormNum.isRat_div, Int.negOfNat, Mathlib.Meta.NormNum.isRat_mul, Inv.inv, Int.ofNat, Eq.refl, Mathlib.Meta.NormNum.IsInt.to_isRat and 109 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Green57.Uhat_norm_sq_le_9 line 858 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, Complex, LE.le, Real, Norm.norm, HAdd.hAdd, HPow.hPow, Green57.Uhat
Proof uses: Eq, MonoidWithZeroHom, Complex.normSq, Prod.mk, HMul.hMul, HSub.hSub, Neg.neg, Green57.w_root, Green57.Uhat_identity, of_eq_true, Eq.trans, True, congrArg, congr, Complex.sq_norm, eq_self, id, Eq.mpr, Complex.mk, Complex.re and 87 more
148 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Green57.Vhat_norm_sq_le_9 line 868 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, Complex, LE.le, Real, Norm.norm, HAdd.hAdd, HPow.hPow, Green57.Vhat
Proof uses: Eq, MonoidWithZeroHom, Complex.normSq, Prod.mk, HMul.hMul, HSub.hSub, Neg.neg, Green57.w_root, Green57.Uhat_identity, Eq.mpr, id, Eq.trans, congrArg, congr, Complex.sq_norm, add_assoc, Complex.re, Complex.im, LE.le.trans, Complex.mk and 85 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Green57.inner_sum_eq line 876 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Prod, Complex, Eq, HMul.hMul, Finset.sum, Finset.univ, Green57.a_vec, HAdd.hAdd, Prod.mk, Green57.What, Green57.Uhat, Green57.Vhat
Proof uses: Green57.sum_zmod3_eq_c, Eq.mpr, id, congrArg, And, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, congr, And.left, And.right, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf and 58 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
def Green57.What_max line 908 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Real
Proof uses: Max.max, Norm.norm, Green57.What
23 instances, coercions and auxiliary constants left out.
lemma Green57.What_le_max line 911 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, LE.le, Real, Norm.norm, Green57.What, Green57.What_max
Proof uses: id, Or, Eq, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Max.max, le_max_left, Eq.symm, le_trans, le_max_right
37 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Green57.multilinear_bound_3 line 921 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Real, LE.le, Norm.norm, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul
Proof uses: Function.comp, LE.le.trans, norm_add_le_of_le, norm_mul_le_of_le, norm_mul_le, Eq.mpr, id, Eq, congrArg, Eq.symm, mul_add, le_refl, LE.le.trans_eq, mul_le_mul_of_nonneg_left, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq and 72 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Green57.inner_sum_bound_z line 928 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Prod, Complex, LE.le, Real, Norm.norm, Green57.What, Finset.sum, Finset.univ, HMul.hMul, Green57.a_vec, HAdd.hAdd, Prod.mk
Proof uses: Eq, Green57.Uhat, Green57.Vhat, Green57.inner_sum_eq, of_eq_true, Eq.trans, True, congrArg, Complex.norm_ofNat, eq_self, eq_true, True.intro, Trans.trans, Eq.mpr, id, Eq.refl, norm_mul, Green57.multilinear_bound_3, Green57.Uhat_norm_sq_le_9, Green57.Vhat_norm_sq_le_9 and 57 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Green57.h_bound_W_lemma line 955 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, ZMod, OfNat.ofNat, Nat, Complex, LE.le, Real, Norm.norm, Exists, And, GE.ge, HAdd.hAdd, HPow.hPow, HDiv.hDiv, Green57.functional, Green57.a_vec, Green57.tripleKernel, Prod.fst, Prod.snd
Proof uses: Exists.intro, Green57.What_max, le_max_of_le_left, Green57.What, Max.max, norm_nonneg, And.intro, Green57.What_max_bound_from_sum_sq, Green57.What_sum_sq_bound, Eq, HMul.hMul, Complex.re, Finset.sum, Finset.univ, Prod.mk, Green57.tripleKernel_reindex, Eq.mpr, id, congrArg, Green57.inner_sum_bound_z and 83 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Green57.functional_baseΦ'_le_5 line 987 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Membership.mem, Set, Green57.baseΦ', LE.le, Real, Green57.functional, Green57.a_vec, HDiv.hDiv
Proof uses: Prod, Exists, And, Norm.norm, Eq, Green57.tripleKernel, HAdd.hAdd, Prod.fst, Prod.snd, GE.ge, HPow.hPow, Green57.h_bound_W_lemma, HMul.hMul, Real.sqrt, Trans.trans, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.add_congr and 120 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma Green57.baseΦ'_nonempty line 1023 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.Nonempty, ZMod, OfNat.ofNat, Nat, Complex, Green57.baseΦ'
Proof uses: Exists.intro, Membership.mem, Set, Green57.tripleKernel, Prod, id, setOf, Exists, And, LE.le, Real, Norm.norm, Eq, HAdd.hAdd, Prod.fst, Prod.snd, And.intro, of_eq_true, Eq.trans, True and 8 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Green57.baseΦ'_subset_baseΦ line 1032 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: HasSubset.Subset, Set, ZMod, OfNat.ofNat, Nat, Complex, Green57.baseΦ', Green57.baseΦ
Proof uses: Membership.mem, Prod, Exists, And, LE.le, Real, Norm.norm, Eq, Green57.tripleKernel, HAdd.hAdd, Prod.fst, Prod.snd, Exists.intro, And.intro, rfl, Eq.symm
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Green57.Φ'_subset_Φ line 1036 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: HasSubset.Subset, Set, ZMod, OfNat.ofNat, Nat, Complex, Green57.Φ', Green57.Φ
Proof uses: convexHull_mono, Real, Green57.baseΦ', Green57.baseΦ, Green57.baseΦ'_subset_baseΦ
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Green57.supportFn_mono line 1040 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ZMod, OfNat.ofNat, Nat, Complex, HasSubset.Subset, Set.Nonempty, BddAbove, Real, Set.image, Green57.functional, Green57.a_vec, LE.le, Green57.supportFn
Proof uses: csSup_le_csSup, Set.Nonempty.image, Membership.mem, And, Eq, Exists.intro, And.intro, rfl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Green57.supportFn_Φ'_le_5 line 1049 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LE.le, Real, Green57.supportFn, ZMod, OfNat.ofNat, Nat, Green57.a_vec, Green57.Φ', HDiv.hDiv
Proof uses: Complex, Membership.mem, Set, Green57.baseΦ', Green57.functional, Green57.functional_baseΦ'_le_5, Eq, Green57.supportFn_convexHull, Eq.mpr, id, congrArg, csSup_le, Set.image, Set.Nonempty.image, Green57.baseΦ'_nonempty, And
43 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Green57.green_57.variants.z3_functional For $G = \mathbb{Z}/3\mathbb{Z}$ and the functional $a(0) = -1$, $a(1) = -3$, $a(2) = 3$, does the support function of $\Phi$ at $a$ strictly exceed that of $\Phi'$? line 1071 source
Source documentation
For $G = \mathbb{Z}/3\mathbb{Z}$ and the functional $a(0) = -1$, $a(1) = -3$, $a(2) = 3$, does the support function of $\Phi$ at $a$ strictly exceed that of $\Phi'$?
Numerical evidence suggests the answer is yes: $$\sup_{\varphi \in \Phi'(\mathbb{Z}/3\mathbb{Z})} \operatorname{Re}\langle a, \varphi \rangle \;<\; \sup_{\varphi \in \Phi(\mathbb{Z}/3\mathbb{Z})} \operatorname{Re}\langle a, \varphi \rangle.$$
The DeepMind prover agent provided a formal proof, showing that $\frac{183095}{30000}$ separates the support functions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Matrix.vecCons, Neg.neg, Matrix.vecEmpty, Iff, True, LT.lt, Real, Green57.supportFn, Green57.Φ', Green57.Φ
Proof uses: Eq, Green57.a_vec, rfl, Eq.mpr, id, congrArg, true_iff, LE.le, HDiv.hDiv, Green57.supportFn_Φ'_le_5, Green57.functional, Green57.witness_phi, Membership.mem, Set, Green57.baseΦ, Green57.witness_phi_in_baseΦ, Green57.supportFn_convexHull, le_csSup, Set.image, Green57.baseΦ_bddAbove and 4 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem green_57.variants.z3_functional :
    let a : ZMod 3 → ℂ := ![(-1 : ℂ), -3, 3]
…
```
theorem Green57.green_57.variants.z3 Do $\Phi(\mathbb{Z}/3\mathbb{Z})$ and $\Phi'(\mathbb{Z}/3\mathbb{Z})$ coincide? line 1101 source
Source documentation
Do $\Phi(\mathbb{Z}/3\mathbb{Z})$ and $\Phi'(\mathbb{Z}/3\mathbb{Z})$ coincide?
Numerical evidence suggests the answer is no: the integer functional $a = (-1, -3, 3)$ separates the two spaces. A branch-and-bound verification over the phase variables shows $\max_{\Phi'} \operatorname{Re}\langle a, \varphi \rangle < 6.112 < 6.115 \approx \max_{\Phi} \operatorname{Re}\langle a, \varphi \rangle$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, Eq, Set, ZMod, OfNat.ofNat, Nat, Complex, Green57.Φ, Green57.Φ'
Proof uses: LT.lt, Real, Green57.supportFn, Matrix.vecCons, Neg.neg, Matrix.vecEmpty, Iff.mp, True, Green57.green_57.variants.z3_functional, trivial, Iff.intro, False.elim, absurd, Eq.mp, congrArg, lt_irrefl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem green_57.variants.z3 :
    answer(False) ↔ (Φ (ZMod 3) = Φ' (ZMod 3)) := by
…
```
Mentions: Green57.Φ, Green57.Φ'
theorem Green57.green_57 Ben Green's Problem 57: the two structured-function spaces do not always coincide line 1120 source
Source documentation
Is it true that for every finite abelian group $G$ the spaces $\Phi(G)$ and $\Phi'(G)$, obtained from kernels $\phi(g) = \mathbb{E}_{x_1 + x_2 + x_3 = g} f_1(x_2, x_3) f_2(x_1, x_3) f_3(x_1, x_2)$ with $\lVert f_i \rVert_\infty \le 1$ (where $f_i : G \times G \to \mathbb{C}$), still coincide when the third kernel is required to depend only on $x_1 + x_2$?
Green guesses that the answer is probably 'no'.
L4DEL explanation
One would guess that the answer is probably ‘no’.
— Ben Green, 100 Open Problems, Problem 57
Our agent helped resolve problem #57 from Green’s well-known list of open conjectures
— George Tsoukalas et al., AlphaProof Nexus paper (Section 4)
The proposed equality Φ(G) = Φ'(G) is false for finite abelian groups. The pinned development constructs a separating real linear functional for G = ZMod 3, so this single finite counterexample refutes the universal equality.
1. Φ(G) is the real convex hull of bounded three-kernel convolutions; Φ'(G) restricts the third kernel to depend only on x₁+x₂.
2. For ZMod 3, the auxiliary theorem uses the coefficient vector (-1,-3,3) and proves that its support function is strictly larger on Φ than on Φ'.
3. Equal sets have equal support functions, so the strict separation proves Φ(ZMod 3) ≠ Φ'(ZMod 3) and therefore negates the quantified claim.
4. The original problem says "abelian group"; this Lean theorem quantifies over finite abelian groups with decidable equality, which is enough because the counterexample is finite.
Sources and attribution: Pinned Lean source (0647711a7118), Ben Green, 100 Open Problems, Problem 57, George Tsoukalas et al., AlphaProof Nexus paper (Section 4)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, AddCommGroup, Fintype, DecidableEq, Eq, Set, Complex, Green57.Φ, Green57.Φ'
Proof uses: Eq.mpr, Exists, Not, id, Eq.trans, congrArg, forall_congr, Decidable, false_iff, funext, Exists.intro, ZMod, OfNat.ofNat, Nat, Green57.green_57.variants.z3, Eq.mp
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem green_57 :
  answer(False) ↔
    ∀ (G : Type) [AddCommGroup G] [Fintype G] [DecidableEq G],
      Φ G = Φ' G := by
…
```
Mentions: Green57.Φ, Green57.Φ'