hilbert_functions_4.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

Imports (1)

Mathlib

abbrev Monomial A monomial as its vector of natural-number exponents line 39 source
Source documentation
Monomials in r variables as finitely supported exponent vectors on Fin r.
L4DEL explanation
the exponent vector m = (m(0), m(1), m(2)) ∈ N3
— Human-written Hilbert-functions proof companion
The Lean type Monomial(r) is the finitely supported exponent vector for a monomial in r variables. For the manuscript's three-variable theorem, a monomial such as x₀^a x₁^b x₂^c is therefore represented by the vector (a,b,c) in ℕ³.
1. A coordinate records the exponent of one variable, so comparing two values pointwise is the same divisibility order used throughout the proof.
2. The Lean definition works for any finite number r of variables; the companion specializes this representation to r = 3.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finsupp, Fin
2 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:39 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:39 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:39 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:39 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:39 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:39 (same declaration text).
```
abbrev Monomial (r : ℕ) := Fin r →₀ ℕ
```
def totalDeg Total degree is the sum of a monomial's exponents line 42 source
Source documentation
Total degree of a monomial (sum of all exponents).
L4DEL explanation
|m| = m(0) + m(1) + m(2) for total degree.
— Human-written Hilbert-functions proof companion
totalDeg(m)—written totalDeg m in Lean—adds every coordinate of the exponent vector. In three variables this is m(0)+m(1)+m(2), the usual total degree of the represented monomial.
1. The finitely supported sum makes the definition uniform in the number of variables.
2. Degree is the grading used both to group the order ideal into its O-sequence and to state that all maximal monomials of a pure ideal lie in one degree.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Monomial
Proof uses: Finsupp.sum, Fin
3 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:42 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:42 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:42 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:42 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:42 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:42 (same declaration text).
```
def totalDeg {r : ℕ} (m : Monomial r) : ℕ :=
…
```
Mentions: Monomial
structure OrderIdeal A finite set of monomials closed downward under divisibility line 47 source
Source documentation
A finite order ideal of monomials, closed downward under divisibility. Divisibility of monomials uses the standard pointwise ≤ on Finsupp.
L4DEL explanation
A finite order ideal Γ ⊂ N3 is a finite set closed downward under this order
— Human-written Hilbert-functions proof companion
is said to be an O-sequence if there exists an order ideal M of monomials
— Richard P. Stanley, Hilbert functions of graded algebras (1978)
An OrderIdeal(r) (Lean: OrderIdeal r) stores a finite collection of monomials together with the guarantee that every divisor of a stored monomial is stored too. In exponent-vector form, divisibility is coordinatewise ≤.
1. carrier is the finite set itself.
2. downward_closed is the proof that if n is in the carrier and m ≤ n, then m is also in it.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion, Richard P. Stanley, Hilbert functions of graded algebras (1978)
standard axioms: Quot.sound, propext what this means
Statement uses: Nat

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:47 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:47 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:47 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:47 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:47 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:47 (same declaration text).
```
structure OrderIdeal (r : ℕ) where
…
```
lemma OrderIdeal.mem_of_dvd line 51 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, OrderIdeal, Monomial, Membership.mem, Finset, OrderIdeal.carrier, LE.le, Fin
Proof uses: OrderIdeal.downward_closed
10 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:51 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:51 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:51 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:51 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:51 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:51 (same declaration text).
def divisorsFinset All monomial divisors of one generator as a finite set line 56 source
Source documentation
The finite set of divisors of a monomial, i.e. the principal lower set {m | m ≤ g}.
L4DEL explanation
Div(g) = {u : u ≤ g}.
— Human-written Hilbert-functions proof companion
divisorsFinset(g) (Lean: divisorsFinset g) is the principal lower set of g: it contains exactly the monomials u whose exponent vector is coordinatewise at most that of g. Equivalently, these are the monomial divisors of g.
1. In the type-two proof, every element of the pure order ideal lies below one of its two maximal monomials.
2. This lets the carrier be rewritten as the union of two such divisor sets, the first combinatorial reduction in the manuscript proof.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Monomial, Finset
Proof uses: Finset.Iic, Fin
13 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:56 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:56 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:56 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:56 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:56 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:56 (same declaration text).
```
noncomputable def divisorsFinset {r : ℕ} (g : Monomial r) : Finset (Monomial r) :=
…
```
Mentions: Monomial
lemma mem_divisorsFinset_iff line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Monomial, Iff, Membership.mem, Finset, divisorsFinset, LE.le, Fin
Proof uses: Finset.mem_Iic
18 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:59 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:59 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:59 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:59 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:59 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:59 (same declaration text).
def generatedOrderIdeal The finite order ideal generated by a finite set of monomials line 64 source
Source documentation
The finite order ideal generated by a finite set of monomials.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Monomial, OrderIdeal
Proof uses: OrderIdeal.mk, Finset.biUnion, Fin, divisorsFinset
6 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:64 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:64 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:64 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:64 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:64 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:64 (same declaration text).

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
noncomputable def generatedOrderIdeal {r : ℕ} (G : Finset (Monomial r)) : OrderIdeal r where
…
```
Mentions: Monomial, OrderIdeal
lemma mem_generatedOrderIdeal_iff line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Monomial, Iff, Membership.mem, OrderIdeal.carrier, generatedOrderIdeal, Exists, And, LE.le, Fin
Proof uses: Iff.intro, divisorsFinset, Iff.mp, Finset.biUnion, Finset.mem_biUnion, Exists.intro, And.intro, mem_divisorsFinset_iff, Iff.mpr
15 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:72 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:72 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:72 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:72 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:72 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:72 (same declaration text).

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def IsMaximalIn Maximality inside an order ideal under monomial divisibility line 82 source
Source documentation
Maximality with respect to divisibility inside an order ideal.
L4DEL explanation
A monomial m ∈ Γ is maximal if every n ∈ Γ with m ≤ n also satisfies n ≤ m.
— Human-written Hilbert-functions proof companion
IsMaximalIn(I,m) (Lean: IsMaximalIn I m) says first that m belongs to I, and then that no strictly larger monomial of I is divisible by m. Any member n above m must also lie below m, hence equals it in the partial order.
1. The condition is relative to the selected order ideal, not maximality among all monomials.
2. These maximal elements are the generators whose shared degree and number determine purity, socle degree, and type.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, OrderIdeal, Monomial
Proof uses: And, Membership.mem, Finset, OrderIdeal.carrier, LE.le, Fin
5 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:82 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:82 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:82 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:82 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:82 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:82 (same declaration text).
```
def IsMaximalIn {r : ℕ} (I : OrderIdeal r) (m : Monomial r) : Prop :=
…
```
Mentions: OrderIdeal, Monomial
def maximalMonomials The finite set of maximal monomials of an order ideal line 87 source
Source documentation
The finite set of maximal monomials of an order ideal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OrderIdeal, Finset, Monomial
Proof uses: Finset.filter, IsMaximalIn, Classical.propDecidable, OrderIdeal.carrier

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:87 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:87 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:87 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:87 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:87 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:87 (same declaration text).
```
noncomputable def maximalMonomials {r : ℕ} (I : OrderIdeal r) : Finset (Monomial r) :=
…
```
Mentions: OrderIdeal, Monomial
def IsPure Purity means every maximal monomial has the same total degree line 91 source
Source documentation
Purity: all maximal monomials have the same total degree.
L4DEL explanation
The ideal is pure if all maximal monomials have the same total degree
— Human-written Hilbert-functions proof companion
IsPure(I) (Lean: IsPure I) requires any two maximal monomials of I to have equal total degree. It does not itself assert that a maximal monomial exists; that nonemptiness is added by PureOrderIdeal.
1. The equal-degree condition supplies one common top grading for the ideal.
2. That common degree becomes the socle degree used as the endpoint of the finite O-sequence.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OrderIdeal
Proof uses: Monomial, Membership.mem, Finset, maximalMonomials, Eq, totalDeg
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:91 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:91 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:91 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:91 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:91 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:91 (same declaration text).
```
def IsPure {r : ℕ} (I : OrderIdeal r) : Prop :=
…
```
Mentions: OrderIdeal
structure PureOrderIdeal An order ideal packaged with purity and a maximal monomial line 95 source
Source documentation
A pure order ideal packages an order ideal with purity and a nonempty maximal set.
L4DEL explanation
The ideal is pure if all maximal monomials have the same total degree
— Human-written Hilbert-functions proof companion
PureOrderIdeal(r) (Lean: PureOrderIdeal r) is the structure used when later statements need a pure finite order ideal as data. It contains the ideal, a proof that its maximal monomials share one degree, and a proof that the maximal set is nonempty.
1. The nonempty field makes the subsequent choice of a maximal monomial—and therefore the definition of socle degree—total rather than conditional.
2. This is a formal packaging choice around the manuscript's mathematical notion of a pure order ideal, not a stronger log-concavity assertion.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:95 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:95 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:95 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:95 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:95 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:95 (same declaration text).
```
structure PureOrderIdeal (r : ℕ) where
…
```
def typePO The type is the number of maximal monomials line 101 source
Source documentation
Type of a pure order ideal: the number of maximal monomials.
L4DEL explanation
The type is the number of maximal monomials.
— Human-written Hilbert-functions proof companion
typePO(P) is the cardinality of maximalMonomials(P.ideal). In Lean these are written typePO P and maximalMonomials P.ideal. Thus “type 2” in the theorem means that the pure order ideal has exactly two maximal monomial generators.
1. The definition counts maximal monomials; it does not count variables, degrees, or all elements of the ideal.
2. The main proof uses type two to name two distinct maxima and express the carrier as the union of their divisor sets.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PureOrderIdeal
Proof uses: Finset.card, Monomial, maximalMonomials, PureOrderIdeal.ideal

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:101 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:101 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:101 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:101 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:101 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:101 (same declaration text).
```
noncomputable def typePO {r : ℕ} (P : PureOrderIdeal r) : ℕ :=
…
```
Mentions: PureOrderIdeal
def socleDegree The shared total degree of a pure ideal's maximal monomials line 106 source
Source documentation
Socle degree of a pure order ideal (the common degree of maximal monomials).
L4DEL explanation
this common degree is the socle degree.
— Human-written Hilbert-functions proof companion
socleDegree(P) (Lean: socleDegree P) chooses one maximal monomial and returns its total degree. Purity proves that every other maximal monomial has the same degree, so the result is independent of which witness is chosen.
1. Nonemptiness of the maximal set supplies the chosen witness.
2. The socle degree is the top index through which unimodality or log-concavity is asserted.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PureOrderIdeal
Proof uses: totalDeg, Classical.choose, Monomial, Membership.mem, Finset, maximalMonomials, PureOrderIdeal.ideal, PureOrderIdeal.maximal_nonempty
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:106 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:106 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:106 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:106 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:106 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:106 (same declaration text).
```
noncomputable def socleDegree {r : ℕ} (P : PureOrderIdeal r) : ℕ :=
…
```
Mentions: PureOrderIdeal
def pureOSequence Degree-by-degree counts of monomials in an order ideal line 110 source
Source documentation
The pure O-sequence: number of monomials of total degree d in an order ideal.
L4DEL explanation
The pure O-sequence of Γ is hΓ (d) = #{m ∈ Γ : |m| = d}.
— Human-written Hilbert-functions proof companion
is said to be an O-sequence if there exists an order ideal M of monomials
— Richard P. Stanley, Hilbert functions of graded algebras (1978)
pureOSequence(I,d) (Lean: pureOSequence I d) counts the monomials in I whose total degree is exactly d. Varying d produces the Hilbert-function sequence studied by the theorem.
1. The carrier is filtered by the equation totalDeg m = d.
2. The cardinality of that filtered finite set is the value of the sequence at degree d.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion, Richard P. Stanley, Hilbert functions of graded algebras (1978)
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, OrderIdeal
Proof uses: Finset.card, Monomial, Finset.filter, Eq, totalDeg, OrderIdeal.carrier
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:110 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:110 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:110 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:110 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:110 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:110 (same declaration text).
```
def pureOSequence {r : ℕ} (I : OrderIdeal r) (d : ℕ) : ℕ :=
…
```
Mentions: OrderIdeal
def IsUnimodal Unimodality of a finite sequence h up to index e: there exists a peak j ≤ e such that h is weakly increasing on [0, j] and weakly decreasing on [j, e] line 116 source
Source documentation
Unimodality of a finite sequence h up to index e: there exists a peak j ≤ e such that h is weakly increasing on [0, j] and weakly decreasing on [j, e].

no axioms what this means
Statement uses: Nat
Proof uses: Exists, And, LE.le, LT.lt, HAdd.hAdd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:116 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:116 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:116 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:116 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:116 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:116 (same declaration text).
```
def IsUnimodal (e : ℕ) (h : ℕ → ℕ) : Prop :=
…
```
def IsLogConcaveUpTo Log-concavity at every internal degree through a chosen endpoint line 122 source
Source documentation
Log-concavity up to degree e: h_i² ≥ h_{i-1} h_{i+1} for i ∈ (0, e).
L4DEL explanation
hΓ (i − 1)hΓ (i + 1) ≤ hΓ (i)2 (0 < i < e).
— Human-written Hilbert-functions proof companion
IsLogConcaveUpTo(e,h) (Lean: IsLogConcaveUpTo e h) requires h(i-1)·h(i+1) ≤ h(i)² for every integer index strictly between 0 and e. Each middle term must therefore dominate the geometric mean of its two neighbours.
1. Finset.Ioo 0 e makes both boundary exclusions explicit: neither 0 nor e is tested.
2. For the pure O-sequence theorem, e is instantiated with the socle degree.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Membership.mem, Finset, Finset.Ioo, OfNat.ofNat, LE.le, HMul.hMul, HSub.hSub, HAdd.hAdd, HPow.hPow
14 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:122 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:122 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:122 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:122 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:122 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:122 (same declaration text).
```
def IsLogConcaveUpTo (e : ℕ) (h : ℕ → ℕ) : Prop :=
…
```
def mXYZ The monomial xyz encoded as an exponent vector in 3 variables line 127 source
Source documentation
The monomial xyz encoded as an exponent vector in 3 variables.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat
Proof uses: HAdd.hAdd, Finsupp, Fin, Finsupp.single
10 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:127 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:127 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:127 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:127 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:127 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:127 (same declaration text).
```
noncomputable def mXYZ : Monomial 3 :=
…
```
Mentions: Monomial
def mXZ2 The monomial xz^2 encoded as an exponent vector in 3 variables line 131 source
Source documentation
The monomial xz^2 encoded as an exponent vector in 3 variables.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat
Proof uses: HAdd.hAdd, Finsupp, Fin, Finsupp.single
10 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:131 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:131 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:131 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:131 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:131 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:131 (same declaration text).
```
noncomputable def mXZ2 : Monomial 3 :=
…
```
Mentions: Monomial
def GammaP1 The order ideal generated by the two monomials from P1 line 135 source
Source documentation
The order ideal generated by the two monomials from P1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OrderIdeal, OfNat.ofNat, Nat
Proof uses: generatedOrderIdeal, Insert.insert, Monomial, Finset, Fin, mXYZ, Singleton.singleton, mXZ2
9 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:135 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:135 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:135 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:135 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:135 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:135 (same declaration text).
```
noncomputable def GammaP1 : OrderIdeal 3 :=
…
```
Mentions: OrderIdeal
def ProblemP1 P1 statement: the degree-counting values for the generated order ideal are (1, 3, 4, 2) line 139 source
Source documentation
P1 statement: the degree-counting values for the generated order ideal are (1, 3, 4, 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: And, Eq, Nat, pureOSequence, OfNat.ofNat, GammaP1
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:139 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:139 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:139 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:139 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:139 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:139 (same declaration text).
```
def ProblemP1 : Prop :=
…
```
def ProblemP2CoeffFormula P2 (coefficient-level): one-generator degree counts match the product-formula coefficients line 149 source
Source documentation
P2 (coefficient-level): one-generator degree counts match the product-formula coefficients.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, Monomial, Eq, pureOSequence, generatedOrderIdeal, Singleton.singleton, Finset, Finset.card, Finset.filter, totalDeg, divisorsFinset
2 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:149 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:149 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:149 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:149 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:149 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:149 (same declaration text).
```
def ProblemP2CoeffFormula : Prop :=
…
```
def ProblemP2Type1Unimodal P2 consequence: every type-1 pure O-sequence is unimodal line 155 source
Source documentation
P2 consequence: every type-1 pure O-sequence is unimodal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, PureOrderIdeal, Eq, typePO, OfNat.ofNat, IsUnimodal, socleDegree, pureOSequence, PureOrderIdeal.ideal
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:155 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:155 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:155 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:155 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:155 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:155 (same declaration text).
```
def ProblemP2Type1Unimodal : Prop :=
…
```
def ProblemP2Type1LogConcave P2 consequence: every type-1 pure O-sequence is log-concave line 160 source
Source documentation
P2 consequence: every type-1 pure O-sequence is log-concave.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, PureOrderIdeal, Eq, typePO, OfNat.ofNat, IsLogConcaveUpTo, socleDegree, pureOSequence, PureOrderIdeal.ideal
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:160 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:160 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:160 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:160 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:160 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:160 (same declaration text).
```
def ProblemP2Type1LogConcave : Prop :=
…
```
def ProblemP2 P2 statement, split into a coefficient-level formula plus two sequence consequences line 165 source
Source documentation
P2 statement, split into a coefficient-level formula plus two sequence consequences.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: And, ProblemP2CoeffFormula, ProblemP2Type1Unimodal, ProblemP2Type1LogConcave

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:165 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:165 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:165 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:165 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:165 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:165 (same declaration text).
```
def ProblemP2 : Prop :=
…
```
def ProblemP3 P3 statement: in codimension 3, first-half log-concavity up to e / 2 line 170 source
Source documentation
P3 statement: in codimension 3, first-half log-concavity up to e / 2. Here e is the socle degree of the pure order ideal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: PureOrderIdeal, OfNat.ofNat, Nat, LT.lt, LE.le, HDiv.hDiv, socleDegree, HMul.hMul, pureOSequence, PureOrderIdeal.ideal, HSub.hSub, HAdd.hAdd, HPow.hPow
14 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:170 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:170 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:170 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:170 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:170 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:170 (same declaration text).
```
def ProblemP3 : Prop :=
…
```
def ProblemP4 P4 statement: codimension 3 and type 2 imply unimodality line 178 source
Source documentation
P4 statement: codimension 3 and type 2 imply unimodality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: PureOrderIdeal, OfNat.ofNat, Nat, Eq, typePO, IsUnimodal, socleDegree, pureOSequence, PureOrderIdeal.ideal
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:178 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:178 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:178 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:178 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:178 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:178 (same declaration text).
```
def ProblemP4 : Prop :=
…
```
def ExistsNonLogConcavePureOSeq Helper predicate for open problems about non-log-concavity at fixed codimension/type line 184 source
Source documentation
Helper predicate for open problems about non-log-concavity at fixed codimension/type.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, PureOrderIdeal, And, Eq, typePO, Not, IsLogConcaveUpTo, socleDegree, pureOSequence, PureOrderIdeal.ideal

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:184 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:184 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:184 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:184 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:184 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:184 (same declaration text).
```
def ExistsNonLogConcavePureOSeq (r t : ℕ) : Prop :=
…
```
def ProblemP5 P5: in codimension 3, every type-2 pure O-sequence is log-concave line 189 source
Source documentation
P5: in codimension 3, every type-2 pure O-sequence is log-concave.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: PureOrderIdeal, OfNat.ofNat, Nat, Eq, typePO, IsLogConcaveUpTo, socleDegree, pureOSequence, PureOrderIdeal.ideal
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:189 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:189 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:189 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:189 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:189 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:189 (same declaration text).
```
def ProblemP5 : Prop :=
…
```
def ProblemP6 P6: for fixed r ≥ 5, every type-2 pure O-sequence in codimension r is unimodal line 195 source
Source documentation
P6: for fixed r ≥ 5, every type-2 pure O-sequence in codimension r is unimodal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: LE.le, OfNat.ofNat, PureOrderIdeal, Eq, typePO, IsUnimodal, socleDegree, pureOSequence, PureOrderIdeal.ideal
2 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:195 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:195 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:195 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:195 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:195 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:195 (same declaration text).
```
def ProblemP6 (r : ℕ) : Prop :=
…
```
def ProblemP7 P7: threshold existence for eventual log-concavity failure in codimension r line 202 source
Source documentation
P7: threshold existence for eventual log-concavity failure in codimension r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: LE.le, OfNat.ofNat, Exists, And, ExistsNonLogConcavePureOSeq
2 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:202 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:202 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:202 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:202 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:202 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:202 (same declaration text).
```
def ProblemP7 (r : ℕ) : Prop :=
…
```
def LCFailureThreshold Helper: t0 is a threshold after which all types admit a non-log-concave example line 207 source
Source documentation
Helper: t0 is a threshold after which all types admit a non-log-concave example.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: LE.le, ExistsNonLogConcavePureOSeq
1 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:207 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:207 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:207 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:207 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:207 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:207 (same declaration text).
```
def LCFailureThreshold (r t0 : ℕ) : Prop :=
…
```
def ProblemP8 P8: least threshold for eventual log-concavity failure in codimension r line 211 source
Source documentation
P8: least threshold for eventual log-concavity failure in codimension r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: LE.le, OfNat.ofNat, Exists, IsLeast, setOf, LCFailureThreshold
2 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:211 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:211 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:211 (same statement text; different proof or body), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:211 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean:211 (same declaration text), APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean:211 (same declaration text). Qualify references as ProblemP8@path.
```
def ProblemP8 (r : ℕ) : Prop :=
…
```
def monomialInf line 216 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Monomial
Proof uses: Finsupp.mk, Fin, Inter.inter, Finset, Finsupp.support, Min.min
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma type_two_maximals line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PureOrderIdeal, Eq, typePO, OfNat.ofNat, Exists, Monomial, And, Ne, Finset, maximalMonomials, PureOrderIdeal.ideal, Insert.insert, Fin, Singleton.singleton
Proof uses: id, Iff.mp, Finset.card, Finsupp, Finset.filter, IsMaximalIn, Classical.propDecidable, OrderIdeal.carrier, Finset.card_eq_two
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma carrier_of_maximals line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PureOrderIdeal, Monomial, Eq, Finset, maximalMonomials, PureOrderIdeal.ideal, Insert.insert, Fin, Singleton.singleton, OrderIdeal.carrier, Union.union, divisorsFinset
Proof uses: id, Eq.mpr, Iff, Membership.mem, Or, LE.le, Eq.trans, Finset.Iic, forall_congr, congrArg, congr, OrderIdeal, IsPure, Finset.Nonempty, PureOrderIdeal.mk, And, IsMaximalIn, OrderIdeal.rec, Finset.filter, Classical.propDecidable and 34 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma OSeq_union line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OrderIdeal, Monomial, Eq, Finset, OrderIdeal.carrier, Union.union, Fin, divisorsFinset, pureOSequence, HSub.hSub, HAdd.hAdd, Finset.card, Finset.filter, totalDeg, Inter.inter
Proof uses: Eq.mpr, id, congrArg, pureOSequence.eq_1, Finset.sum, ite, OfNat.ofNat, Finset.card_filter, Eq.symm, Finset.sum_union_inter, Nat.add_sub_cancel, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma divisors_inter line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Monomial, Eq, Finset, Inter.inter, Fin, divisorsFinset, monomialInf
Proof uses: id, Finset.ext, Finsupp, Finset.Iic, Finsupp.mk, Finsupp.support, Min.min, Iff.trans, Membership.mem, And, LE.le, Eq.mpr, Iff, congrArg, propext, Finset.mem_inter, Finset.mem_Iic, Iff.rfl, Iff.symm, Iff.intro and 7 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma size_S1_le_1_or_size_S2_le_1 line 258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Or, LE.le, Finset.card, Fin, Finset.filter, LT.lt, Finset.univ
Proof uses: Or.imp_right, Nat.succ, Iff.mp, Not, not_lt, Function.comp, HAdd.hAdd, Fintype.card, False, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, LE.le.trans, Nat.add_le_add, Union.union, Finset 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.
def OSeq line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat
Proof uses: Finset.card, Finset.filter, Eq, totalDeg, divisorsFinset
3 instances, coercions and auxiliary constants left out.
def OSeqZ line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int
Proof uses: ite, LT.lt, OSeq, Int.toNat
7 instances, coercions and auxiliary constants left out.
def c_seq line 269 source
no axioms what this means
Statement uses: Nat, Int
Proof uses: ite, LT.lt, OfNat.ofNat, GT.gt, HAdd.hAdd, HSub.hSub, Min.min, Int.toNat
10 instances, coercions and auxiliary constants left out.
lemma c_seq_symm line 273 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Eq, c_seq, HSub.hSub, HAdd.hAdd
Proof uses: id
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma sum_telescope_c_seq line 278 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Eq, HSub.hSub, Finset.sum, Finset.Iic, c_seq, OfNat.ofNat
Proof uses: Eq.trans, Finset.range, HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_sub_distrib, Finset, of_eq_true, Iff, Membership.mem, True, forall_congr, LE.le, congr, LT.lt, iff_self, implies_true, Eq.refl and 11 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma totalDeg_three line 283 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, HAdd.hAdd, Fin
Proof uses: Eq.mpr, Finsupp.sum, id, congrArg, totalDeg.eq_1, add_assoc, Eq.trans, Finset.sum, Finset.univ, Finsupp, Finsupp.sum_fintype, of_eq_true, True, implies_congr, Eq.refl, eq_self, implies_true, Eq.rec, Eq.symm, Fin.sum_univ_three
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma card_solutions_2d line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Finset.filter, HAdd.hAdd, Prod.fst, Prod.snd, SProd.sprod, Finset, Finset.Iic, ite, GT.gt, OfNat.ofNat, HSub.hSub, Min.min
Proof uses: Eq.rec, Finset.range, Eq.trans, Finset.sum, Prod.mk, Eq.mpr, id, congrArg, Finset.card_filter, Finset.sum_product, Eq.refl, Trans.simple, And, LE.le, congr_arg, funext, dite, GE.ge, of_eq_true, True and 47 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma card_filter_eq_card_solutions line 295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, LE.le, Fin, Eq, Finset.card, Finset.filter, And, totalDeg, divisorsFinset, ite, LT.lt, Prod, HAdd.hAdd, Prod.fst, Prod.snd, HSub.hSub, SProd.sprod, Finset and 1 more
Proof uses: id, Decidable, Finsupp, Finsupp.sum, Not, Eq.mpr, congrArg, if_neg, Finset.card_bij, Membership.mem, Prod.mk, of_eq_true, Eq.trans, True, forall_congr, implies_congr_ctx, Finset.filter.congr_simp, funext, congr, Finset.sum and 43 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma c_seq_eq_card_solutions line 309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, c_seq, Finset.card, Prod, Finset.filter, HAdd.hAdd, Prod.fst, Prod.snd, SProd.sprod, Finset, Finset.Iic
Proof uses: Eq.mpr, ite, GT.gt, OfNat.ofNat, HSub.hSub, Min.min, id, congrArg, card_solutions_2d, Int.toNat, Decidable.byContradiction, Not, LT.lt, dite, if_pos, if_neg
42 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma disjoint_filter_filter_helper line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, DecidablePred, Not, And, Disjoint, Finset.filter
Proof uses: Eq.mpr, Membership.mem, id, Eq, congrArg, propext, Finset.disjoint_filter, And.intro
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma OSeq_eq_sum_c_seq_nat line 323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, Int, OSeq, Finset.sum, Finset.Iic, Fin, c_seq, HSub.hSub
Proof uses: id, Finset, Finset.filter, totalDeg, divisorsFinset, Finset.biUnion, And, Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, LE.le, congr, congrArg, Eq.trans, funext, Iff.intro, Exists.intro, Eq.mp and 33 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma OSeqZ_eq_sum_c_seq line 365 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, Eq, OSeqZ, Finset.sum, Finset.Iic, Fin, c_seq, HSub.hSub
Proof uses: id, dite, ite, LT.lt, OSeq, Int.toNat, Eq.mpr, congrArg, if_pos, Finset.sum_eq_zero, Membership.mem, Finset, Decidable.byContradiction, Not, GT.gt, HAdd.hAdd, Min.min, Eq.refl, if_neg, Int.toNat_of_nonneg and 3 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def swap02 line 385 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat
Proof uses: HAdd.hAdd, Finsupp, Fin, Finsupp.single
12 instances, coercions and auxiliary constants left out.
lemma swap02_0 line 388 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, Fin, swap02
Proof uses: of_eq_true, HAdd.hAdd, Finsupp, Finsupp.single, Eq.trans, True, congrArg, congr, Finsupp.single_eq_same, Finsupp.single_eq_of_ne, Not, False, not_false_eq_true, add_zero, eq_false_of_decide, Eq.refl, Bool, Bool.false, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma swap02_1 line 389 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, Fin, swap02
Proof uses: of_eq_true, HAdd.hAdd, Finsupp, Finsupp.single, Eq.trans, True, congrArg, congr, Finsupp.single_eq_of_ne, Not, False, not_false_eq_true, Finsupp.single_eq_same, zero_add, eq_false_of_decide, Eq.refl, Bool, Bool.false, add_zero, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma swap02_2 line 390 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, Fin, swap02
Proof uses: of_eq_true, HAdd.hAdd, Finsupp, Finsupp.single, Eq.trans, True, congrArg, congr, Finsupp.single_eq_of_ne, Not, False, eq_false_of_decide, Eq.refl, Bool, Bool.false, not_false_eq_true, add_zero, Finsupp.single_eq_same, zero_add, eq_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma totalDeg_swap02 line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, swap02
Proof uses: id, Eq.mpr, Finsupp.sum, Fin, HAdd.hAdd, Finsupp, Finsupp.single, congr, congrArg, Eq.trans, Finset.sum, Top.top, Finset, add_comm, Zero, AddCommMonoid, Top, HasSubset.Subset, Finsupp.support, Membership.mem and 27 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma swap02_swap02 line 395 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, swap02
Proof uses: Eq.mpr, HAdd.hAdd, Finsupp, Fin, Finsupp.single, id, congrArg, congr, Eq.trans, Finsupp.single_eq_same, Finsupp.single_add, Finsupp.single_eq_of_ne, of_eq_true, Not, True, False, eq_false, not_false, not_false_eq_true, eq_true and 12 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma swap02_divisors line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Iff, Membership.mem, Finset, divisorsFinset, swap02
Proof uses: id, Eq.mpr, Finsupp, Fin, Finset.Iic, HAdd.hAdd, Finsupp.single, And, LE.le, Eq, congr, congrArg, Eq.trans, Fin.succ, True, and_true, Finsupp.single_eq_same, Finsupp.single_eq_of_ne, of_eq_true, Not and 11 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma OSeq_swap02 line 402 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, OSeq, swap02
Proof uses: id, Finset.card_bij, Finset.filter, totalDeg, divisorsFinset, Membership.mem, Finset, Eq.mpr, And, congrArg, propext, Finset.mem_filter, And.intro, Iff.mp, swap02_divisors, And.left, Eq.mp, totalDeg_swap02, And.right, Eq.refl and 5 more
4 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma OSeqZ_swap02 line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, Eq, OSeqZ, swap02
Proof uses: id, dite, ite, LT.lt, OSeq, Int.toNat, Eq.mpr, congrArg, if_pos, Eq.refl, Not, if_neg, OSeq_swap02
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma diff_OSeqZ_eq line 436 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, Eq, HSub.hSub, OSeqZ, c_seq, Fin
Proof uses: Finset.sum, Finset.Iic, OSeqZ_eq_sum_c_seq, Eq.mpr, id, congrArg, sum_telescope_c_seq
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def dc_seq line 444 source
no axioms what this means
Statement uses: Nat, Int
Proof uses: ite, LT.lt, OfNat.ofNat, LE.le, Min.min, Max.max, HAdd.hAdd, Neg.neg
12 instances, coercions and auxiliary constants left out.
lemma c_seq_diff_eq line 451 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Eq, HSub.hSub, c_seq, OfNat.ofNat, dc_seq
Proof uses: id
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma dc_seq_mono line 456 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, OfNat.ofNat, HAdd.hAdd, dc_seq
Proof uses: id, dite, ite, LT.lt, Min.min, Max.max, Neg.neg, Eq.mpr, Eq, congrArg, Eq.trans, ite_congr, Eq.refl, Not, if_pos, Decidable.byContradiction, if_neg
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma diff2_OSeqZ_le_zero_C line 461 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, LE.le, HSub.hSub, Fin, HAdd.hAdd, OSeqZ
Proof uses: Eq, c_seq, diff_OSeqZ_eq, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, Eq.mp, dc_seq, c_seq_diff_eq, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast and 41 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma diff2_OSeqZ_le_zero_symm line 477 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, LE.le, HSub.hSub, Fin, HAdd.hAdd, OSeqZ
Proof uses: swap02, diff2_OSeqZ_le_zero_C, Eq.mp, congrArg, Eq.symm, OSeqZ_swap02, Eq.mpr, id, Eq, swap02_2, swap02_0, swap02_1, Decidable.byContradiction, Not
32 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def swap12 line 491 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat
Proof uses: HAdd.hAdd, Finsupp, Fin, Finsupp.single
12 instances, coercions and auxiliary constants left out.
lemma swap12_0 line 494 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, Fin, swap12
Proof uses: of_eq_true, HAdd.hAdd, Finsupp, Finsupp.single, Eq.trans, True, congrArg, congr, Finsupp.single_eq_same, Finsupp.single_eq_of_ne, Not, False, not_false_eq_true, add_zero, eq_false_of_decide, Eq.refl, Bool, Bool.false, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma swap12_1 line 495 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, Fin, swap12
Proof uses: of_eq_true, HAdd.hAdd, Finsupp, Finsupp.single, Eq.trans, True, congrArg, congr, Finsupp.single_eq_of_ne, Not, False, not_false_eq_true, Finsupp.single_eq_same, zero_add, eq_false_of_decide, Eq.refl, Bool, Bool.false, add_zero, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma swap12_2 line 496 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, Fin, swap12
Proof uses: of_eq_true, HAdd.hAdd, Finsupp, Finsupp.single, Eq.trans, True, congrArg, congr, Finsupp.single_eq_of_ne, Not, False, eq_false_of_decide, Eq.refl, Bool, Bool.false, not_false_eq_true, add_zero, Finsupp.single_eq_same, zero_add, eq_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma totalDeg_swap12 line 498 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, swap12
Proof uses: id, of_eq_true, Finsupp.sum, Fin, HAdd.hAdd, Finsupp, Finsupp.single, Eq.trans, True, congr, congrArg, add_assoc, Finsupp.sum_add_index', forall_congr, eq_self, implies_true, Finsupp.sum_single_index, add_comm, Finset.sum, Finset.univ and 3 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma swap12_swap12 line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, swap12
Proof uses: id, of_eq_true, Finsupp, Fin, HAdd.hAdd, Finsupp.single, Eq.trans, True, congrArg, congr, Finsupp.single_eq_same, Finsupp.single_eq_of_ne, Not, eq_true_of_decide, Eq.refl, Bool, Bool.true, add_zero, zero_add, And and 6 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma swap12_divisors line 502 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Iff, Membership.mem, Finset, divisorsFinset, swap12
Proof uses: id, Eq.mpr, Finsupp, Fin, Finset.Iic, HAdd.hAdd, Finsupp.single, LE.le, And, Eq, Eq.trans, congr, congrArg, Fin.succ, True, eq_true, True.intro, and_true, Finsupp.single_eq_same, Finsupp.single_eq_of_ne and 15 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma OSeq_swap12 line 507 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, OSeq, swap12
Proof uses: id, Finset.card_bij, Finset.filter, totalDeg, divisorsFinset, Membership.mem, Finset, Eq.mpr, And, congrArg, propext, Finset.mem_filter, And.intro, Iff.mp, swap12_divisors, And.left, Eq.mp, totalDeg_swap12, And.right, Eq.refl and 5 more
4 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma OSeqZ_swap12 line 532 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, Eq, OSeqZ, swap12
Proof uses: id, dite, ite, LT.lt, OSeq, Int.toNat, Eq.mpr, congrArg, if_pos, Eq.refl, Not, if_neg, OSeq_swap12
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma diff2_OSeqZ_le_zero_symm2 line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, LE.le, HSub.hSub, Fin, HAdd.hAdd, OSeqZ
Proof uses: swap12, diff2_OSeqZ_le_zero_C, Eq.mp, congrArg, Eq.symm, OSeqZ_swap12, Eq.mpr, id, Eq, swap12_2, swap12_0, swap12_1
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma diff2_OSeqZ_le_zero_min line 553 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, LE.le, HSub.hSub, Min.min, Fin, HAdd.hAdd, totalDeg, OSeqZ
Proof uses: Or, And, Decidable.byContradiction, Not, Eq, totalDeg_three, diff2_OSeqZ_le_zero_C, diff2_OSeqZ_le_zero_symm, diff2_OSeqZ_le_zero_symm2
52 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma c_seq_diff_pos line 574 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, HMul.hMul, OfNat.ofNat, HAdd.hAdd, c_seq, HSub.hSub
Proof uses: Eq.mpr, ite, LT.lt, Min.min, Max.max, id, Eq, congr, GT.gt, Int.toNat, congrArg, ite_congr, Eq.trans, sub_sub, Eq.refl, Not, Int.ofNat_toNat, Decidable.byContradiction, Eq.mp, two_mul
80 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OSeqZ_diff_pos line 579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, LE.le, HMul.hMul, totalDeg, HSub.hSub, OSeqZ
Proof uses: Eq.mpr, c_seq, Fin, id, Eq, congrArg, diff_OSeqZ_eq, HAdd.hAdd, Finsupp, Eq.mp, Finsupp.sum, Eq.trans, Finset.sum, Top.top, Finset, AddCommMonoid, HasSubset.Subset, Finsupp.support, Membership.mem, Finsupp.sum_of_support_subset and 13 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma diff_OSeqZ_anti_symm line 586 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, Eq, HSub.hSub, OSeqZ, Neg.neg, HAdd.hAdd, totalDeg
Proof uses: c_seq, Fin, diff_OSeqZ_eq, Eq.mpr, Finsupp.sum, id, congrArg, Nat.cast_finsupp_sum, Eq.trans, Finset.sum, Finset.univ, Finsupp, Finsupp.sum_fintype, of_eq_true, True, implies_congr, Eq.refl, eq_true, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natCast and 9 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
def OSeq_diff line 608 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat
Proof uses: Finset.card, Finset.filter, Eq, totalDeg, SDiff.sdiff, Finset, Fin, divisorsFinset
8 instances, coercions and auxiliary constants left out.
lemma oseq_union_eq_add_diff line 611 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, HSub.hSub, HAdd.hAdd, Finset.card, Finset.filter, totalDeg, divisorsFinset, monomialInf, OSeq, OSeq_diff
Proof uses: id, tsub_eq_of_eq_add, Finsupp.sum, Fin, Finset.Iic, Finsupp.mk, Inter.inter, Finset, Finsupp.support, Min.min, SDiff.sdiff, Eq.trans, add_comm, symm, add_assoc, congr_arg, Union.union, Eq.symm, Finset.card_union_of_disjoint, Iff.mpr and 27 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma diff_eq_shifted_OSeq line 620 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, Ne, LE.le, LT.lt, Eq, OSeq_diff, monomialInf, ite, HAdd.hAdd, OSeq, HSub.hSub, Finsupp, Finsupp.single
Proof uses: Membership.mem, Finset, divisorsFinset, Iff, Eq.mpr, Finsupp.mk, Inter.inter, Finsupp.support, Min.min, id, forall_congr, Finset.Iic, implies_congr, congrArg, Iff.intro, Function.comp, LE.le.trans', inf_le_right, le_min, Or.elim and 91 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
def H_Z line 656 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int
Proof uses: HAdd.hAdd, OSeqZ, ite, LT.lt, HSub.hSub
11 instances, coercions and auxiliary constants left out.
lemma H_Z_eq line 659 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Int, Eq, H_Z, HAdd.hAdd, OSeqZ, HSub.hSub
Proof uses: id, ite, LT.lt, dite, OSeq, Int.toNat, Eq.mpr, congr, congrArg, if_pos, Decidable.byContradiction, Not, if_neg
24 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma IsUnimodal_of_Z_diff line 668 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Eq, LE.le, OfNat.ofNat, HSub.hSub, LT.lt, IsUnimodal
Proof uses: id, dite, Exists, And, HAdd.hAdd, Set.Nonempty, setOf, Classical.propDecidable, Exists.imp, Membership.mem, Set, IsUnimodal_of_Z_diff.match_1, And.intro, Nat.strongRec, Iff.mp, Not, not_lt, Function.comp, Nat.succ, False and 80 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma H_Z_eq_fun line 686 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, Int, H_Z, HAdd.hAdd, OSeq, ite, LT.lt, HSub.hSub
Proof uses: Eq.mpr, OSeqZ, id, congr, congrArg, ite_congr, Eq.refl, Not, Nat.cast_ite, of_eq_true, Int.toNat, Finset.card, Finset.filter, totalDeg, divisorsFinset, Eq.trans, True, ite_cond_eq_false, False, LE.le and 7 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma H_Z_inc line 691 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, HAdd.hAdd, Int, LE.le, HDiv.hDiv, HSub.hSub, H_Z
Proof uses: OSeqZ, OSeqZ_diff_pos, Decidable.byContradiction, HMul.hMul, Not, H_Z_eq, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 36 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma H_Z_dec line 702 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, HAdd.hAdd, Int, LT.lt, HDiv.hDiv, LE.le, HSub.hSub, H_Z
Proof uses: OSeqZ, Neg.neg, diff_OSeqZ_anti_symm, dite, HMul.hMul, OSeqZ_diff_pos, Decidable.byContradiction, Not, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 52 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma diff_c_seq_mono line 733 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, OfNat.ofNat, HAdd.hAdd, HSub.hSub, c_seq
Proof uses: Eq.mpr, ite, LT.lt, Min.min, Max.max, Int.toNat, id, Eq, Eq.trans, GT.gt, congr, congrArg, ite_congr, Eq.refl, Not, Int.ofNat_toNat, Int.pred_toNat
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma diff_c_seq_le_diff_c_seq line 740 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, Max.max, HSub.hSub, c_seq, OfNat.ofNat
Proof uses: Eq.mpr, ite, LT.lt, HAdd.hAdd, Min.min, Int.toNat, id, Eq, Eq.trans, GT.gt, congr, congrArg, ite_congr, Eq.refl, Not, Int.ofNat_toNat, Int.pred_toNat
48 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma diff_c_seq_le_zero line 746 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, Min.min, LE.le, HSub.hSub, c_seq, OfNat.ofNat
Proof uses: id, Iff.mp, Not, ite, GT.gt, HAdd.hAdd, Int.toNat, not_lt, Function.comp, False, absurd, min_le_right, min_le_left
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma diff_c_seq_ge_zero line 751 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, Max.max, OfNat.ofNat, HSub.hSub, c_seq
Proof uses: Eq.mpr, ite, LT.lt, HAdd.hAdd, Min.min, Int.toNat, id, Eq, Eq.trans, GT.gt, congrArg, congr, ite_congr, Eq.refl, Not, Int.ofNat_toNat, Int.pred_toNat, Function.comp, Decidable.byContradiction, LE.le.trans_eq and 1 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma H_Z_concave_exact line 756 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, LE.le, Fin, Eq, HAdd.hAdd, Int, LT.lt, Min.min, HSub.hSub, Max.max, H_Z
Proof uses: OSeqZ, H_Z_eq, Decidable.byContradiction, Not, c_seq, diff_OSeqZ_eq, diff_c_seq_le_zero, Eq.mpr, id, congrArg, diff_c_seq_ge_zero, diff_c_seq_le_diff_c_seq, Eq.mp, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat and 44 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma unimodal_of_OSeq_add_shifted_exact line 801 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, LE.le, Fin, Eq, HAdd.hAdd, totalDeg, IsUnimodal, OSeq, ite, LT.lt, HSub.hSub
Proof uses: Int, H_Z, IsUnimodal_of_Z_diff, HDiv.hDiv, H_Z_eq_fun, Decidable.byContradiction, Not, H_Z_inc, H_Z_dec, H_Z_concave_exact, Iff.mpr, Min.min, Or, min_lt_iff, of_eq_true, Finsupp.sum, Eq.trans, Finsupp, True, congrArg and 37 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma IsUnimodal_eq line 821 source
standard axioms: Quot.sound what this means
Statement uses: Nat, Eq, IsUnimodal
Proof uses: funext, Eq.mpr, id, congrArg, Eq.symm

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma unimodal_of_OSeq_add_shifted line 826 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, Ne, LE.le, Eq, HAdd.hAdd, totalDeg, IsUnimodal, OSeq, ite, LT.lt, HSub.hSub
Proof uses: Or, Decidable.byContradiction, Not, Fin.ext, swap02, Eq.mpr, id, congrArg, swap02_0, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, swap02_1, swap02_2, totalDeg_swap02, unimodal_of_OSeq_add_shifted_exact, IsUnimodal_eq, OSeq_swap02 and 12 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
lemma unimodal_of_two_maximals_case1 line 881 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, Eq, totalDeg, Ne, LE.le, LT.lt, IsUnimodal, HAdd.hAdd, OSeq, OSeq_diff, monomialInf
Proof uses: ite, HSub.hSub, Finsupp, Finsupp.single, funext, Eq.mpr, id, congrArg, diff_eq_shifted_OSeq, Eq.refl, Finsupp.sum, Finsupp.single_add, Mathlib.Tactic.LinearCombination'.eq_trans₃, Eq.symm, of_eq_true, Eq.trans, True, Finset.sum, Top.top, Finset and 43 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma exists_eq_empty_or_singleton line 899 source
standard axioms: Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, LE.le, Nat, Finset.card, OfNat.ofNat, Or, Eq, EmptyCollection.emptyCollection, Exists, Singleton.singleton
Proof uses: Eq.mp, congrArg, propext, Finset.card_eq_one, Finset.card_eq_zero, Nat.le_one_iff_eq_zero_or_eq_one
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma unimodal_OSeq line 903 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, IsUnimodal, totalDeg, OSeq
Proof uses: Eq, Int, OSeqZ, IsUnimodal_of_Z_diff, HDiv.hDiv, Eq.refl, le_refl, LE.le, OSeqZ_diff_pos, Decidable.byContradiction, HMul.hMul, Not, LT.lt, HSub.hSub, Neg.neg, HAdd.hAdd, diff_OSeqZ_anti_symm, dite, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl and 58 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma unimodal_of_two_maximals_case1_wrapper line 922 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, LE.le, Finset.card, Fin, Finset.filter, LT.lt, Finset.univ, IsUnimodal, HAdd.hAdd, OSeq, OSeq_diff, monomialInf
Proof uses: Or, Finset, EmptyCollection.emptyCollection, Exists, Singleton.singleton, exists_eq_empty_or_singleton, id, Eq.mpr, Finsupp, Finsupp.sum, SDiff.sdiff, divisorsFinset, Finsupp.mk, Inter.inter, Finsupp.support, Min.min, Not, Iff, Membership.mem, Ne and 31 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma oseq_union_eq_add_diff_symm line 941 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, HAdd.hAdd, OSeq, OSeq_diff, monomialInf
Proof uses: id, Finset.card, Finset.filter, totalDeg, divisorsFinset, SDiff.sdiff, Finset, Fin, Eq.mpr, Finsupp, Finsupp.sum, Finset.Iic, Finsupp.mk, Inter.inter, Finsupp.support, Min.min, Iff, Membership.mem, Ne, funext and 30 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma unimodal_of_two_maximals line 950 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, IsUnimodal, HSub.hSub, HAdd.hAdd, Finset.card, Finset.filter, divisorsFinset, monomialInf
Proof uses: OSeq, OSeq_diff, funext, Eq.mpr, id, congrArg, oseq_union_eq_add_diff, Eq.refl, Or, LE.le, Fin, LT.lt, Finset.univ, size_S1_le_1_or_size_S2_le_1, unimodal_of_two_maximals_case1_wrapper, oseq_union_eq_add_diff_symm, Eq.symm, Eq.mp
21 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
theorem P4 line 977 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ProblemP4
Proof uses: PureOrderIdeal, OfNat.ofNat, Nat, Eq, typePO, Exists, Monomial, And, Ne, Finset, maximalMonomials, PureOrderIdeal.ideal, Insert.insert, Fin, Singleton.singleton, type_two_maximals, IsUnimodal, socleDegree, pureOSequence, OrderIdeal.carrier and 55 more
31 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/oeis_51293_conjecture_0.lean:128 (different declaration text). Qualify references as P4@path.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.