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

169 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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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.
L4DEL explanation
The type is the number of maximal monomials.
— Human-written Hilbert-functions proof companion
maximalMonomials(I) filters the carrier of I, keeping exactly the members satisfying IsMaximalIn(I,·). In Lean these applications are written maximalMonomials I and IsMaximalIn I. The result turns the mathematical notion of maximal generator into a finite set that Lean can count and select from.
1. Finiteness comes from the order ideal's finite carrier.
2. Its cardinality is the type, while purity says all of its members have the same total 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, 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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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_4.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 :=
…
```
lemma card_filter_union_inter line 216 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, DecidablePred, Eq, Nat, HAdd.hAdd, Finset.card, Finset.filter, Union.union, Inter.inter
Proof uses: of_eq_true, Eq.trans, Finset.sum, ite, OfNat.ofNat, True, congr, congrArg, Finset.card_filter, AddCommMonoid, Finset.sum_union_inter, eq_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma type_two_implies_two_maximals Type two produces exactly two distinct maximal monomials line 221 source
L4DEL explanation
suppose that its two maximal monomials are
— Human-written Hilbert-functions proof companion
If a pure order ideal has type 2, its finite set of maximal monomials can be written as the pair {m₁,m₂} with m₁ ≠ m₂. This is the bridge from the numerical type hypothesis to the two concrete generators used throughout the proof.
1. typePO P = 2 is a cardinality statement about maximalMonomials P.ideal.
2. The finite-set cardinality lemma exposes two witnesses, their distinctness, and the exact pair equality in one result.
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, Eq, typePO, OfNat.ofNat, Exists, Monomial, And, Ne, Finset, maximalMonomials, PureOrderIdeal.ideal, Insert.insert, Fin, Singleton.singleton
Proof uses: id, Iff.mp, Finset.card, 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 type_two_implies_two_maximals {r : ℕ} (P : PureOrderIdeal r) (h_type : typePO P = 2) :
    ∃ m1 m2, m1 ≠ m2 ∧ maximalMonomials P.ideal = {m1, m2} := by
…
```
Mentions: PureOrderIdeal, typePO, maximalMonomials
lemma ideal_carrier_eq_union A type-two pure ideal is the union of two principal divisor sets line 226 source
L4DEL explanation
Every element of a finite order ideal lies below a maximal element
— Human-written Hilbert-functions proof companion
Once m₁ and m₂ are known to be all the maximal monomials, every monomial in the order ideal divides one of them. The carrier is therefore exactly divisorsFinset(m₁) ∪ divisorsFinset(m₂); Lean writes the two applications with spaces.
1. Downward closure puts every divisor of either maximum into the carrier.
2. Finiteness guarantees that every carrier element lies below some maximal element; the pair equality leaves only m₁ or m₂.
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, Monomial, Eq, Finset, maximalMonomials, PureOrderIdeal.ideal, Insert.insert, Fin, Singleton.singleton, OrderIdeal.carrier, Union.union, divisorsFinset
Proof uses: OrderIdeal, IsPure, Finset.Nonempty, PureOrderIdeal.mk, id, Eq.mpr, Finset.Iic, Iff, Membership.mem, Or, LE.le, Eq.trans, forall_congr, congrArg, congr, Finsupp, OrderIdeal.mk, Finset.filter, And, Classical.propDecidable and 36 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma ideal_carrier_eq_union {r : ℕ} (P : PureOrderIdeal r) (m1 m2 : Monomial r)
    (h_max_eq : maximalMonomials P.ideal = {m1, m2}) :
    P.ideal.carrier = divisorsFinset m1 ∪ divisorsFinset m2 := by
…
```
Mentions: PureOrderIdeal, Monomial, maximalMonomials, divisorsFinset
lemma pureOSeq_eq line 242 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, HAdd.hAdd, pureOSequence, Finset.card, Finset.filter, totalDeg, Inter.inter, divisorsFinset
Proof uses: id, OrderIdeal.carrier, Union.union, ideal_carrier_eq_union, Eq.mpr, congrArg, card_filter_union_inter
21 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma inter_divisorsFinset_eq line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Monomial, Exists, Eq, Finset, Inter.inter, Fin, divisorsFinset
Proof uses: Eq.mpr, Iff, And, Membership.mem, Finset.Iic, id, congrArg, funext, Eq.trans, forall_congr, Exists.intro, Min.min, Iff.trans, LE.le, and_congr, Finset.mem_Iic, Iff.symm, le_inf_iff
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma exists_single_greater_var Equal-degree distinct triples can be oriented around one exceptional coordinate line 258 source
L4DEL explanation
there is a coordinate x ∈ {0, 1, 2} such that
— Human-written Hilbert-functions proof companion
For two distinct three-variable monomials of equal total degree, the proof may order the pair so that the second exponent is larger at one coordinate x and no larger at either other coordinate. The Lean disjunction records the two possible orientations instead of silently swapping names.
1. Equal total degree says the three coordinate differences sum to zero.
2. Because the vectors differ, one sign is in the minority; choosing that coordinate and, if needed, reversing the pair gives the required inequalities.
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: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, Ne, Or, Exists, Fin, And, GT.gt, LE.le
Proof uses: Eq.mpr, LT.lt, HAdd.hAdd, id, congr, Not, congrArg, Eq.trans, Fin.succ, funext, forall_congr, True, eq_true, True.intro, and_true, propext, Fin.exists_iff_succ, eq_true_of_decide, Eq.refl, Bool and 34 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma exists_single_greater_var {m1 m2 : Monomial 3} (h_deg : totalDeg m1 = totalDeg m2) (h_neq : m1 ≠ m2) :
    (∃ x : Fin 3, m1 x > m2 x ∧ ∀ y, y ≠ x → m1 y ≤ m2 y) ∨
    (∃ x : Fin 3, m2 x > m1 x ∧ ∀ y, y ≠ x → m2 y ≤ m1 y) := by
…
```
Mentions: Monomial, totalDeg
lemma filter_union_card_eq_add_diff line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, DecidablePred, Eq, Nat, Finset.card, Finset.filter, Union.union, HAdd.hAdd, SDiff.sdiff
Proof uses: Eq.trans, congr_arg, Finset.card_union_of_disjoint, Iff.mpr, Disjoint, Membership.mem, Not, Finset.disjoint_left, of_eq_true, True, forall_congr, And, implies_congr_ctx, False, congrArg, congr, eq_true, not_true_eq_false, and_false, and_true and 2 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma diff_divisorsFinset line 268 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Monomial, Eq, Finset, SDiff.sdiff, Fin, divisorsFinset, Finset.filter, Not, LE.le
Proof uses: of_eq_true, Finset.Iic, Eq.trans, Iff, Membership.mem, True, forall_congr, And, congr, congrArg, iff_self, eq_true, True.intro, implies_true
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma not_le_of_gt_var line 272 source
standard axioms: Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, Ne, LE.le, Iff, Not, GE.ge, HAdd.hAdd
Proof uses: Iff.intro, Function.comp, Finsupp, Iff.mp, LT.lt, not_le, mt, dite, Eq, Eq.rec, Eq.symm, LE.le.trans, LE.le.not_gt
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def reduced_monomial The residual monomial after removing the exceptional-coordinate shift line 276 source
L4DEL explanation
Then |Mred | = e − c.
— Human-written Hilbert-functions proof companion
Given oriented maxima m₁,m₂ and the exceptional coordinate x, reduced_monomial lowers the x exponent of m₂ by m₁(x)+1 and leaves its other exponents unchanged. Its degree is correspondingly reduced by the same shift.
1. At x, the exponent becomes m₂(x)-m₁(x)-1.
2. Away from x, the exponent remains m₂(y), matching the manuscript's M_red construction.
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: Monomial, OfNat.ofNat, Nat, Fin
Proof uses: Equiv, Finsupp, Equiv.symm, Finsupp.equivFunOnFinite, ite, Eq, HSub.hSub
12 instances, coercions and auxiliary constants left out.
```
noncomputable def reduced_monomial (m1 m2 : Monomial 3) (x : Fin 3) : Monomial 3 :=
…
```
Mentions: Monomial
lemma bijection_diff_to_reduced line 279 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, GE.ge, HAdd.hAdd, Eq, Finset.card, Finset.filter, And, totalDeg, divisorsFinset, HSub.hSub, reduced_monomial
Proof uses: Eq.mpr, Finset.sum, Finset.Iic, ite, Finsupp.sum, Equiv, Finsupp, Equiv.symm, Finsupp.equivFunOnFinite, id, congr, congrArg, Finset.card_filter, Finset.image, Finsupp.single, Eq.symm, Finset.sum_subset, Iff.mpr, HasSubset.Subset, Finset and 72 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma pureOSeq_decomposition Split the union's degree count into a principal sequence and a shifted residual sequence line 291 source
L4DEL explanation
H(d) := hΓ (d) = hm1 (d) + 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
The degree-d monomials below m₁ contribute the first summand. Monomials below m₂ but not m₁ exist only when d ≥ m₁(x)+1; subtracting that amount in coordinate x bijects them with degree-d-(m₁(x)+1) divisors of the reduced monomial.
1. A filter-and-cardinality identity first separates the union into the first divisor set and the nonoverlapping part of the second.
2. The exceptional-coordinate bijection turns that second part into the shifted residual count, producing the manuscript's equation (2).
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, Finset.card, Finset.filter, totalDeg, Union.union, Finset, divisorsFinset, HAdd.hAdd, ite, GE.ge, HSub.hSub, reduced_monomial
Proof uses: SDiff.sdiff, filter_union_card_eq_add_diff, id, Eq.mpr, Finsupp, Finsupp.sum, Finset.Iic, Equiv, Equiv.symm, Finsupp.equivFunOnFinite, Finset.sum, Finset.univ, LT.lt, Eq.trans, congr, congrArg, Finset.filter.congr_simp, funext, Top.top, Zero and 100 more
138 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma pureOSeq_decomposition {m1 m2 : Monomial 3} (x : Fin 3)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (d : ℕ) :
    (Finset.filter (fun m => totalDeg m = d) (divisorsFinset m1 ∪ divisorsFinset m2)).card =
    (Finset.filter (fun m => totalDeg m = d) (divisorsFinset m1)).card +
    if d ≥ m1 x + 1 then
      (Finset.filter (fun m => totalDeg m = d - (m1 x + 1)) (divisorsFinset (reduced_monomial m1 m2 x))).card
    else 0 := by
…
```
Mentions: Monomial, totalDeg, divisorsFinset, reduced_monomial
def h_seq Degree counts for the divisors of one monomial line 321 source
L4DEL explanation
For g a monomial, write hg (d) = #{u ≤ g : |u| = d}.
— Human-written Hilbert-functions proof companion
h_seq(m,d) (Lean: h_seq m d) counts the divisors of m having total degree d. Geometrically this is a slice of the exponent box below m; it is the principal sequence denoted h_m(d) in the companion proof.
1. divisorsFinset m provides all exponent vectors below m.
2. Filtering by totalDeg = d and taking the cardinality produces the degree slice.
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: Monomial, OfNat.ofNat, Nat
Proof uses: Finset.card, Finset.filter, Eq, totalDeg, divisorsFinset
3 instances, coercions and auxiliary constants left out.
```
noncomputable def h_seq (m : Monomial 3) (d : ℕ) : ℕ :=
…
```
Mentions: Monomial
def diff The first backward difference of an integer-valued sequence line 324 source
L4DEL explanation
∆F (d) = F (d) − F (d − 1) (d > 0),
— Human-written Hilbert-functions proof companion
At a positive index, diff(h,d) (Lean: diff h d) is h(d)-h(d-1), the change from the preceding value. At index zero the definition uses h(0), giving the difference operator a total boundary value on natural-number indices.
1. The positive-index branch is the manuscript's ΔF(d).
2. The explicit zero branch avoids forming a predecessor outside ℕ.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
no axioms what this means
Statement uses: Nat, Int
Proof uses: ite, Eq, OfNat.ofNat, HSub.hSub
5 instances, coercions and auxiliary constants left out.
```
def diff (h : ℕ → ℤ) (d : ℕ) : ℤ :=
…
```
def diff2 The second backward difference of an integer-valued sequence line 327 source
L4DEL explanation
∆2 F (d) = ∆F (d) − ∆F (d − 1) (d > 0).
— Human-written Hilbert-functions proof companion
At a positive index, diff2(h,d) (Lean: diff2 h d) measures how the first difference changes: Δh(d)-Δh(d-1). This discrete curvature is the quantity bounded by 1 for each principal sequence and by 2 for their sum.
1. The definition reuses diff, so its boundary convention is inherited consistently.
2. Positive second difference marks local convexity of the discrete sequence; the proof isolates its only critical values.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
no axioms what this means
Statement uses: Nat, Int
Proof uses: ite, Eq, OfNat.ofNat, diff, HSub.hSub
5 instances, coercions and auxiliary constants left out.
```
def diff2 (h : ℕ → ℤ) (d : ℕ) : ℤ :=
…
```
def L_seq Count a diagonal slice of a two-dimensional exponent box line 330 source
L4DEL explanation
where LA,B (k) = #{r < A : k − r < B, r ≤ k}.
— Human-written Hilbert-functions proof companion
L_seq(A,B,d) (Lean: L_seq A B d) counts pairs of nonnegative exponents with first coordinate below A, second coordinate below B, and total degree d. Lean stores only the first coordinate because the second is forced to be d-x.
1. Finset.range A enforces 0 ≤ x < A.
2. The filter d-x < B supplies the second side of the box, while x ≤ d prevents truncated subtraction from admitting an invalid pair.
3. This is the companion's two-variable slice L_{A,B} used to assemble the three-variable count.
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: Finset.card, Finset.filter, And, LT.lt, HSub.hSub, LE.le, Finset.range
7 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/oeis_62567_conjecture_0.lean:242 (different declaration text). Qualify references as L_seq@path.
```
def L_seq (A B d : ℕ) : ℕ :=
…
```
lemma delta_L The first difference of a box slice is three threshold indicators line 333 source
L4DEL explanation
∆LA,B (d) = 1d<A + 1d<B − 1d<A+B (d > 0),
— Human-written Hilbert-functions proof companion
For positive d, the change in the diagonal slice count is one contribution from crossing each side length, corrected once when the combined length is crossed.
1. The terms d<A and d<B record the two ways a new boundary point can enter the slice.
2. The subtraction at d<A+B removes their overlap so the integer identity remains exact across every threshold.
3. This compact indicator formula is the first finite-difference input to the manuscript's second-difference computation.
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, GT.gt, OfNat.ofNat, Eq, Int, HSub.hSub, L_seq, HAdd.hAdd, ite, LT.lt
Proof uses: Eq.mpr, Finset.card, Finset.filter, And, LE.le, Finset.range, id, delta_L.match_3, cast, Eq.symm, Eq.trans, congr, congrArg, ite_congr, Eq.refl, Nat.cast_one, Not, Nat.cast_zero, delta_L.match_2, Unit and 16 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma delta_L (A B d : ℕ) (hd : d > 0) :
  (L_seq A B d : ℤ) - (L_seq A B (d - 1) : ℤ) =
  (if d < A then 1 else 0) + (if d < B then 1 else 0) - (if d < A + B then 1 else 0) := by
…
```
def H_calc Assemble a three-dimensional degree slice from two-dimensional slices line 339 source
L4DEL explanation
A direct box count gives
— Human-written Hilbert-functions proof companion
H_calc(A,B,C,d) sums the two-coordinate count L_seq(A,B,k) over possible partial degrees k, retaining only those for which the remaining exponent d-k fits below C. Lean writes these applications with spaces.
1. range (d+1) considers every k from 0 through d.
2. The guard d-k<C is exactly the bound on the third exponent.
3. The sum is a computational form of the companion's direct box count for a principal monomial divisor 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
Proof uses: Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, ite, LT.lt, HSub.hSub, L_seq
8 instances, coercions and auxiliary constants left out.
```
def H_calc (A B C d : ℕ) : ℕ :=
…
```
lemma H_eq_H_calc The box-count formula equals the actual monomial divisor count line 342 source
L4DEL explanation
A direct box count gives
— Human-written Hilbert-functions proof companion
For a three-variable monomial m, the number of divisors of degree d is exactly H_calc (m 0+1) (m 1+1) (m 2+1) d.
1. A divisor is converted to its three exponent coordinates, each lying in the corresponding closed interval from zero through m(i).
2. The total-degree filter becomes the equation that those three coordinates sum to d.
3. Rearranging the finite sum leaves the first two coordinates in L_seq and the third-coordinate bound in H_calc.
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: Monomial, OfNat.ofNat, Nat, Eq, Finset.card, Finset.filter, totalDeg, divisorsFinset, H_calc, HAdd.hAdd, Fin
Proof uses: id, Trans.simple, Finsupp, Finsupp.sum, Finset.Iic, Prod, Prod.fst, Prod.snd, SProd.sprod, Finset, Finset.Icc, Finset.sum, Finset.range, ite, LT.lt, HSub.hSub, L_seq, Finset.card_equiv, Equiv.mk, Prod.mk and 73 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma H_eq_H_calc (m : Monomial 3) (d : ℕ) :
  ((divisorsFinset m).filter (fun x => totalDeg x = d)).card =
  H_calc (m 0 + 1) (m 1 + 1) (m 2 + 1) d := by
…
```
Mentions: Monomial, divisorsFinset, totalDeg, H_calc
lemma delta_H_calc First difference of the three-dimensional box count line 355 source
L4DEL explanation
∆HA,B,C (d) = LA,B (d) − 1d≥C LA,B (d − C) (d > 0).
— Human-written Hilbert-functions proof companion
At a positive degree, the change in H_calc is the new two-dimensional slice at d, minus the slice that falls out after shifting by the third side length C.
1. Before degree C, no slice falls out and the correction term is zero.
2. From degree C onward, L_seq A B (d-C) is subtracted.
3. This is the Lean form of the companion's second first-difference identity.
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, GT.gt, OfNat.ofNat, Eq, Int, HSub.hSub, H_calc, L_seq, ite, GE.ge
Proof uses: Eq.mpr, HAdd.hAdd, id, Eq.rec, Finset.sum, Finset.range, LT.lt, cast, Eq.symm, Eq.trans, congrArg, ite_congr, Eq.refl, Not, Nat.cast_zero, congr, delta_H_calc.match_2, Finset.sum_range_succ_comm, add_assoc, delta_L.match_2 and 46 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma delta_H_calc (A B C d : ℕ) (hd : d > 0) :
  (H_calc A B C d : ℤ) - (H_calc A B C (d - 1) : ℤ) =
  (L_seq A B d : ℤ) - (if d ≥ C then (L_seq A B (d - C) : ℤ) else 0) := by
…
```
Mentions: H_calc
def Z_calc The seven-threshold formula for discrete curvature line 364 source
L4DEL explanation
∆2 hm (d) = Z(A, B, C, d)
— Human-written Hilbert-functions proof companion
Z_calc(A,B,C,d) (Lean: Z_calc A B C d) combines three single-side, three pair-sum, and one triple-sum indicators. Its value is the exact second difference of a three-dimensional monomial box count.
1. The three positive indicators register whether d is below each side length.
2. The three negative indicators correct pairwise overlaps, and the final positive indicator restores the triple overlap.
3. This inclusion-exclusion shape is why the second difference can later be bounded and classified by elementary integer arithmetic.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
no axioms what this means
Statement uses: Nat, Int
Proof uses: HAdd.hAdd, HSub.hSub, ite, LT.lt, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
def Z_calc (A B C d : ℕ) : ℤ :=
…
```
lemma L_seq_zero line 369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, L_seq, OfNat.ofNat, ite, And, LT.lt
Proof uses: Eq.mpr, Finset.card, Finset.filter, Not, Finset.range, id, congr, HSub.hSub, LE.le, congrArg, Finset, Finset.filter.congr_simp, funext, Ne, Eq.trans, zero_tsub, Eq.refl, ite_congr, Nat.casesAuxOn, of_eq_true and 32 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma H_calc_zero line 374 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, H_calc, OfNat.ofNat, ite, LT.lt, L_seq
Proof uses: id, Eq.mpr, Finset.sum, Finset.range, HAdd.hAdd, HSub.hSub, congrArg, Finset.sum_range_one, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma diff2_H_calc_eq_1 Verify the curvature formula at the first positive degree line 379 source
L4DEL explanation
∆2 hm (d) = Z(A, B, C, d)
— Human-written Hilbert-functions proof companion
The general predecessor algebra has a boundary at d=1; this lemma checks directly that diff2 H_calc 1 still equals Z_calc A B C 1.
1. Both diff and diff2 are unfolded using their special value at zero.
2. The possible small side lengths are split so every indicator and finite slice can be evaluated exactly.
3. This is Lean boundary bookkeeping for the manuscript's all-positive-degree formula, not an additional mathematical assumption.
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, Eq, Int, diff2, H_calc, OfNat.ofNat, Z_calc
Proof uses: id, Eq.mpr, ite, diff, Finset.sum, Finset.range, HAdd.hAdd, LT.lt, HSub.hSub, L_seq, And, Not, Finset.card, Finset.filter, LE.le, congr, False, congrArg, ite_congr, eq_false and 95 more
156 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_calc_eq_1 (A B C : ℕ) :
  diff2 (fun k => (H_calc A B C k : ℤ)) 1 = Z_calc A B C 1 := by
…
```
Mentions: diff2, H_calc, Z_calc
lemma diff2_H_calc_d_unfold Expand a positive second difference into two neighbouring slice differences line 389 source
L4DEL explanation
∆HA,B,C (d) = LA,B (d) − 1d≥C LA,B (d − C) (d > 0).
— Human-written Hilbert-functions proof companion
For d>1, this lemma substitutes the first-difference formula at d and d-1, exposing the subtraction whose simplification produces Z_calc.
1. The hypotheses eliminate the zero branches of both finite-difference definitions.
2. delta_H_calc supplies the two adjacent first differences.
3. The conclusion deliberately remains expanded so the ordinary and C-shifted L_seq changes can be simplified separately.
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, GT.gt, OfNat.ofNat, Eq, Int, diff2, H_calc, HSub.hSub, L_seq, ite, GE.ge
Proof uses: id, diff, Ne, Eq.mpr, congrArg, if_neg, delta_H_calc, Decidable.byContradiction, Not, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat and 45 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_calc_d_unfold (A B C d : ℕ) (hd : d > 1) :
  diff2 (fun k => (H_calc A B C k : ℤ)) d =
  (L_seq A B d : ℤ) - (if d ≥ C then (L_seq A B (d - C) : ℤ) else 0) -
  ((L_seq A B (d - 1) : ℤ) - (if d - 1 ≥ C then (L_seq A B (d - 1 - C) : ℤ) else 0)) := by
…
```
Mentions: diff2, H_calc
lemma diff2_H_calc_L2 Normalize the shifted slice difference across its threshold line 401 source
L4DEL explanation
∆HA,B,C (d) = LA,B (d) − 1d≥C LA,B (d − C) (d > 0).
— Human-written Hilbert-functions proof companion
The correction term in delta_H_calc changes form depending on whether d lies above, at, or below C; this lemma states those three cases explicitly.
1. Above C, both neighbouring correction slices exist and their difference remains.
2. At C, only the new zero-degree slice exists; below C, neither correction contributes.
3. Isolating this threshold case prevents natural-number truncated subtraction from hiding the boundary behavior.
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, GT.gt, OfNat.ofNat, Eq, Int, HSub.hSub, ite, GE.ge, L_seq
Proof uses: Or, LT.lt, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, if_pos, Eq.refl, if_neg, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat and 4 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_calc_L2 (A B C d : ℕ) (hd : d > 1) :
  (if d ≥ C then (L_seq A B (d - C) : ℤ) else 0) - (if d - 1 ≥ C then (L_seq A B (d - 1 - C) : ℤ) else 0) =
    if d > C then (L_seq A B (d - C) : ℤ) - (L_seq A B (d - 1 - C) : ℤ) else if d = C then (L_seq A B 0 : ℤ) else 0 := by
…
```
lemma diff2_H_calc_eq_d Derive the seven-indicator curvature formula above the boundary line 425 source
L4DEL explanation
∆2 hm (d) = Z(A, B, C, d)
— Human-written Hilbert-functions proof companion
For d>1, the expanded second difference of H_calc simplifies exactly to Z_calc A B C d.
1. The unshifted L_seq change becomes its three-indicator formula through delta_L.
2. diff2_H_calc_L2 handles the shifted change, with separate cases above, at, and below C.
3. Integer arithmetic then combines the two expressions into the seven-term inclusion-exclusion formula.
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, GT.gt, OfNat.ofNat, Eq, Int, diff2, H_calc, Z_calc
Proof uses: Eq.mpr, HSub.hSub, L_seq, ite, GE.ge, id, congrArg, diff2_H_calc_d_unfold, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.sub_pf and 28 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_calc_eq_d (A B C d : ℕ) (hd : d > 1) :
  diff2 (fun k => (H_calc A B C k : ℤ)) d = Z_calc A B C d := by
…
```
Mentions: diff2, H_calc, Z_calc
lemma diff2_H_calc_eq The box count has the manuscript's curvature formula at every positive degree line 459 source
L4DEL explanation
∆2 hm (d) = Z(A, B, C, d)
— Human-written Hilbert-functions proof companion
diff2 H_calc d = Z_calc A B C d for all positive d, joining the direct d=1 boundary proof with the uniform argument for d>1.
1. Positivity leaves exactly the cases d=1 or d>1.
2. diff2_H_calc_eq_1 closes the boundary and diff2_H_calc_eq_d closes every later degree.
3. Later lemmas transfer this computational identity from H_calc back to the actual divisor-count 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, GT.gt, OfNat.ofNat, Eq, Int, diff2, H_calc, Z_calc
Proof uses: Or, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, diff2_H_calc_eq_1, diff2_H_calc_eq_d
13 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_calc_eq (A B C d : ℕ) (hd : d > 0) :
  diff2 (fun k => (H_calc A B C k : ℤ)) d = Z_calc A B C d := by
…
```
Mentions: diff2, H_calc, Z_calc
lemma Z_calc_le_one The curvature indicator expression never exceeds one line 467 source
L4DEL explanation
In particular Z(A, B, C, d) ≤ 1
— Human-written Hilbert-functions proof companion
Regardless of the side lengths or degree, the inclusion-exclusion integer Z_calc A B C d is at most 1.
1. Each comparison is a zero-or-one threshold indicator.
2. Their nesting relationships rule out any combination with total larger than one.
3. Transferred through diff2_H_calc_eq, this is the one-summand curvature bound driving the rest of the proof.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, Int, Z_calc, OfNat.ofNat
Proof uses: id, Decidable.byContradiction, HAdd.hAdd, HSub.hSub, ite, LT.lt, Not
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma Z_calc_le_one (A B C d : ℕ) : Z_calc A B C d ≤ 1 := by
…
```
Mentions: Z_calc
lemma diff2_eq_func Pointwise equal sequences have equal second differences line 471 source
L4DEL explanation
For an integer-valued sequence F : N → Z set
— Human-written Hilbert-functions proof companion
If two integer-valued sequences agree at every natural index, their diff2 values agree at any selected degree.
1. Function extensionality upgrades the pointwise equality to equality of functions.
2. Rewriting by that equality transports the finite-difference expression without redoing its arithmetic.
3. The proof uses this bridge to replace the semantic monomial count by the explicit H_calc formula.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Quot.sound what this means
Statement uses: Nat, Int, Eq, diff2
Proof uses: funext, Eq.mpr, id, congrArg, Eq.refl

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_eq_func {h1 h2 : ℕ → ℤ} (heq : ∀ d, h1 d = h2 d) (d : ℕ) :
  diff2 h1 d = diff2 h2 d := by
…
```
Mentions: diff2
lemma diff2_h_seq_le_one A single monomial's degree-count sequence has second difference at most one line 476 source
L4DEL explanation
In particular Z(A, B, C, d) ≤ 1, hence ∆2 hm (d) ≤ 1 for every d
— Human-written Hilbert-functions proof companion
For every three-variable monomial and degree, the discrete second difference of its divisor-count sequence is at most 1. This is the uniform curvature bound obtained from the companion's explicit seven-indicator box-count formula.
1. The Lean proof identifies diff2 h_seq with the integer expression Z_calc.
2. Arithmetic on the indicator thresholds proves Z_calc ≤ 1, including the boundary case at degree zero.
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: Monomial, OfNat.ofNat, Nat, LE.le, Int, diff2, h_seq
Proof uses: Or, Eq, GT.gt, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, ite, diff, HSub.hSub, rfl, if_pos, Finset.card, Finset.filter, totalDeg, divisorsFinset, Exists, Iff, And and 41 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_h_seq_le_one (m : Monomial 3) (d : ℕ) :
  diff2 (fun k => (h_seq m k : ℤ)) d ≤ 1 := by
…
```
Mentions: Monomial, diff2, h_seq
lemma log_concave_core Reduce log-concavity to the only two positive second-difference cases line 504 source
L4DEL explanation
Since H(d − 1) ≥ 0 and ∆2 H(d + 1) ≤ 2, it is enough to prove
— Human-written Hilbert-functions proof companion
The algebraic identity for the log-concavity deficit expresses it as y²-x·z, where x is a nonnegative previous value, y is the first difference, and z is a second difference bounded above by 2. Nonpositive z is automatic; hypotheses for z=1 and z=2 close the remaining cases.
1. Integer arithmetic handles all possibilities below the upper bound, including negative second differences.
2. This lemma is the compact formal core behind the manuscript's reductions (9) and (10), not an independent assumption of log-concavity.
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: Int, GE.ge, OfNat.ofNat, LE.le, Eq, HPow.hPow, Nat, HMul.hMul
Proof uses: Or, Decidable.byContradiction, Not, mul_nonpos_of_nonneg_of_nonpos, sq_nonneg, Eq.mpr, id, congrArg
46 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma log_concave_core (x y z : ℤ) (hx : x ≥ 0) (hz : z ≤ 2) (hy : z = 1 → y^2 ≥ x) (hy2 : z = 2 → y^2 ≥ 2*x) :
  y^2 ≥ x * z := by
…
```
lemma diff_eq Reconstruct a sequence value from its preceding value and first difference line 518 source
L4DEL explanation
Expanding H(d) = H(d − 1) + ∆H(d)
— Human-written Hilbert-functions proof companion
At a positive degree, h(d) is exactly h(d-1)+diff h d; this is the defining first-difference equation rearranged for later algebra.
1. Positivity selects the nonzero branch of diff.
2. Integer arithmetic moves h(d-1) to the other side.
3. The identity is one half of the log-concavity-deficit expansion used in the companion's equation (8).
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Int, GT.gt, OfNat.ofNat, Eq, HAdd.hAdd, HSub.hSub, diff
Proof uses: id, Ne, Eq.mpr, ite, congrArg, if_neg, Decidable.byContradiction, Not
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma diff_eq (h : ℕ → ℤ) (d : ℕ) (hd : d > 0) :
  h d = h (d - 1) + diff h d := by
…
```
Mentions: diff
lemma diff2_eq Advance the first difference using the second difference line 525 source
L4DEL explanation
∆H(d + 1) = ∆H(d) + ∆2 H(d + 1)
— Human-written Hilbert-functions proof companion
For positive d, the next first difference is the current first difference plus the second difference at d+1.
1. The positive index makes d+1 nonzero, so diff2 unfolds to an ordinary subtraction.
2. Natural-number predecessor simplification turns (d+1)-1 back into d.
3. This is the second identity used to rewrite the log-concavity deficit in terms of discrete curvature.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Int, GT.gt, OfNat.ofNat, Eq, diff, HAdd.hAdd, diff2
Proof uses: id, Ne, Eq.mpr, ite, HSub.hSub, congrArg, if_neg, Decidable.byContradiction, Not
18 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_eq (h : ℕ → ℤ) (d : ℕ) (hd : d > 0) :
  diff h (d + 1) = diff h d + diff2 h (d + 1) := by
…
```
Mentions: diff, diff2
def shifted_h_seq Shift a principal divisor sequence behind a degree threshold line 534 source
L4DEL explanation
H(d) := hΓ (d) = hm1 (d) + 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
shifted_h_seq(m,c,d) (Lean: shifted_h_seq m c d) is zero below c and otherwise reads the divisor-count sequence of m at degree d-c.
1. The threshold prevents natural-number subtraction from creating spurious low-degree values.
2. For the reduced monomial, c=m₁(x)+1 records the exponent removed in the exceptional coordinate.
3. This packages the indicator-weighted residual term in the companion's decomposition of H.
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: Monomial, OfNat.ofNat, Nat, Int
Proof uses: ite, GE.ge, h_seq, HSub.hSub
9 instances, coercions and auxiliary constants left out.
```
noncomputable def shifted_h_seq (m : Monomial 3) (c : ℕ) (d : ℕ) : ℤ :=
…
```
Mentions: Monomial
lemma diff_add First differences distribute over pointwise addition line 537 source
L4DEL explanation
Write f (t) = hm1 (t), g(t) = 1t≥c hMred (t − c), so that H = f + g.
— Human-written Hilbert-functions proof companion
Taking the first discrete difference of h₁+h₂ gives diff h₁ + diff h₂ at every degree, including the special boundary value at zero.
1. At zero, all three expressions reduce to their sequence values at zero.
2. At positive degrees, ordinary subtraction distributes over addition.
3. This lets the two summands of the decomposed Hilbert sequence be analysed independently.
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, Int, Eq, diff, HAdd.hAdd
Proof uses: id, dite, ite, OfNat.ofNat, HSub.hSub, Eq.mpr, congr, congrArg, if_pos, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Not, if_neg and 16 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma diff_add (h1 h2 : ℕ → ℤ) (d : ℕ) :
  diff (fun k => h1 k + h2 k) d = diff h1 d + diff h2 d := by
…
```
Mentions: diff
lemma diff2_add Second differences distribute over pointwise addition line 544 source
L4DEL explanation
Because ∆2 f ≤ 1 and ∆2 g ≤ 1
— Human-written Hilbert-functions proof companion
The discrete curvature of a sum is the sum of the two discrete curvatures, with the identity valid at zero as well as positive degrees.
1. diff2 is unfolded into first differences.
2. diff_add is applied to every first-difference term.
3. This converts two individual upper bounds of one into the upper bound of two for the decomposed 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, Int, Eq, diff2, HAdd.hAdd
Proof uses: id, dite, ite, OfNat.ofNat, diff, HSub.hSub, Eq.mpr, congr, congrArg, if_pos, diff_add, Eq.refl, Not, if_neg, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast and 18 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_add (h1 h2 : ℕ → ℤ) (d : ℕ) :
  diff2 (fun k => h1 k + h2 k) d = diff2 h1 d + diff2 h2 d := by
…
```
Mentions: diff2
def H_seq The decomposed degree sequence for the two-generator order ideal line 552 source
L4DEL explanation
H(d) := hΓ (d) = hm1 (d) + 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
H_seq adds the principal degree counts below m₁ to a shifted residual degree count derived from m₂. The second term is zero below the threshold m₁(x)+1, exactly encoding the piecewise decomposition of the manuscript's equation (2).
1. The result is stored as an integer-valued sequence so finite differences and signed inequalities can be used without truncated subtraction.
2. Under the orientation and equal-degree hypotheses, H_seq is later identified with the original pure 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: Monomial, OfNat.ofNat, Nat, Fin, Int
Proof uses: HAdd.hAdd, h_seq, ite, GE.ge, reduced_monomial, HSub.hSub
14 instances, coercions and auxiliary constants left out.
```
noncomputable def H_seq {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) : ℤ :=
…
```
Mentions: Monomial
lemma H_seq_eq_add Expose the decomposed Hilbert sequence as an explicit pointwise sum line 555 source
L4DEL explanation
H(d) := hΓ (d) = hm1 (d) + 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
H_seq is definitionally the principal sequence of m₁ plus the shifted sequence of the reduced monomial; this lemma presents that structure in the form expected by the finite-difference linearity lemmas.
1. The conditional in H_seq and the conditional in shifted_h_seq use the same threshold.
2. Splitting on that condition makes both sides identical in each branch.
3. The resulting equality is the formal counterpart of writing the manuscript's H as f+g.
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: Monomial, OfNat.ofNat, Nat, Fin, Eq, Int, H_seq, HAdd.hAdd, h_seq, shifted_h_seq, reduced_monomial
Proof uses: id, ite, GE.ge, HSub.hSub, Eq.mpr, congrArg, Eq.trans, Nat.cast_add, Nat.cast_ite, ite_congr, Eq.refl, Not, Nat.cast_zero, dite, congr, if_pos, if_neg
36 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma H_seq_eq_add {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) :
  H_seq (m1:=m1) (m2:=m2) x d = (fun k => (h_seq m1 k : ℤ)) d + shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1) d := by
…
```
Mentions: Monomial, H_seq, h_seq, shifted_h_seq, reduced_monomial
lemma diff2_h_seq_eq_Z_calc The actual monomial divisor sequence has the seven-indicator curvature line 565 source
L4DEL explanation
∆2 hm (d) = Z(A, B, C, d)
— Human-written Hilbert-functions proof companion
At every positive degree, the second difference of h_seq(m) equals Z_calc with side lengths one larger than the three exponents of m; Lean writes the partial application as h_seq m.
1. H_eq_H_calc gives pointwise equality between the semantic divisor count and the explicit box count.
2. diff2_eq_func transports the second difference across that equality.
3. diff2_H_calc_eq supplies the exact threshold expression on the computational side.
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: Monomial, OfNat.ofNat, Nat, GT.gt, Eq, Int, diff2, h_seq, Z_calc, HAdd.hAdd, Fin
Proof uses: H_calc, congrArg, H_eq_H_calc, diff2_eq_func, Eq.mpr, id, diff2_H_calc_eq
24 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_h_seq_eq_Z_calc (m : Monomial 3) (d : ℕ) (hd : d > 0) :
  diff2 (fun k => (h_seq m k : ℤ)) d = Z_calc (m 0 + 1) (m 1 + 1) (m 2 + 1) d := by
…
```
Mentions: Monomial, diff2, h_seq, Z_calc
lemma Z_calc_eq_zero_cases Classify where the curvature indicator can vanish line 574 source
L4DEL explanation
∆2 hm (d) = Z(A, B, C, d)
— Human-written Hilbert-functions proof companion
If Z_calc A B C d is zero, then d has crossed at least one single-side threshold while remaining below the opposite pair sum, or it has crossed the total sum.
1. The first three alternatives are symmetric in A, B, and C.
2. The last alternative is the post-support region beyond A+B+C.
3. This is a Lean case-analysis helper derived from the manuscript's indicator formula; the companion does not state this zero classification as a separate lemma.
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, Eq, Int, Z_calc, OfNat.ofNat, Or, And, GE.ge, LT.lt, HAdd.hAdd
Proof uses: id, HSub.hSub, ite, Decidable.byContradiction, Not
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma Z_calc_eq_zero_cases (A B C d : ℕ) :
  Z_calc A B C d = 0 → (d ≥ A ∧ d < B + C) ∨ (d ≥ B ∧ d < A + C) ∨ (d ≥ C ∧ d < A + B) ∨ (d ≥ A + B + C) := by
…
```
Mentions: Z_calc
lemma Z_calc_eq_one_cases Curvature one occurs only in the lower or upper box region line 579 source
L4DEL explanation
Moreover, if ∆2 hm (t) = 1, then either
— Human-written Hilbert-functions proof companion
When the indicator expression equals one, either d lies below all three side lengths or it lies above all three pair sums but below the total sum.
1. The first alternative is the lower region, where the degree slice has its unrestricted quadratic form.
2. The second alternative is the upper region, where the complementary quadratic form applies.
3. The classification turns a numerical equality into the exact geometric regions used by the manuscript's 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, Eq, Int, Z_calc, OfNat.ofNat, Or, And, LT.lt, GE.ge, HAdd.hAdd
Proof uses: id, HSub.hSub, ite, Decidable.byContradiction, Not
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma Z_calc_eq_one_cases (A B C d : ℕ) :
  Z_calc A B C d = 1 → (d < A ∧ d < B ∧ d < C) ∨ (d ≥ A + B ∧ d ≥ B + C ∧ d ≥ C + A ∧ d < A + B + C) := by
…
```
Mentions: Z_calc
lemma diff2_h_seq_eq_one_implies_pos Positive-degree curvature one forces a lower-or-upper region certificate line 584 source
L4DEL explanation
if ∆2 hm (t) = 1, then either
— Human-written Hilbert-functions proof companion
If the monomial divisor count has second difference exactly one at a positive degree, Lean returns the coordinate inequalities describing the manuscript's two permitted regions.
1. The semantic second difference is rewritten as Z_calc.
2. Z_calc_eq_one_cases gives the threshold alternatives in side-length coordinates.
3. Substituting A=m(0)+1, B=m(1)+1, and C=m(2)+1 converts them to exponent inequalities.
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: Monomial, OfNat.ofNat, Nat, GT.gt, Eq, Int, diff2, h_seq, Or, And, LE.le, Fin, GE.ge, HAdd.hAdd
Proof uses: H_calc, id, H_eq_H_calc, congrArg, diff2_eq_func, Eq.mpr, Z_calc, diff2_H_calc_eq, LT.lt, Z_calc_eq_one_cases, Or.inl, Decidable.byContradiction, Not, Or.inr
33 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_h_seq_eq_one_implies_pos (m : Monomial 3) (d : ℕ) (hd : d > 0) :
  diff2 (fun k => (h_seq m k : ℤ)) d = 1 → (d ≤ m 0 ∧ d ≤ m 1 ∧ d ≤ m 2) ∨ (d ≥ m 0 + m 1 + 2 ∧ d ≥ m 1 + m 2 + 2 ∧ d ≥ m 0 + m 2 + 2 ∧ d ≤ m 0 + m 1 + m 2 + 2) := by
…
```
Mentions: Monomial, diff2, h_seq
lemma diff2_h_seq_eq_one_implies Curvature one has the same two-region classification at every degree line 603 source
L4DEL explanation
if ∆2 hm (t) = 1, then either
— Human-written Hilbert-functions proof companion
This wrapper extends the positive-degree classification to degree zero, yielding one uniform lower-or-upper alternative for all natural indices.
1. At zero, the lower-region inequalities hold automatically.
2. At a positive degree, diff2_h_seq_eq_one_implies_pos supplies the full classification.
3. Later case analysis can therefore consume one theorem without reopening the boundary convention of diff2.
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: Monomial, OfNat.ofNat, Nat, Eq, Int, diff2, h_seq, Or, And, LE.le, Fin, GE.ge, HAdd.hAdd
Proof uses: GT.gt, Decidable.byContradiction, Not, Or.inl, diff2_h_seq_eq_one_implies_pos
35 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_h_seq_eq_one_implies (m : Monomial 3) (d : ℕ) :
  diff2 (fun k => (h_seq m k : ℤ)) d = 1 → (d ≤ m 0 ∧ d ≤ m 1 ∧ d ≤ m 2) ∨ (d ≥ m 0 + m 1 + 2 ∧ d ≥ m 1 + m 2 + 2 ∧ d ≥ m 0 + m 2 + 2 ∧ d ≤ m 0 + m 1 + m 2 + 2) := by
…
```
Mentions: Monomial, diff2, h_seq
lemma diff2_shifted_h_seq_eq_zero_lt A shifted divisor sequence has zero curvature before it begins line 614 source
L4DEL explanation
H(d) := hΓ (d) = hm1 (d) + 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
When d<c, the shifted residual sequence is still zero at d and at the predecessor indices used by diff2, so its second difference is exactly zero.
1. Unfolding shifted_h_seq selects the zero branch at every relevant index.
2. The result formalizes the indicator 1_{d≥c} in the companion's decomposition.
3. It also prevents the shift from contributing spurious curvature below its threshold.
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: Monomial, OfNat.ofNat, Nat, LT.lt, Eq, Int, diff2, shifted_h_seq
Proof uses: id, ite, diff, HSub.hSub, dite, GE.ge, h_seq, Eq.mpr, congrArg, Eq.trans, ite_congr, Eq.refl, Not, if_pos, Decidable.byContradiction, if_neg, congr
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_shifted_h_seq_eq_zero_lt (m : Monomial 3) (c d : ℕ) (h : d < c) :
  diff2 (shifted_h_seq m c) d = 0 := by
…
```
Mentions: Monomial, diff2, shifted_h_seq
lemma diff2_shifted_h_seq_le_one_lt The shifted summand obeys the curvature bound below its threshold line 619 source
L4DEL explanation
the same is true for the shifted sequence
— Human-written Hilbert-functions proof companion
Before the residual term turns on, its second difference is zero and therefore certainly at most one.
1. diff2_shifted_h_seq_eq_zero_lt supplies the exact zero value.
2. The remaining inequality is integer arithmetic.
3. This is the below-threshold half of the uniform one-summand curvature bound.
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: Monomial, OfNat.ofNat, Nat, LT.lt, LE.le, Int, diff2, shifted_h_seq
Proof uses: Eq.mpr, id, Eq, congrArg, diff2_shifted_h_seq_eq_zero_lt, Decidable.byContradiction, Not
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_shifted_h_seq_le_one_lt (m : Monomial 3) (c d : ℕ) (h : d < c) :
  diff2 (shifted_h_seq m c) d ≤ 1 := by
…
```
Mentions: Monomial, diff2, shifted_h_seq
lemma diff2_shifted_h_seq_eq_ge Above the threshold, shifting only translates the curvature index line 624 source
L4DEL explanation
the same is true for the shifted sequence d 7→ 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
Once d≥c, the second difference of shifted_h_seq(m,c) at d equals the second difference of the original divisor sequence at d-c; Lean writes the partial application as shifted_h_seq m c.
1. The threshold branch rewrites shifted values as h_seq m values.
2. Predecessor cases at the activation boundary are handled explicitly so the identity includes d=c.
3. The statement lets every curvature classification for h_seq be reused for the residual summand.
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: Monomial, OfNat.ofNat, Nat, GE.ge, Eq, Int, diff2, shifted_h_seq, h_seq, HSub.hSub
Proof uses: id, ite, diff, diff2_shifted_h_seq_eq_ge.match_3, LE.le, Eq.mp, diff2_shifted_h_seq_eq_ge.match_4, HAdd.hAdd, diff2_shifted_h_seq_eq_ge.match_6, diff2_shifted_h_seq_eq_ge.match_9
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_shifted_h_seq_eq_ge (m : Monomial 3) (c d : ℕ) (h : d ≥ c) :
  diff2 (shifted_h_seq m c) d = diff2 (fun k => (h_seq m k : ℤ)) (d - c) := by
…
```
Mentions: Monomial, diff2, shifted_h_seq, h_seq
lemma diff2_shifted_h_seq_le_one_ge The shifted summand obeys the curvature bound after activation line 630 source
L4DEL explanation
the same is true for the shifted sequence d 7→ 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
At and above the shift threshold, the residual curvature is just the original monomial curvature at a translated index, which is already bounded by one.
1. diff2_shifted_h_seq_eq_ge removes the shift.
2. diff2_h_seq_le_one supplies the established principal-sequence bound.
3. No new analytic estimate is introduced by this wrapper.
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: Monomial, OfNat.ofNat, Nat, GE.ge, LE.le, Int, diff2, shifted_h_seq
Proof uses: Eq, h_seq, HSub.hSub, diff2_shifted_h_seq_eq_ge, Eq.mpr, id, congrArg, diff2_h_seq_le_one
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_shifted_h_seq_le_one_ge (m : Monomial 3) (c d : ℕ) (h : d ≥ c) :
  diff2 (shifted_h_seq m c) d ≤ 1 := by
…
```
Mentions: Monomial, diff2, shifted_h_seq
lemma diff2_shifted_h_seq_le_one Every shifted principal sequence has second difference at most one line 636 source
L4DEL explanation
the same is true for the shifted sequence d 7→ 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
The curvature bound for a shifted residual sequence holds at every natural degree, whether the degree lies before or after the activation threshold.
1. The proof splits on d<c versus d≥c.
2. The two preceding lemmas close the inactive and active cases.
3. This is the second one-summand estimate used to prove diff2 H≤2.
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: Monomial, OfNat.ofNat, Nat, LE.le, Int, diff2, shifted_h_seq
Proof uses: Or, LT.lt, GE.ge, Decidable.byContradiction, Not, diff2_shifted_h_seq_le_one_lt, diff2_shifted_h_seq_le_one_ge
13 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_shifted_h_seq_le_one (m : Monomial 3) (c d : ℕ) :
  diff2 (shifted_h_seq m c) d ≤ 1 := by
…
```
Mentions: Monomial, diff2, shifted_h_seq
lemma diff2_shifted_h_seq_eq_one_implies Curvature one proves that the shifted term has activated line 643 source
L4DEL explanation
Since ∆2 g(D) = 1, necessarily D ≥ c
— Human-written Hilbert-functions proof companion
If the shifted sequence has second difference exactly one at d, then d cannot lie below c; it must satisfy d≥c.
1. Below c, the exact-zero lemma contradicts curvature one.
2. Negating the below-threshold inequality yields the activation bound.
3. This is a Lean bridge needed before translating a residual critical case back to h_seq.
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: Monomial, OfNat.ofNat, Nat, Eq, Int, diff2, shifted_h_seq, GE.ge
Proof uses: Decidable.byContradiction, Not, diff2_shifted_h_seq_eq_zero_lt, Eq.mp, LT.lt
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_shifted_h_seq_eq_one_implies (m : Monomial 3) (c d : ℕ) :
  diff2 (shifted_h_seq m c) d = 1 → d ≥ c := by
…
```
Mentions: Monomial, diff2, shifted_h_seq
lemma diff2_shifted_h_seq_eq_one_implies_eq Transfer residual curvature one to the unshifted reduced monomial line 651 source
L4DEL explanation
D ≥ c and ∆2 hMred (D − c) = 1.
— Human-written Hilbert-functions proof companion
Curvature one for the shifted residual at degree d becomes curvature one for the reduced monomial's divisor sequence at degree d-c.
1. The preceding lemma first proves that the shift is active.
2. diff2_shifted_h_seq_eq_ge supplies equality of the two second differences.
3. This exposes the lower-or-upper region classification for the reduced monomial.
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: Monomial, OfNat.ofNat, Nat, Eq, Int, diff2, shifted_h_seq, h_seq, HSub.hSub
Proof uses: GE.ge, diff2_shifted_h_seq_eq_one_implies, diff2_shifted_h_seq_eq_ge, Decidable.byContradiction, Not
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_shifted_h_seq_eq_one_implies_eq (m : Monomial 3) (c d : ℕ) :
  diff2 (shifted_h_seq m c) d = 1 → diff2 (fun k => (h_seq m k : ℤ)) (d - c) = 1 := by
…
```
Mentions: Monomial, diff2, shifted_h_seq, h_seq
lemma H_seq_eval_add Evaluate the decomposed sequence as principal plus shifted residual line 658 source
L4DEL explanation
H(d) := hΓ (d) = hm1 (d) + 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
At a concrete degree d, H_seq is the integer sum of the principal divisor count and the shifted reduced-monomial count.
1. This is the pointwise form of H_seq_eq_add.
2. It exposes the two summands used in all subsequent numerical bounds.
3. The equality mirrors the companion's equation (2) without changing its mathematical content.
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: Monomial, OfNat.ofNat, Nat, Fin, Eq, Int, H_seq, HAdd.hAdd, h_seq, shifted_h_seq, reduced_monomial
Proof uses: H_seq_eq_add
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma H_seq_eval_add {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) :
  H_seq (m1:=m1) (m2:=m2) x d = (h_seq m1 d : ℤ) + shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1) d := by
…
```
Mentions: Monomial, H_seq, h_seq, shifted_h_seq, reduced_monomial
lemma diff_H_seq_eval_add Split the first difference of the decomposed sequence line 662 source
L4DEL explanation
so that H = f + g.
— Human-written Hilbert-functions proof companion
The first difference of H_seq is the sum of the first differences of its principal and shifted-residual components.
1. Function extensionality rewrites H_seq as its two summands.
2. diff_add distributes the first-difference operator.
3. This is the formal version of the manuscript's notation ΔH=Δf+Δg.
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: Monomial, OfNat.ofNat, Nat, Fin, Eq, Int, diff, H_seq, HAdd.hAdd, h_seq, shifted_h_seq, reduced_monomial
Proof uses: funext, H_seq_eq_add, Eq.mpr, id, congrArg, diff_add, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma diff_H_seq_eval_add {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) :
  diff (H_seq (m1:=m1) (m2:=m2) x) d = diff (fun k => (h_seq m1 k : ℤ)) d + diff (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) d := by
…
```
Mentions: Monomial, diff, H_seq, h_seq, shifted_h_seq, reduced_monomial
lemma diff2_H_seq_eq_add Split the second difference of the decomposed sequence line 669 source
L4DEL explanation
Because ∆2 f ≤ 1 and ∆2 g ≤ 1
— Human-written Hilbert-functions proof companion
The discrete curvature of H_seq is exactly the sum of the curvatures of its principal and shifted-residual parts.
1. The pointwise sum representation replaces H_seq.
2. diff2_add distributes the second-difference operator.
3. This equality makes the manuscript's curvature-one and curvature-two case split exhaustive.
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: Monomial, OfNat.ofNat, Nat, Fin, Eq, Int, diff2, H_seq, HAdd.hAdd, h_seq, shifted_h_seq, reduced_monomial
Proof uses: funext, H_seq_eq_add, Eq.mpr, id, congrArg, diff2_add, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_add {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) :
  diff2 (H_seq (m1:=m1) (m2:=m2) x) d = diff2 (fun k => (h_seq m1 k : ℤ)) d + diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) d := by
…
```
Mentions: Monomial, diff2, H_seq, h_seq, shifted_h_seq, reduced_monomial
lemma diff2_H_seq_le_two The decomposed two-generator sequence has second difference at most two line 676 source
L4DEL explanation
Thus ∆2 H(d) ≤ 2.
— Human-written Hilbert-functions proof companion
Because H_seq is the sum of two principal-type sequences and each has second difference at most 1, its second difference is at most 2. This confines the positive-curvature analysis to the cases 1 and 2.
1. Finite differences distribute over the sum of the principal and shifted residual sequences.
2. Applying the one-summand bound twice yields the manuscript's inequality (4).
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: Monomial, OfNat.ofNat, Nat, Fin, LE.le, Int, diff2, H_seq
Proof uses: Eq.mpr, HAdd.hAdd, h_seq, shifted_h_seq, reduced_monomial, id, Eq, congrArg, diff2_H_seq_eq_add, diff2_h_seq_le_one, diff2_shifted_h_seq_le_one, Decidable.byContradiction, Not
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_le_two {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) :
  diff2 (H_seq (m1:=m1) (m2:=m2) x) d ≤ 2 := by
…
```
Mentions: Monomial, diff2, H_seq
lemma L_seq_le A two-variable degree slice has at most d+1 points line 685 source
L4DEL explanation
where LA,B (k) = #{r < A : k − r < B, r ≤ k}.
— Human-written Hilbert-functions proof companion
L_seq(A,B,d) filters possible first exponents from the d+1 integers between zero and d, so its cardinality cannot exceed d+1; Lean writes this as L_seq A B d.
1. Every accepted exponent belongs to the finite interval {0,…,d}.
2. Finset cardinality monotonicity supplies the bound.
3. The estimate is independent of the side lengths and feeds the unrestricted three-variable upper bound.
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, LE.le, L_seq, HAdd.hAdd, OfNat.ofNat
Proof uses: id, Finset.card, Finset.filter, And, LT.lt, HSub.hSub, Finset.range, Eq.rec, Finset.Iic, Eq, Nat.le, Finset.card_mono, of_eq_true, Membership.mem, Finset, Eq.trans, True, implies_congr_ctx, congrArg, eq_true and 2 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma L_seq_le (A B d : ℕ) : L_seq A B d ≤ d + 1 := by
…
```
lemma h_seq_le_binom A principal three-variable degree slice is bounded by all weak compositions line 689 source
L4DEL explanation
If t ≤ m(i) for all i, then
— Human-written Hilbert-functions proof companion
The divisors of a fixed monomial at degree d form a subset of all triples of nonnegative integers summing to d, of which there are (d+1)(d+2)/2.
1. Forgetting the coordinatewise upper bounds gives an injection into the unrestricted degree slice.
2. A finite counting argument evaluates that unrestricted slice by stars and bars.
3. This supplies the universal lower-region-size envelope used later in log-concavity estimates.
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: Monomial, OfNat.ofNat, Nat, LE.le, h_seq, HDiv.hDiv, HMul.hMul, HAdd.hAdd
Proof uses: id, Trans.simple, Finset.card, Finsupp, Fin, Finset.filter, Eq, totalDeg, divisorsFinset, Nat.card, setOf, Eq.mpr, Subtype, And, Membership.mem, Finset, Finset.Iic, Finsupp.sum, congr, congrArg and 103 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma h_seq_le_binom (m : Monomial 3) (d : ℕ) :
  h_seq m d ≤ (d + 1) * (d + 2) / 2 := by
…
```
Mentions: Monomial, h_seq
lemma h_seq_pure_lower Exact quadratic formula in the lower box region line 709 source
L4DEL explanation
2hm (t) = (t + 1)(t + 2),
— Human-written Hilbert-functions proof companion
If d does not exceed any exponent of m, none of the divisor-box ceilings are active, so twice the degree count is (d+1)(d+2).
1. Under the hypotheses, every weak composition of d automatically divides m.
2. Counting the unrestricted triples gives the binomial coefficient choose(d+2,2).
3. Multiplication by two avoids division in the integer-valued form used by later inequalities.
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: Monomial, OfNat.ofNat, Nat, And, LE.le, Fin, Eq, Int, HMul.hMul, h_seq, HAdd.hAdd
Proof uses: Eq.mpr, id, Eq.trans, congrArg, Eq.symm, Nat.cast_one, congr, Finset.card, Finset.filter, totalDeg, divisorsFinset, h_seq.eq_1, Trans.simple, Finsupp.sum, Finset.Iic, Nat.card, setOf, Finset.sum, Finset.univ, Subtype and 110 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma h_seq_pure_lower (m : Monomial 3) (d : ℕ) (h : d ≤ m 0 ∧ d ≤ m 1 ∧ d ≤ m 2) :
  (h_seq m d : ℤ) * 2 = (d + 1) * (d + 2) := by
…
```
Mentions: Monomial, h_seq
lemma h_seq_pure_lower_diff First difference in the lower region is d+2 line 728 source
L4DEL explanation
∆hm (t) = t + 1.
— Human-written Hilbert-functions proof companion
When degree d+1 remains below every exponent ceiling, subtracting consecutive lower-region quadratic formulas gives first difference d+2.
1. h_seq_pure_lower evaluates the counts at d+1 and d.
2. The definition of diff reduces to their subtraction.
3. Ring arithmetic cancels the two quadratic expressions.
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: Monomial, OfNat.ofNat, Nat, And, LE.le, HAdd.hAdd, Fin, Eq, Int, diff, h_seq
Proof uses: HMul.hMul, h_seq_pure_lower, Decidable.byContradiction, Not, id, Ne, Eq.mpr, ite, HSub.hSub, congrArg, if_neg, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.sub_congr and 61 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma h_seq_pure_lower_diff (m : Monomial 3) (d : ℕ) (h : d + 1 ≤ m 0 ∧ d + 1 ≤ m 1 ∧ d + 1 ≤ m 2) :
  diff (fun k => (h_seq m k : ℤ)) (d + 1) = d + 2 := by
…
```
Mentions: Monomial, diff, h_seq
lemma h_seq_symm A monomial divisor sequence is symmetric about half its total degree line 748 source
L4DEL explanation
Finally, for all t one has the universal upper estimate
— Human-written Hilbert-functions proof companion
Divisors of m at degree d are in bijection with complementary divisors m-u at degree |m|-d.
1. Coordinatewise subtraction stays inside the same exponent box.
2. Applying the complement twice returns the original divisor.
3. This Lean symmetry bridge derives the companion's upper-region formulas from the lower-region count.
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: Monomial, OfNat.ofNat, Nat, LE.le, HAdd.hAdd, Fin, Eq, h_seq, HSub.hSub
Proof uses: id, Finset.card, Finset.filter, totalDeg, divisorsFinset, Finsupp.sum, Finset.Iic, Eq.mpr, Finsupp, Finset.sum, ite, congrArg, Finset.card_filter, Finset.image, Finset.univ, HSMul.hSMul, Finsupp.single, Finset.Icc, Finset, of_eq_true and 74 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma h_seq_symm (m : Monomial 3) (d : ℕ) (hd : d ≤ m 0 + m 1 + m 2) :
  h_seq m d = h_seq m (m 0 + m 1 + m 2 - d) := by
…
```
Mentions: Monomial, h_seq
lemma h_seq_upper_bound_int Universal complementary quadratic upper bound line 763 source
L4DEL explanation
2hm (t) ≤ (|m| − t + 1)(|m| − t + 2),
— Human-written Hilbert-functions proof companion
Below the total degree, twice h_seq(m,d) is at most (|m|-d+1)(|m|-d+2), the number of unrestricted complementary triples; Lean writes the application as h_seq m d.
1. h_seq_symm moves degree d to complementary degree |m|-d.
2. Forgetting the exponent ceilings gives the unrestricted weak-composition bound there.
3. The integer cast preserves the inequality in the signed arithmetic used by the main 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: Monomial, OfNat.ofNat, Nat, LE.le, HAdd.hAdd, Fin, Int, HMul.hMul, h_seq, HSub.hSub
Proof uses: Eq, h_seq_symm, congrArg, Eq.mpr, id, Finsupp, Finset.card, Finset.filter, totalDeg, divisorsFinset, Finsupp.sum, Finset.Iic, Trans.simple, Nat.card, setOf, Finset.sum, Finset.univ, Subtype, And, Eq.trans and 110 more
159 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
```
lemma h_seq_upper_bound_int (m : Monomial 3) (d : ℕ) (h_le : d ≤ m 0 + m 1 + m 2) :
  (h_seq m d : ℤ) * 2 ≤ (m 0 + m 1 + m 2 - d + 1 : ℤ) * (m 0 + m 1 + m 2 - d + 2 : ℤ) := by
…
```
Mentions: Monomial, h_seq
lemma h_seq_pure_upper Exact complementary quadratic formula in the upper box region line 790 source
L4DEL explanation
2hm (t) = (|m| + 1 − t)(|m| + 2 − t),
— Human-written Hilbert-functions proof companion
Once d lies beyond every pairwise exponent sum, the complementary degree is below every exponent ceiling, giving the exact upper-tail formula for the divisor count.
1. For d≤|m|, symmetry reduces the claim to h_seq_pure_lower at |m|-d.
2. The endpoint d=|m|+1 is handled separately, where the count is zero.
3. The result is the Lean version of the companion's equation (5).
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: Monomial, OfNat.ofNat, Nat, And, GE.ge, HAdd.hAdd, Fin, LE.le, Eq, Int, HMul.hMul, h_seq, HSub.hSub
Proof uses: Or, Decidable.byContradiction, Not, h_seq_symm, congrArg, Eq.mpr, id, h_seq_pure_lower, Eq.mp, Membership.mem, Finset, divisorsFinset, totalDeg, Eq.trans, Finset.card, Finset.filter, EmptyCollection.emptyCollection, Finsupp, Finset.Iic, LT.lt.ne and 23 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma h_seq_pure_upper (m : Monomial 3) (d : ℕ) (h : d ≥ m 0 + m 1 ∧ d ≥ m 1 + m 2 ∧ d ≥ m 0 + m 2 ∧ d ≤ m 0 + m 1 + m 2 + 1) :
  (h_seq m d : ℤ) * 2 = (m 0 + m 1 + m 2 + 1 - d : ℤ) * (m 0 + m 1 + m 2 + 2 - d : ℤ) := by
…
```
Mentions: Monomial, h_seq
lemma h_seq_pure_upper_diff First difference in the upper region is negative complementary distance line 813 source
L4DEL explanation
∆hm (t) = −(|m| + 2 − t).
— Human-written Hilbert-functions proof companion
In the upper box region, subtracting the exact complementary quadratic formulas at adjacent degrees gives Δh(d)=-(|m|+2-d).
1. h_seq_pure_upper evaluates both neighbouring counts.
2. Positivity of d selects the ordinary subtraction branch of diff.
3. Ring arithmetic yields the companion's equation (6).
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: Monomial, OfNat.ofNat, Nat, And, GE.ge, HAdd.hAdd, Fin, LE.le, Eq, Int, diff, h_seq, Neg.neg, HSub.hSub
Proof uses: Decidable.byContradiction, Not, HMul.hMul, h_seq_pure_upper, id, Ne, Eq.mpr, ite, congrArg, if_neg, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf and 59 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma h_seq_pure_upper_diff (m : Monomial 3) (d : ℕ) (h : d ≥ m 0 + m 1 + 1 ∧ d ≥ m 1 + m 2 + 1 ∧ d ≥ m 0 + m 2 + 1 ∧ d ≤ m 0 + m 1 + m 2 + 1) :
  diff (fun k => (h_seq m k : ℤ)) d = - (m 0 + m 1 + m 2 + 2 - d : ℤ) := by
…
```
Mentions: Monomial, diff, h_seq
lemma int_add_eq_two_of_le_one A sum of two one-bounded integers reaches two only as one plus one line 832 source
L4DEL explanation
The case ∆2 H(d + 1) = 2. Then ∆2 f (d + 1) = ∆2 g(d + 1) = 1.
— Human-written Hilbert-functions proof companion
If a≤1, b≤1, and a+b=2, then both summands must equal one.
1. The lemma is elementary integer arithmetic.
2. Its role is semantic: curvature two for H=f+g forces curvature one in both summands.
3. It introduces no extra mathematical hypothesis beyond the two individual curvature bounds.
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: Int, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, And
Proof uses: Decidable.byContradiction, Not
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma int_add_eq_two_of_le_one (a b : ℤ) (ha : a ≤ 1) (hb : b ≤ 1) (hab : a + b = 2) : a = 1 ∧ b = 1 := by omega
```
lemma diff2_H_seq_eq_two_implies_both_one Curvature two means both component curvatures equal one line 834 source
L4DEL explanation
The case ∆2 H(d + 1) = 2. Then ∆2 f (d + 1) = ∆2 g(d + 1) = 1.
— Human-written Hilbert-functions proof companion
If the decomposed sequence has second difference two, its principal and shifted-residual summands must each contribute their maximum possible curvature one.
1. diff2_H_seq_eq_add rewrites the total curvature as the sum of component curvatures.
2. Each component is bounded above by one.
3. int_add_eq_two_of_le_one forces equality in both bounds.
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: Monomial, OfNat.ofNat, Nat, Fin, Eq, Int, diff2, H_seq, And, h_seq, shifted_h_seq, reduced_monomial, HAdd.hAdd
Proof uses: diff2_H_seq_eq_add, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, int_add_eq_two_of_le_one, diff2_h_seq_le_one, diff2_shifted_h_seq_le_one
21 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_two_implies_both_one {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) :
  diff2 (H_seq (m1:=m1) (m2:=m2) x) d = 2 →
…
```
Mentions: Monomial, diff2, H_seq
lemma int_add_eq_one_of_le_one_cases A sum of two one-bounded integers equals one in exactly two zero-one cases line 843 source
L4DEL explanation
if ∆2 H(d + 1) = 1, then either
— Human-written Hilbert-functions proof companion
Under upper bounds a≤1 and b≤1, an integer sum of one forces either (a,b)=(1,0) or (0,1).
1. Negative alternatives cannot compensate without pushing the other summand above one.
2. Presburger arithmetic proves the exhaustive disjunction.
3. This is the formal splitter for the manuscript's cases A and B.
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: Int, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, Or, And
Proof uses: Decidable.byContradiction, Not
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma int_add_eq_one_of_le_one_cases (a b : ℤ) (ha : a ≤ 1) (hb : b ≤ 1) (hab : a + b = 1) :
  (a = 1 ∧ b = 0) ∨ (a = 0 ∧ b = 1) := by omega
```
lemma diff2_H_seq_eq_one_implies_cases Curvature one splits into the manuscript's principal or residual case line 846 source
L4DEL explanation
∆2 f (d + 1) = 1, ∆2 g(d + 1) = 0,
— Human-written Hilbert-functions proof companion
When H=f+g has second difference one, exactly one component has curvature one and the other has curvature zero.
1. The total second difference is rewritten as the component sum.
2. Both component curvatures are at most one.
3. The integer splitter returns the two alternatives labeled A and B in the companion.
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: Monomial, OfNat.ofNat, Nat, Fin, Eq, Int, diff2, H_seq, Or, And, h_seq, shifted_h_seq, reduced_monomial, HAdd.hAdd
Proof uses: diff2_H_seq_eq_add, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, int_add_eq_one_of_le_one_cases, diff2_h_seq_le_one, diff2_shifted_h_seq_le_one
21 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_one_implies_cases {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) :
  diff2 (H_seq (m1:=m1) (m2:=m2) x) d = 1 →
…
```
Mentions: Monomial, diff2, H_seq
lemma log_concave_algebra_lower_eval Lower-region quadratic counts satisfy the needed square bound line 856 source
L4DEL explanation
2f (d − 1) = d(d + 1), ∆f (d) = d + 1.
— Human-written Hilbert-functions proof companion
For an active shift c≥1 and d≥c-1, the sum of the two lower-region quadratic count expressions is bounded by the square of their combined first differences.
1. Expanding the deficit expresses it as nonnegative products in d-c and c.
2. The hypotheses make every remaining factor nonnegative.
3. This arithmetic lemma packages the lower-lower configuration used in the curvature-two analysis.
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: Int, GE.ge, OfNat.ofNat, HSub.hSub, LE.le, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat
Proof uses: Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_add_overlap, Mathlib.Tactic.Ring.add_overlap_pf, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 57 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma log_concave_algebra_lower_eval (d c : ℤ) (hc : c ≥ 1) (hd : d ≥ c - 1) :
  (d) * (d + 1) + (d - c) * (d - c + 1) ≤ (d + 1 + d - c + 1) ^ 2 := by
…
```
lemma log_concave_weak_lower A lower-region principal term absorbs a bounded residual term line 869 source
L4DEL explanation
2S ≤ (U + 2)(U + 3), 2S ′ ≤ (U + 1)(U + 2),
— Human-written Hilbert-functions proof companion
If the residual value has the companion's quadratic upper bound and its first difference is nonnegative, the combined value is controlled by twice the square of the combined first difference.
1. The residual-size hypothesis substitutes its worst permitted quadratic envelope.
2. Expanding the target leaves only nonnegative terms from c≥1, d≥c, and dS≥0.
3. This helper isolates arithmetic from the surrounding monomial-region reasoning.
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: Int, LE.le, HMul.hMul, OfNat.ofNat, HSub.hSub, HAdd.hAdd, GE.ge, HPow.hPow, Nat
Proof uses: Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.pow_add, Mathlib.Tactic.Ring.pow_nat, Mathlib.Tactic.Ring.coeff_one, Mathlib.Tactic.Ring.pow_one_cast, Mathlib.Tactic.Ring.pow_bit0 and 60 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma log_concave_weak_lower (d c S dS : ℤ) (hS : 2 * S ≤ (d - c) * (d - c + 1)) (hdS : dS ≥ 0) (hc : c ≥ 1) (hd : d ≥ c) :
  d * (d + 1) + 2 * S ≤ 2 * (d + 1 + dS)^2 := by
…
```
lemma log_concave_algebra_upper_two Two upper-tail quadratics are dominated by the squared combined slope line 877 source
L4DEL explanation
The case ∆2 H(d + 1) = 2. Then ∆2 f (d + 1) = ∆2 g(d + 1) = 1.
— Human-written Hilbert-functions proof companion
For positive complementary distances k₁,k₂, the two quadratic upper-tail counts fit beneath twice the square of the sum of their negative first differences.
1. Expanding the difference produces k₁(k₁-1), k₂(k₂-1), and a positive cross term.
2. Positivity of both distances makes all three contributions nonnegative.
3. This is a general arithmetic form of the companion's final upper-upper estimate.
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: Int, GE.ge, OfNat.ofNat, LE.le, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, HSub.hSub, Neg.neg
Proof uses: Eq, 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.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.pow_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 and 57 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma log_concave_algebra_upper_two (k1 k2 : ℤ) (h1 : k1 ≥ 1) (h2 : k2 ≥ 1) :
  k1 * (k1 + 1) + k2 * (k2 + 1) ≤ 2 * (-k1 - k2)^2 := by
…
```
lemma log_concave_algebra_upper_eval The exact upper-upper region inequality line 887 source
L4DEL explanation
2(U1 + 1)(U2 + 1) + U1 + U2 + 2 ≥ 0,
— Human-written Hilbert-functions proof companion
When the two upper-region offsets satisfy U₁,U₂≥-1, their complementary quadratic counts are bounded by the square of the sum of their negative slopes.
1. Ring expansion identifies the deficit as 2(U₁+1)(U₂+1)+U₁+U₂+2.
2. Both shifted offsets are nonnegative under the hypotheses.
3. This matches the last algebraic inequality in the companion's curvature-two case.
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: Int, GE.ge, Neg.neg, OfNat.ofNat, LE.le, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, HSub.hSub
Proof uses: Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.pow_congr, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq and 55 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma log_concave_algebra_upper_eval (U1 U2 : ℤ) (h1 : U1 ≥ -1) (h2 : U2 ≥ -1) :
  (U1 + 2) * (U1 + 3) + (U2 + 2) * (U2 + 3) ≤ (- (U1 + 2) - (U2 + 2)) ^ 2 := by
…
```
lemma diff2_eq_one_reduction Shift a curvature-one square bound back by one degree line 895 source
L4DEL explanation
If ∆2 H(d + 1) = 1 and H(d + 1) ≤ (∆H(d + 1))2 , then
— Human-written Hilbert-functions proof companion
If neighbouring first differences differ by one and the earlier sequence value is reconstructed from the later one, a square bound at the later degree implies the required square bound two indices earlier.
1. The curvature-one equation rewrites the earlier first difference as the later one minus one.
2. The sequence identity rewrites the earlier value as the later value minus twice the later slope plus one.
3. Substituting the later square bound completes the square exactly as in the companion's reduction (13).
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: Int, Eq, HSub.hSub, OfNat.ofNat, LE.le, HPow.hPow, Nat
Proof uses: Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HMul.hMul, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 55 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_eq_one_reduction (H_d_minus_1 H_d_plus_1 diff_H_d diff_H_d_plus_1 : ℤ) :
  diff_H_d_plus_1 - diff_H_d = 1 →
  H_d_plus_1 - diff_H_d_plus_1 - diff_H_d = H_d_minus_1 →
  H_d_plus_1 ≤ diff_H_d_plus_1 ^ 2 →
  H_d_minus_1 ≤ diff_H_d ^ 2 := by
…
```
lemma H_seq_identity Reconstruct H(d−1) from H(d+1) and two first differences line 905 source
L4DEL explanation
H(d − 1) = H(d+1)−∆H(d+1)−∆H(d),
— Human-written Hilbert-functions proof companion
For positive d, the earlier value equals the later value minus the first differences at d+1 and d.
1. Each first difference is unfolded as a subtraction of adjacent H_seq values.
2. The middle values cancel by integer linear arithmetic.
3. This supplies the sequence identity required by diff2_eq_one_reduction.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Eq, Int, HSub.hSub, H_seq, HAdd.hAdd, diff
Proof uses: id, Ne, Eq.mpr, ite, congrArg, if_neg, Decidable.byContradiction, Not, Eq.refl, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HMul.hMul and 40 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma H_seq_identity {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0) :
  H_seq (m1:=m1) (m2:=m2) x (d + 1) - diff (H_seq (m1:=m1) (m2:=m2) x) (d + 1) - diff (H_seq (m1:=m1) (m2:=m2) x) d = H_seq (m1:=m1) (m2:=m2) x (d - 1) := by
…
```
Mentions: Monomial, H_seq, diff
lemma H_seq_diff2_reduction Shift a critical second-difference-one bound back one degree line 919 source
L4DEL explanation
If ∆2 H(d + 1) = 1 and H(d + 1) ≤ (∆H(d + 1))2 , then H(d − 1) ≤ (∆H(d))2 .
— Human-written Hilbert-functions proof companion
When the second difference at d+1 equals 1, an upper bound at d+1 by the square of its first difference implies the required bound at d-1. This is the formal version of the companion's shift reduction (13).
1. H_seq_identity rewrites the earlier value using the later value and the two neighbouring first differences.
2. The second-difference-one equation says those first differences differ by exactly one, so the later square completes to the earlier square.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Eq, Int, diff2, H_seq, HAdd.hAdd, LE.le, HPow.hPow, diff, HSub.hSub
Proof uses: diff2_eq_one_reduction, H_seq_identity
22 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma H_seq_diff2_reduction {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0) :
  diff2 (H_seq (m1:=m1) (m2:=m2) x) (d + 1) = 1 →
…
```
Mentions: Monomial, diff2, H_seq
lemma H_seq_diff_eq The first difference of H is the sum of the two component differences line 929 source
L4DEL explanation
so that H = f + g.
— Human-written Hilbert-functions proof companion
This theorem packages the decomposition H=f+g at the level of first differences, so later case proofs can reason about the principal and residual slopes separately.
1. Rewrite H_seq as the pointwise sum of h_seq m1 and the shifted reduced sequence.
2. Apply linearity of the first-difference operator.
3. This is a transport lemma for the manuscript's notation, not an extra mathematical assumption.
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: Monomial, OfNat.ofNat, Nat, Fin, Eq, Int, diff, H_seq, HAdd.hAdd, h_seq, shifted_h_seq, reduced_monomial
Proof uses: funext, H_seq_eq_add, Eq.mpr, id, congrArg, diff_add, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma H_seq_diff_eq {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) :
  diff (H_seq (m1:=m1) (m2:=m2) x) d = diff (fun k => (h_seq m1 k : ℤ)) d + diff (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) d := by
…
```
Mentions: Monomial, diff, H_seq, h_seq, shifted_h_seq, reduced_monomial
lemma shifted_h_seq_zero_of_lt line 935 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, LT.lt, Eq, Int, shifted_h_seq
Proof uses: id, Eq.mpr, ite, GE.ge, h_seq, HSub.hSub, congrArg, if_neg, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma diff_shifted_h_seq_zero_of_lt line 940 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, GT.gt, LT.lt, Eq, Int, diff, shifted_h_seq
Proof uses: id, Ne, Eq.mpr, ite, HSub.hSub, congrArg, if_neg, shifted_h_seq_zero_of_lt, Decidable.byContradiction, Not, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_zero, Mathlib.Tactic.Ring.add_pf_zero_add
24 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma diff2_H_seq_eq_one_implies_inl_low Curvature-one case A closes immediately in the principal lower region line 950 source
L4DEL explanation
Case A, lower region for f
— Human-written Hilbert-functions proof companion
When the principal summand has curvature one in its lower region, the shift has not activated yet, so the desired square bound reduces to the exact lower quadratic formula.
1. The lower-region inequalities force d+1<m1(x)+1, making the shifted residual and its first difference zero.
2. Evaluate the remaining principal value and slope by the lower formulas.
3. The resulting polynomial inequality is discharged arithmetically.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, h_seq, HAdd.hAdd, shifted_h_seq, reduced_monomial, And, H_seq, HSub.hSub, HPow.hPow, diff
Proof uses: LT.lt, Fin.isLt, Or, Decidable.byContradiction, Not, congrArg, Fin.ext, Eq.mpr, id, H_seq_eval_add, shifted_h_seq_zero_of_lt, Mathlib.Tactic.Ring.of_eq, HMul.hMul, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 70 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_one_implies_inl_low {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1 : diff2 (fun k => (h_seq m1 k : ℤ)) (d + 1) = 1)
    (h2 : diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = 0)
    (h1_low : d + 1 ≤ m1 0 ∧ d + 1 ≤ m1 1 ∧ d + 1 ≤ m1 2) :
  H_seq (m1:=m1) (m2:=m2) x (d - 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) d)^2 := by
…
```
Mentions: Monomial, totalDeg, diff2, h_seq, shifted_h_seq, reduced_monomial, H_seq, diff
lemma h_seq_zero_of_gt line 999 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, GT.gt, HAdd.hAdd, Fin, Eq, h_seq
Proof uses: Nat.rec, Nat.zero, h_seq_zero_of_gt.match_1, Nat.succ, Eq.trans, Finset.card, Finset.filter, totalDeg, divisorsFinset, Eq.mpr, id, congrArg, h_seq.eq_1, Eq.refl, LE.le, Not, Finsupp.sum, Finset.Iic, Finset, EmptyCollection.emptyCollection and 31 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma h_seq_upper_bound_int_all line 1004 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, LE.le, Int, HMul.hMul, h_seq, HAdd.hAdd, HSub.hSub, Fin
Proof uses: Or, GT.gt, Decidable.byContradiction, Not, h_seq_upper_bound_int, Eq, Eq.mp, congrArg, h_seq_zero_of_gt, cast, Eq.symm, Eq.trans, Nat.cast_zero, Eq.mpr, id, Neg.neg, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat and 60 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma h_seq_pure_upper_eval line 1029 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, GT.gt, And, GE.ge, HAdd.hAdd, Fin, LE.le, Eq, Int, HMul.hMul, h_seq, HSub.hSub, diff, Neg.neg
Proof uses: And.intro, Decidable.byContradiction, Not, h_seq_pure_upper, Eq.mp, congrArg, h_seq_pure_upper_diff
50 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma m_deg_eq_2 line 1050 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, HAdd.hAdd, Fin
Proof uses: of_eq_true, Finsupp, Eq.trans, True, congrArg, id, Eq.mp, Finsupp.sum, congr, Finset.sum, Top.top, Finset, Zero, AddCommMonoid, Top, HasSubset.Subset, Finsupp.support, Membership.mem, Finsupp.sum_of_support_subset, Finset.univ and 5 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma M_red_eq line 1055 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, HAdd.hAdd, reduced_monomial, HSub.hSub
Proof uses: m_deg_eq_2, Or, LT.lt, Fin.isLt, Decidable.byContradiction, Not, Fin.ext, Eq.mpr, id, congrArg, of_eq_true, ite, Eq.trans, True, ite_congr, eq_self, eq_true, True.intro, Eq.refl, False and 15 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
lemma inl_high_algebra line 1091 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, GE.ge, Neg.neg, OfNat.ofNat, LE.le, HMul.hMul, HAdd.hAdd, Eq, HSub.hSub, HPow.hPow, Nat
Proof uses: Decidable.byContradiction, Not, Eq.mpr, id, congrArg, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 56 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma algebra_helper_1 line 1102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Int, Eq, HSub.hSub, HAdd.hAdd, LE.le, And, GE.ge, Neg.neg
Proof uses: Decidable.byContradiction, Not
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma algebra_helper_2 line 1112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Eq, HSub.hSub, HAdd.hAdd, GE.ge, And, Int
Proof uses: Decidable.byContradiction, Not
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma algebra_helper_3 line 1116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Eq, HSub.hSub, HAdd.hAdd, GE.ge, And, Int
Proof uses: Decidable.byContradiction, Not
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ineq_helper line 1120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, HAdd.hAdd, OfNat.ofNat, LE.le, And, HSub.hSub
Proof uses: Decidable.byContradiction, Not
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma diff_shifted_h_seq_eq_ge line 1124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, GT.gt, GE.ge, Eq, Int, diff, shifted_h_seq, h_seq, HSub.hSub
Proof uses: Or, Decidable.byContradiction, Not, id, Ne, Eq.mpr, ite, congrArg, if_neg, if_pos, Eq.refl, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_zero and 6 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
lemma L_seq_eq_min line 1159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, L_seq, HSub.hSub, Min.min, HAdd.hAdd, OfNat.ofNat, ite, GE.ge
Proof uses: id, Finset.card, Finset.filter, And, LT.lt, LE.le, Finset.range, Or.elim, Not, em, Eq.rec, Eq.trans, Finset.Ico, Function.comp, Iff, Membership.mem, Finset, congr_arg, Finset.ext, Iff.trans and 23 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma L_seq_eq_min_z line 1164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, L_seq, HSub.hSub, Min.min, HAdd.hAdd, OfNat.ofNat, ite, GE.ge
Proof uses: Eq.mpr, id, congrArg, L_seq_eq_min, dite, congr, if_pos, Decidable.byContradiction, Not, if_neg
29 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma diff_h_seq_eq_L_seq line 1170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, GT.gt, Eq, Int, diff, h_seq, HSub.hSub, L_seq, HAdd.hAdd, Fin, ite, GE.ge
Proof uses: rfl, id, Ne, Eq.mpr, congrArg, if_neg, H_calc, cast, Eq.symm, H_eq_H_calc, delta_H_calc
44 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma h_seq_diff_le_zero_of_past_mid line 1182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, GE.ge, HMul.hMul, HAdd.hAdd, Fin, LE.le, Int, diff, h_seq
Proof uses: GT.gt, Decidable.byContradiction, Not, Eq.mpr, HSub.hSub, L_seq, ite, id, Eq, congrArg, diff_h_seq_eq_L_seq, Min.min, L_seq_eq_min_z, dite, if_pos, if_neg
48 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma inl_high_shift_diff line 1195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, And, GE.ge, HAdd.hAdd, Int, diff, shifted_h_seq, reduced_monomial
Proof uses: Or, LT.lt, Decidable.byContradiction, Not, diff_shifted_h_seq_zero_of_lt, Eq.mpr, id, congrArg, le_refl, h_seq, HSub.hSub, diff_shifted_h_seq_eq_ge, h_seq_diff_le_zero_of_past_mid, M_red_eq, ineq_helper, And.left, And.right, m_deg_eq_2, Fin.isLt, Fin.ext and 72 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
lemma reduced_monomial_eval_0 line 1239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, Eq, And, reduced_monomial, HSub.hSub
Proof uses: of_eq_true, Equiv, Finsupp, Equiv.symm, Finsupp.equivFunOnFinite, ite, Eq.trans, True, congr, congrArg, HAdd.hAdd, funext, ite_congr, tsub_tsub, Not, Eq.refl, ite_cond_eq_true, eq_self, ite_cond_eq_false, eq_false_of_decide and 3 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma reduced_monomial_eval_1 line 1244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, Eq, And, reduced_monomial, HSub.hSub
Proof uses: Finsupp, Finset, Iff, Membership.mem, Ne, Finsupp.mk, of_eq_true, Equiv, Equiv.symm, Finsupp.equivFunOnFinite, ite, Eq.trans, True, congr, congrArg, HAdd.hAdd, funext, ite_congr, tsub_tsub, Not and 9 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma reduced_monomial_eval_2 line 1249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, Eq, And, reduced_monomial, HSub.hSub
Proof uses: of_eq_true, Equiv, Finsupp, Equiv.symm, Finsupp.equivFunOnFinite, ite, Eq.trans, True, congr, congrArg, funext, ite_congr, Not, Eq.refl, ite_cond_eq_false, eq_false_of_decide, Bool, Bool.false, eq_self, ite_cond_eq_true and 1 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma m1_x_le_M1 line 1259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Eq, totalDeg, LE.le, HAdd.hAdd
Proof uses: m_deg_eq_2, Or, LT.lt, Fin.isLt, Decidable.byContradiction, Not, Fin.ext, Eq.symm
32 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma inl_high_H_eval_bounds_shift_d line 1268 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, HSub.hSub, HAdd.hAdd, HMul.hMul, shifted_h_seq, reduced_monomial
Proof uses: m1_x_le_M1, M_red_eq, Or, LT.lt, GE.ge, Decidable.byContradiction, Not, shifted_h_seq_zero_of_lt, Eq.mpr, id, congrArg, rfl, mul_nonneg, h_seq, ite, if_pos, Eq.refl, h_seq_upper_bound_int_all, And, algebra_helper_3 and 3 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma inl_high_H_eval_bounds_shift_d_minus_1 line 1297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, HSub.hSub, HAdd.hAdd, HMul.hMul, shifted_h_seq, reduced_monomial
Proof uses: m1_x_le_M1, M_red_eq, Or, LT.lt, GE.ge, lt_or_ge, shifted_h_seq_zero_of_lt, Eq.mpr, id, congrArg, rfl, Decidable.byContradiction, Not, mul_nonneg, h_seq, ite, if_pos, Eq.refl, h_seq_upper_bound_int_all, And and 4 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma inl_high_H_eval_bounds Curvature-one case A satisfies the square bound in the principal upper region line 1326 source
L4DEL explanation
Case A, upper region for f
— Human-written Hilbert-functions proof companion
The principal upper-tail value is exact, while the residual value has a matching quadratic envelope and nonpositive slope; together they fit under the square of the combined slope.
1. Express the principal term using the upper-region formulas with offset U1.
2. Bound the shifted term at the two neighboring degrees and show its first difference is nonpositive.
3. inl_high_algebra combines those estimates into the required inequality for H.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, And, GE.ge, HAdd.hAdd, Int, H_seq, HSub.hSub, HPow.hPow, diff
Proof uses: ineq_helper, And.left, And.right, HMul.hMul, h_seq, h_seq_pure_upper, Neg.neg, h_seq_pure_upper_diff, shifted_h_seq, reduced_monomial, inl_high_shift_diff, Eq.mpr, id, congrArg, H_seq_eval_add, Eq.refl, diff_H_seq_eval_add, algebra_helper_1, rfl, inl_high_H_eval_bounds_shift_d_minus_1 and 67 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma inl_high_H_eval_bounds {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1_high : d + 1 ≥ m1 0 + m1 1 + 2 ∧ d + 1 ≥ m1 1 + m1 2 + 2 ∧ d + 1 ≥ m1 0 + m1 2 + 2 ∧ d + 1 ≤ m1 0 + m1 1 + m1 2 + 2) :
  H_seq (m1:=m1) (m2:=m2) x (d - 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) d)^2 := by
…
```
Mentions: Monomial, totalDeg, H_seq, diff
lemma diff2_H_seq_eq_one_implies_inl_high Case A upper region is discharged by the assembled evaluation bound line 1373 source
L4DEL explanation
Case A, upper region for f
— Human-written Hilbert-functions proof companion
This wrapper identifies the upper-region branch of the principal-curvature case with the already proved inl_high_H_eval_bounds estimate.
1. Preserve the degree, monomial-order, and equal-total-degree hypotheses.
2. Forward the upper-region inequalities unchanged.
3. No new inequality is introduced here; the lemma records proof structure.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, h_seq, HAdd.hAdd, shifted_h_seq, reduced_monomial, And, GE.ge, H_seq, HSub.hSub, HPow.hPow and 1 more
Proof uses: inl_high_H_eval_bounds
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_one_implies_inl_high {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1 : diff2 (fun k => (h_seq m1 k : ℤ)) (d + 1) = 1)
    (h2 : diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = 0)
    (h1_high : d + 1 ≥ m1 0 + m1 1 + 2 ∧ d + 1 ≥ m1 1 + m1 2 + 2 ∧ d + 1 ≥ m1 0 + m1 2 + 2 ∧ d + 1 ≤ m1 0 + m1 1 + m1 2 + 2) :
  H_seq (m1:=m1) (m2:=m2) x (d - 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) d)^2 := by
…
```
Mentions: Monomial, totalDeg, diff2, h_seq, shifted_h_seq, reduced_monomial, H_seq, diff
lemma diff2_H_seq_eq_one_implies_inl Case A is complete after splitting the principal sequence into lower and upper regions line 1381 source
L4DEL explanation
if ∆2 H(d + 1) = 1, then either
— Human-written Hilbert-functions proof companion
If the principal component contributes curvature one and the residual contributes zero, the monomial curvature classifier leaves exactly the lower and upper cases already proved.
1. Classify the principal sequence with diff2_h_seq_eq_one_implies.
2. Send the lower branch to diff2_H_seq_eq_one_implies_inl_low.
3. Send the upper branch to diff2_H_seq_eq_one_implies_inl_high.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, h_seq, HAdd.hAdd, shifted_h_seq, reduced_monomial, H_seq, HSub.hSub, HPow.hPow, diff
Proof uses: Or, And, GE.ge, diff2_h_seq_eq_one_implies, diff2_H_seq_eq_one_implies_inl_low, diff2_H_seq_eq_one_implies_inl_high
39 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_one_implies_inl {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1 : diff2 (fun k => (h_seq m1 k : ℤ)) (d + 1) = 1)
    (h2 : diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = 0) :
  H_seq (m1:=m1) (m2:=m2) x (d - 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) d)^2 := by
…
```
Mentions: Monomial, totalDeg, diff2, h_seq, shifted_h_seq, reduced_monomial, H_seq, diff
lemma shifted_h_seq_eval_lower Exact value of the shifted residual in its lower region line 1393 source
L4DEL explanation
X = D − c + 1 ≥ 1.
— Human-written Hilbert-functions proof companion
Once the shift is active and the translated degree lies below every exponent ceiling, twice the residual value is the usual lower-region quadratic at d-c.
1. The threshold hypothesis selects the active branch of shifted_h_seq.
2. Apply the exact lower formula to the reduced monomial at translated degree d-c.
3. Cast the natural-number identity into the integer arithmetic of the main 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: Monomial, OfNat.ofNat, Nat, GE.ge, And, LE.le, HSub.hSub, Fin, Eq, Int, HMul.hMul, shifted_h_seq, HAdd.hAdd
Proof uses: id, Eq.mpr, ite, h_seq, congrArg, if_pos, cast, Eq.trans, Eq.symm, Nat.cast_one, congr, h_seq_pure_lower
63 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma shifted_h_seq_eval_lower (m : Monomial 3) (c d : ℕ) (hc : d ≥ c) (h_low : d - c ≤ m 0 ∧ d - c ≤ m 1 ∧ d - c ≤ m 2) :
  shifted_h_seq m c d * 2 = (d - c + 1 : ℤ) * (d - c + 2 : ℤ) := by
…
```
Mentions: Monomial, shifted_h_seq
lemma diff_shifted_h_seq_eval_lower Exact first difference of the shifted residual in its lower region line 1399 source
L4DEL explanation
2g(D) = X(X + 1), ∆g(D) = X.
— Human-written Hilbert-functions proof companion
In the active lower region, the residual slope is d-c+1, including the activation boundary where the preceding shifted value is still zero.
1. Separate the boundary case d=c from the strictly active case d>c.
2. At the boundary, evaluate h_seq m 0=1 directly.
3. Above the boundary, translate the first difference and apply the lower-region slope formula.
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: Monomial, OfNat.ofNat, Nat, GT.gt, GE.ge, And, LE.le, HSub.hSub, Fin, Eq, Int, diff, shifted_h_seq, HAdd.hAdd
Proof uses: Or, Decidable.byContradiction, Not, id, ite, Ne, Eq.mpr, h_seq, congrArg, if_neg, if_pos, H_calc, H_eq_H_calc, LT.lt, L_seq, H_calc_zero, L_seq_zero, cast, Eq.trans, Eq.symm and 55 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma diff_shifted_h_seq_eval_lower (m : Monomial 3) (c d : ℕ) (hd : d > 0) (hc : d ≥ c) (h_low : d - c ≤ m 0 ∧ d - c ≤ m 1 ∧ d - c ≤ m 2) :
  diff (shifted_h_seq m c) d = (d - c + 1 : ℤ) := by
…
```
Mentions: Monomial, diff, shifted_h_seq
lemma L_seq_le_A line 1447 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, L_seq
Proof uses: id, HasSubset.Subset, Finset, Finset.filter, And, LT.lt, HSub.hSub, Finset.range, Finset.filter_subset, Eq, Finset.card, Finset.card_range, Finset.card_le_card, Decidable.byContradiction, Not
10 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma L_seq_le_B line 1460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, L_seq
Proof uses: id, HasSubset.Subset, Finset, Finset.filter, And, LT.lt, HSub.hSub, Finset.range, Finset.Icc, HAdd.hAdd, OfNat.ofNat, Membership.mem, Eq.mpr, Eq, congrArg, propext, Finset.mem_Icc, Eq.mp, Finset.mem_range, Finset.mem_filter and 6 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma diff_h_seq_le_var_1 line 1474 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, GT.gt, LE.le, Int, diff, h_seq, HAdd.hAdd, Fin
Proof uses: Eq, rfl, HSub.hSub, id, Ne, Eq.mpr, ite, congrArg, if_neg, H_calc, cast, Eq.symm, H_eq_H_calc, L_seq, GE.ge, delta_H_calc, L_seq_le_B, dite, if_pos, Decidable.byContradiction and 1 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma diff_h_seq_le_var_0 line 1491 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, GT.gt, LE.le, Int, diff, h_seq, HAdd.hAdd, Fin
Proof uses: Eq, rfl, HSub.hSub, id, Ne, Eq.mpr, ite, congrArg, if_neg, H_calc, cast, Eq.symm, H_eq_H_calc, L_seq, GE.ge, delta_H_calc, L_seq_le_A, dite, if_pos, Decidable.byContradiction and 1 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma L_seq_sub_le line 1508 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, LE.le, Int, HSub.hSub, L_seq
Proof uses: Nat.recAux, OfNat.ofNat, Eq, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, HAdd.hAdd, ite, LT.lt, delta_L, GT.gt, Nat.succ, dite, if_pos, if_neg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 45 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma diff_h_seq_le_var line 1527 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, LE.le, Int, diff, h_seq, HAdd.hAdd
Proof uses: Or, Eq, GT.gt, Decidable.byContradiction, Not, id, Eq.mpr, ite, HSub.hSub, congrArg, if_pos, rfl, H_calc, H_eq_H_calc, LT.lt, L_seq, H_calc_zero, And, L_seq_zero, cast and 18 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
lemma h_le_diff_mul_of_diff2_nonneg line 1576 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, OfNat.ofNat, LE.le, GE.ge, diff2, HMul.hMul, diff, HAdd.hAdd
Proof uses: Nat.recAux, Eq, id, Eq.mpr, ite, HSub.hSub, congrArg, if_pos, rfl, Eq.refl, Eq.symm, Decidable.byContradiction, Not, diff_eq, GT.gt, Ne, if_neg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 57 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma h_seq_le_diff_mul_of_low line 1607 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, And, LT.lt, HAdd.hAdd, Fin, Eq, Int, Z_calc, LE.le, h_seq, HMul.hMul, diff
Proof uses: h_le_diff_mul_of_diff2_nonneg, diff2, diff2_h_seq_eq_Z_calc, Eq.mpr, GE.ge, id, congrArg, Decidable.byContradiction, HSub.hSub, ite, Not
38 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma h_seq_diff_ge_min line 1617 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, GE.ge, HAdd.hAdd, And, LT.lt, Eq, Int, Z_calc, diff, h_seq
Proof uses: Or, Fin.isLt, Decidable.byContradiction, Not, GT.gt, Eq.mpr, HSub.hSub, L_seq, ite, id, congrArg, diff_h_seq_eq_L_seq, Fin.ext, Min.min, L_seq_eq_min_z, dite, if_pos, if_neg, Eq.symm, congr
60 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
lemma inr_low_hd_bound line 1655 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, Z_calc, HAdd.hAdd, GE.ge, And, HSub.hSub, reduced_monomial, LT.lt
Proof uses: Eq.mpr, id, congr, congrArg, Eq.trans, add_right_comm, Not, Eq.mp, ite, ite_congr, Eq.refl, Nat.Simproc.add_sub_add_le, of_decide_eq_true, Bool, Bool.true
72 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma inr_low_H_eval_bounds Case B lower region supplies the four value-and-slope bounds line 1663 source
L4DEL explanation
Case B, lower region for g.
— Human-written Hilbert-functions proof companion
For a lower-region residual curvature-one event, this lemma assembles the principal growth bound, a lower bound on its slope, and exact residual value and slope formulas.
1. Convert zero principal curvature into the strict pairwise inequalities used by the manuscript.
2. Bound the principal value by its slope times the degree factor.
3. Evaluate the shifted residual exactly at translated lower-region 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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, Z_calc, HAdd.hAdd, GE.ge, And, HSub.hSub, reduced_monomial, h_seq, HMul.hMul, diff, shifted_h_seq
Proof uses: LT.lt, inr_low_hd_bound, h_seq_le_diff_mul_of_low, Decidable.byContradiction, Not, Eq.mp, congrArg, shifted_h_seq_eval_lower, diff_shifted_h_seq_eval_lower, h_seq_diff_ge_min, And.intro
46 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma inr_low_H_eval_bounds {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (hz : Z_calc (m1 0 + 1) (m1 1 + 1) (m1 2 + 1) (d + 1) = 0) (hd_c : d + 1 ≥ m1 x + 1)
    (h2_low : d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 1 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 2) :
  (h_seq m1 (d + 1) : ℤ) ≤ (diff (fun k => (h_seq m1 k : ℤ)) (d + 1)) * (d + 2 : ℤ) ∧
  diff (fun k => (h_seq m1 k : ℤ)) (d + 1) ≥ m1 x + 1 ∧
  shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1) (d + 1) * 2 = (d + 1 - (m1 x + 1) + 1 : ℤ) * (d + 1 - (m1 x + 1) + 2 : ℤ) ∧
  diff (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = (d + 1 - (m1 x + 1) + 1 : ℤ) := by
…
```
Mentions: Monomial, totalDeg, Z_calc, reduced_monomial, h_seq, diff, shifted_h_seq
lemma inr_low_master_ineq line 1686 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, GE.ge, OfNat.ofNat, Eq, HAdd.hAdd, LE.le, HMul.hMul, HPow.hPow, Nat
Proof uses: Eq.mpr, id, congrArg, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 57 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma inr_low_reduction_goal_helper Case B lower region proves the later-degree square bound line 1692 source
L4DEL explanation
H(D) ≤ (∆H(D))2 , and (13) proves (9).
— Human-written Hilbert-functions proof companion
The principal estimate and exact lower residual formula combine into H(d+1)≤(ΔH(d+1))², which is the premise needed by the one-step reduction.
1. Assemble the bounds from inr_low_H_eval_bounds.
2. Introduce the manuscript variables for the principal slope, translated residual degree, shift, and current degree.
3. Apply the packaged polynomial inequality and reconstruct H and ΔH.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, h_seq, HAdd.hAdd, shifted_h_seq, reduced_monomial, And, HSub.hSub, H_seq, HPow.hPow, diff
Proof uses: GE.ge, diff2_shifted_h_seq_eq_one_implies, Z_calc, diff2_h_seq_eq_Z_calc, Decidable.byContradiction, Not, HMul.hMul, inr_low_H_eval_bounds, Eq.symm, Eq.mp, congrArg, Eq.mpr, id, H_seq_eval_add, diff_H_seq_eval_add, Eq.refl, inr_low_master_ineq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat and 75 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma inr_low_reduction_goal_helper {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1 : diff2 (fun k => (h_seq m1 k : ℤ)) (d + 1) = 0)
    (h2 : diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = 1)
    (h2_low : d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 1 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 2) :
    H_seq (m1:=m1) (m2:=m2) x (d + 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) (d + 1))^2 := by
…
```
Mentions: Monomial, totalDeg, diff2, h_seq, shifted_h_seq, reduced_monomial, H_seq, diff
lemma diff2_H_seq_eq_one_implies_inr_low Case B lower region transfers its later-degree bound back to d−1 line 1739 source
L4DEL explanation
Case B, lower region for g.
— Human-written Hilbert-functions proof companion
After proving the square bound at d+1, the curvature-one reduction gives the exact earlier-degree inequality required for log-concavity.
1. Reconstruct total curvature one from component curvatures zero and one.
2. Use inr_low_reduction_goal_helper for the later-degree premise.
3. Apply H_seq_diff2_reduction to shift the result back.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, h_seq, HAdd.hAdd, shifted_h_seq, reduced_monomial, And, HSub.hSub, H_seq, HPow.hPow, diff
Proof uses: H_seq_diff2_reduction, Eq.mpr, id, congrArg, diff2_H_seq_eq_add, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.add_pf_zero_add, inr_low_reduction_goal_helper
50 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_one_implies_inr_low {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1 : diff2 (fun k => (h_seq m1 k : ℤ)) (d + 1) = 0)
    (h2 : diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = 1)
    (h2_low : d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 1 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 2) :
  H_seq (m1:=m1) (m2:=m2) x (d - 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) d)^2 := by
…
```
Mentions: Monomial, totalDeg, diff2, h_seq, shifted_h_seq, reduced_monomial, H_seq, diff
lemma h_seq_pure_upper_ext line 1749 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, And, GE.ge, HAdd.hAdd, Fin, LE.le, Eq, Int, HMul.hMul, h_seq, HSub.hSub
Proof uses: Or, Decidable.byContradiction, Not, h_seq_pure_upper, Eq.mpr, id, congrArg, h_seq_zero_of_gt, GT.gt, cast, Eq.symm, Eq.trans, Nat.cast_zero, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.mul_congr, Nat.rawCast, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.cast_pos and 30 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma h_seq_pure_upper_diff_ext line 1763 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, And, GE.ge, HAdd.hAdd, Fin, LE.le, Eq, Int, diff, h_seq, Neg.neg, HSub.hSub
Proof uses: Or, Decidable.byContradiction, Not, h_seq_pure_upper_diff, Eq.mpr, id, congrArg, Ne, ite, if_neg, h_seq_zero_of_gt, GT.gt, cast, Eq.symm, Eq.trans, Nat.cast_zero, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat and 30 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma inr_high_H_eval_bounds Case B upper region supplies the residual upper-tail formulas line 1783 source
L4DEL explanation
Case B, upper region for g.
— Human-written Hilbert-functions proof companion
When the residual component has curvature one in its upper region, both its value and slope are controlled by the complementary offset while the principal slope is nonpositive.
1. Translate the residual degree back through the shift.
2. Apply the exact upper value and first-difference formulas to the reduced monomial.
3. Record the principal quadratic bound and the endpoint constraint needed by the master inequality.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, Z_calc, HAdd.hAdd, GE.ge, And, HSub.hSub, reduced_monomial, HMul.hMul, h_seq, diff, shifted_h_seq
Proof uses: m1_x_le_M1, M_red_eq, congrArg, Decidable.byContradiction, Not, Eq.mp, Eq.trans, Nat.cast_add, h_seq_upper_bound_int_all, Eq.mpr, id, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr and 60 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma inr_high_H_eval_bounds {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (hz : Z_calc (m1 0 + 1) (m1 1 + 1) (m1 2 + 1) (d + 1) = 0) (hd_c : d + 1 ≥ m1 x + 1)
    (h2_high : d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + 2 ∧ d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2 ∧ d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 2 + 2 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2) :
  (h_seq m1 (d + 1) : ℤ) * 2 ≤ (m1 0 + m1 1 + m1 2 + 1 - (d + 1 : ℤ)) * (m1 0 + m1 1 + m1 2 + 2 - (d + 1 : ℤ)) ∧
  diff (fun k => (h_seq m1 k : ℤ)) (d + 1) ≤ 0 ∧
  shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1) (d + 1) * 2 = (m1 0 + m1 1 + m1 2 + 1 - (d + 1 : ℤ)) * (m1 0 + m1 1 + m1 2 + 2 - (d + 1 : ℤ)) ∧
  diff (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = (d + 1 : ℤ) - (m1 0 + m1 1 + m1 2 + 2) ∧
  (d + 1 : ℤ) ≤ m1 0 + m1 1 + m1 2 + 2 := by
…
```
Mentions: Monomial, totalDeg, Z_calc, reduced_monomial, h_seq, diff, shifted_h_seq
lemma inr_high_master_ineq line 1832 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, GE.ge, OfNat.ofNat, Neg.neg, LE.le, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat
Proof uses: Or, Eq, Decidable.byContradiction, Not, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 63 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma inr_high_reduction_goal_helper Case B upper region proves the later-degree square bound line 1840 source
L4DEL explanation
H(D) ≤ (∆H(D))2 , and (13) proves (9).
— Human-written Hilbert-functions proof companion
The two upper-tail envelopes fit beneath the square of the combined negative slope, establishing the later-degree hypothesis for the curvature-one reduction.
1. Gather the upper-region bounds for the principal and shifted residual components.
2. Normalize both components with a common complementary offset U.
3. Apply the upper master inequality and reconstruct the value and first difference of H.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, h_seq, HAdd.hAdd, shifted_h_seq, reduced_monomial, And, GE.ge, HSub.hSub, H_seq, HPow.hPow and 1 more
Proof uses: diff2_shifted_h_seq_eq_one_implies, Z_calc, diff2_h_seq_eq_Z_calc, Decidable.byContradiction, Not, HMul.hMul, inr_high_H_eval_bounds, Eq.symm, Eq.mp, congrArg, Eq.mpr, id, H_seq_eval_add, diff_H_seq_eval_add, Neg.neg, Eq.refl, inr_high_master_ineq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat and 74 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
```
lemma inr_high_reduction_goal_helper {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1 : diff2 (fun k => (h_seq m1 k : ℤ)) (d + 1) = 0)
    (h2 : diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = 1)
    (h2_high : d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + 2 ∧ d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2 ∧ d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 2 + 2 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2) :
  H_seq (m1:=m1) (m2:=m2) x (d + 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) (d + 1))^2 := by
…
```
Mentions: Monomial, totalDeg, diff2, h_seq, shifted_h_seq, reduced_monomial, H_seq, diff
lemma diff2_H_seq_eq_one_implies_inr_high Case B upper region transfers its later-degree bound back to d−1 line 1895 source
L4DEL explanation
Case B, upper region for g.
— Human-written Hilbert-functions proof companion
This is the upper-region analogue of the lower residual case: prove the later square bound, then apply the same exact curvature-one reduction.
1. Combine component curvatures zero and one into total curvature one.
2. Use inr_high_reduction_goal_helper at the later degree.
3. Shift the bound back with H_seq_diff2_reduction.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, h_seq, HAdd.hAdd, shifted_h_seq, reduced_monomial, And, GE.ge, HSub.hSub, H_seq, HPow.hPow and 1 more
Proof uses: H_seq_diff2_reduction, Eq.mpr, id, congrArg, diff2_H_seq_eq_add, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.add_pf_zero_add, inr_high_reduction_goal_helper
50 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_one_implies_inr_high {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1 : diff2 (fun k => (h_seq m1 k : ℤ)) (d + 1) = 0)
    (h2 : diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = 1)
    (h2_high : d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + 2 ∧ d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2 ∧ d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 2 + 2 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2) :
  H_seq (m1:=m1) (m2:=m2) x (d - 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) d)^2 := by
…
```
Mentions: Monomial, totalDeg, diff2, h_seq, shifted_h_seq, reduced_monomial, H_seq, diff
lemma diff2_H_seq_eq_one_implies_inr Case B is complete after classifying the translated residual sequence line 1905 source
L4DEL explanation
∆2 f (d + 1) = 0, ∆2 g(d + 1) = 1.
— Human-written Hilbert-functions proof companion
Residual curvature one first proves that the shift is active, then the unshifted reduced monomial lies in either its lower or upper critical region.
1. Transfer curvature one from the shifted sequence to h_seq at degree d+1-c.
2. Classify that translated degree into lower or upper region.
3. Dispatch to the corresponding residual-region theorem.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, h_seq, HAdd.hAdd, shifted_h_seq, reduced_monomial, H_seq, HSub.hSub, HPow.hPow, diff
Proof uses: GE.ge, diff2_shifted_h_seq_eq_one_implies, diff2_shifted_h_seq_eq_one_implies_eq, Or, And, diff2_h_seq_eq_one_implies, diff2_H_seq_eq_one_implies_inr_low, diff2_H_seq_eq_one_implies_inr_high
39 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_one_implies_inr {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1 : diff2 (fun k => (h_seq m1 k : ℤ)) (d + 1) = 0)
    (h2 : diff2 (shifted_h_seq (reduced_monomial m1 m2 x) (m1 x + 1)) (d + 1) = 1) :
  H_seq (m1:=m1) (m2:=m2) x (d - 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) d)^2 := by
…
```
Mentions: Monomial, totalDeg, diff2, h_seq, shifted_h_seq, reduced_monomial, H_seq, diff
lemma diff2_H_seq_eq_one_implies The full curvature-one implication is the union of cases A and B line 1917 source
L4DEL explanation
If ∆2 H(d + 1) = 1 and H(d + 1) ≤ (∆H(d + 1))2 , then
— Human-written Hilbert-functions proof companion
Whenever H has second difference one, exactly one component contributes curvature one; both component choices have now been proved in both critical regions.
1. Split total curvature one into the principal-one/residual-zero and principal-zero/residual-one alternatives.
2. Case A is handled by diff2_H_seq_eq_one_implies_inl.
3. Case B is handled by diff2_H_seq_eq_one_implies_inr.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, H_seq, HAdd.hAdd, HSub.hSub, HPow.hPow, diff
Proof uses: Or, And, h_seq, shifted_h_seq, reduced_monomial, diff2_H_seq_eq_one_implies_cases, diff2_H_seq_eq_one_implies_inl, diff2_H_seq_eq_one_implies_inr
36 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_one_implies {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2) :
  diff2 (H_seq (m1:=m1) (m2:=m2) x) (d + 1) = 1 →
…
```
Mentions: Monomial, totalDeg, diff2, H_seq
lemma m_deg_eq line 1927 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Eq, totalDeg, HAdd.hAdd, Fin
Proof uses: id, Eq.trans, Finset.sum, Finsupp.support, Finsupp, Finset.univ, Finset.sum_subset, Finset.subset_univ, of_eq_true, Membership.mem, Finset, Not, True, forall_congr, implies_congr_ctx, Ne, congrArg, eq_self, implies_true, Fin.sum_univ_three and 4 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma h1_high_h2_low_contradiction In the curvature-two case, principal-upper and residual-lower regions are incompatible line 1941 source
L4DEL explanation
whereas the upper-region inequalities for f give
— Human-written Hilbert-functions proof companion
Equal total degrees and the distinguished-coordinate shift make the residual lower inequalities contradict one of the principal upper inequalities.
1. Expand the reduced monomial coordinate by coordinate.
2. Use the coordinatewise comparison away from x and equality of total degrees.
3. Derive the strict pairwise-sum contradiction described in the manuscript.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, And, GE.ge, HAdd.hAdd, HSub.hSub, reduced_monomial, False
Proof uses: m_deg_eq, Or, LT.lt, Fin.isLt, Decidable.byContradiction, Not, Fin.ext, of_eq_true, ite, Eq.trans, True, congrArg, ite_congr, eq_self, eq_true, True.intro, Eq.refl, eq_false, not_false, ite_cond_eq_false and 8 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
```
lemma h1_high_h2_low_contradiction {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ)
  (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
  (h1_high : d + 1 ≥ m1 0 + m1 1 + 2 ∧ d + 1 ≥ m1 1 + m1 2 + 2 ∧ d + 1 ≥ m1 0 + m1 2 + 2 ∧ d + 1 ≤ m1 0 + m1 1 + m1 2 + 2)
  (h2_low : d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 1 ∧ d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 2) :
  False := by
…
```
Mentions: Monomial, totalDeg, reduced_monomial
lemma h1_low_h2_high_contradiction In the curvature-two case, a principal lower region is impossible after shift activation line 1979 source
L4DEL explanation
Therefore the lower region for f is impossible
— Human-written Hilbert-functions proof companion
Residual curvature one forces d+1≥c=m1(x)+1, while a principal lower region requires d+1≤m1(x).
1. Inspect the distinguished coordinate x.
2. Compare the activation threshold with the principal lower bound at that coordinate.
3. The two natural-number inequalities are contradictory.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, And, HAdd.hAdd, GE.ge, HSub.hSub, reduced_monomial, False
Proof uses: h1_low_h2_high_contradiction.match_1
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma h1_low_h2_high_contradiction {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ)
  (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
  (h1_low : d + 1 ≤ m1 0 ∧ d + 1 ≤ m1 1 ∧ d + 1 ≤ m1 2)
  (h2_high : d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + 2 ∧
    d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2 ∧
    d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 2 + 2 ∧
    d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2) :
  False := by match x with|0|2|1=>omega
```
Mentions: Monomial, totalDeg, reduced_monomial
lemma diff2_H_seq_eq_two_implies_inr_inr The curvature-two upper-upper case satisfies the doubled square bound line 1988 source
L4DEL explanation
Thus g is also in its upper region.
— Human-written Hilbert-functions proof companion
Once both components are in their upper regions, their exact complementary quadratics are bounded by the square of the sum of their negative first differences.
1. Evaluate both component values at d-1 by the upper formulas.
2. Evaluate both first differences at d with offsets U1 and U2.
3. Apply log_concave_algebra_upper_eval and reassemble H.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, And, GE.ge, HAdd.hAdd, HSub.hSub, reduced_monomial, Int, HMul.hMul, H_seq, HPow.hPow, diff
Proof uses: Decidable.byContradiction, Not, h_seq, h_seq_pure_upper, Neg.neg, h_seq_pure_upper_diff, shifted_h_seq, id, Eq.mpr, ite, congrArg, if_pos, Eq.refl, if_neg, H_seq_eval_add, diff_H_seq_eval_add, log_concave_algebra_upper_eval, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat and 63 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_two_implies_inr_inr {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2)
    (h1_high : d + 1 ≥ m1 0 + m1 1 + 2 ∧ d + 1 ≥ m1 1 + m1 2 + 2 ∧ d + 1 ≥ m1 0 + m1 2 + 2 ∧ d + 1 ≤ m1 0 + m1 1 + m1 2 + 2)
    (h2_high : d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + 2 ∧
      d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2 ∧
      d + 1 - (m1 x + 1) ≥ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 2 + 2 ∧
      d + 1 - (m1 x + 1) ≤ (reduced_monomial m1 m2 x) 0 + (reduced_monomial m1 m2 x) 1 + (reduced_monomial m1 m2 x) 2 + 2) :
    2 * H_seq (m1:=m1) (m2:=m2) x (d - 1) ≤ (diff (H_seq (m1:=m1) (m2:=m2) x) d)^2 := by
…
```
Mentions: Monomial, totalDeg, reduced_monomial, H_seq, diff
lemma h1_low_contradiction Shift activation alone rules out the principal lower region line 2051 source
L4DEL explanation
Therefore the lower region for f is impossible
— Human-written Hilbert-functions proof companion
If d+1 reaches the shift threshold m1(x)+1, it cannot simultaneously remain at most m1(x) as a lower-region hypothesis demands.
1. Split the finite coordinate x into 0, 1, or 2.
2. Rewrite the lower-region hypothesis at the selected coordinate.
3. Linear arithmetic yields the contradiction in each branch.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion
standard axioms: Quot.sound, propext what this means
Statement uses: Monomial, OfNat.ofNat, Nat, Fin, And, LE.le, HAdd.hAdd, GE.ge, False
Proof uses: Or, Eq, LT.lt, Fin.isLt, Decidable.byContradiction, Not, congrArg, Fin.ext, Eq.mp
29 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma h1_low_contradiction {m1 : Monomial 3} (x : Fin 3) (d : ℕ)
  (h1_low : d + 1 ≤ m1 0 ∧ d + 1 ≤ m1 1 ∧ d + 1 ≤ m1 2)
  (h_ge : d + 1 ≥ m1 x + 1) : False := by
…
```
Mentions: Monomial
lemma diff2_H_seq_eq_two_implies The full curvature-two implication leaves only the upper-upper case line 2074 source
L4DEL explanation
The case ∆2 H(d + 1) = 2. Then ∆2 f (d + 1) = ∆2 g(d + 1) = 1.
— Human-written Hilbert-functions proof companion
Total curvature two forces both summands to have curvature one; activation rules out a lower principal region, and the remaining mixed region is contradictory.
1. Prove that both component curvatures equal one and classify both monomial sequences.
2. Eliminate principal-lower and principal-upper/residual-lower combinations.
3. Apply the proved upper-upper inequality to the only surviving case.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, Int, diff2, H_seq, HAdd.hAdd, HMul.hMul, HSub.hSub, HPow.hPow, diff
Proof uses: And, h_seq, shifted_h_seq, reduced_monomial, diff2_H_seq_eq_two_implies_both_one, Or, GE.ge, diff2_h_seq_eq_one_implies, And.left, diff2_shifted_h_seq_eq_one_implies, And.right, diff2_shifted_h_seq_eq_one_implies_eq, False.elim, h1_low_contradiction, h1_high_h2_low_contradiction, diff2_H_seq_eq_two_implies_inr_inr
41 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma diff2_H_seq_eq_two_implies {m1 m2 : Monomial 3} (x : Fin 3) (d : ℕ) (hd : d > 0)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2) :
  diff2 (H_seq (m1:=m1) (m2:=m2) x) (d + 1) = 2 →
…
```
Mentions: Monomial, totalDeg, diff2, H_seq
lemma sum_log_concave_helper The principal-plus-shifted-residual sequence is log-concave line 2090 source
L4DEL explanation
Combining the cases proves (9) and (10), hence by (8) the sequence H is log-concave at degree d.
— Human-written Hilbert-functions proof companion
Under the exceptional-coordinate orientation and equal-degree hypotheses, the complete finite-difference case analysis proves log-concavity of the decomposed sequence through the common degree of m₁ and m₂.
1. The second-difference bound disposes of nonpositive curvature and reduces positive curvature to values 1 and 2.
2. Lower- and upper-region estimates for the principal and shifted sequences establish the two critical inequalities, which log_concave_core turns into the desired neighbour-product bound.
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: Monomial, OfNat.ofNat, Nat, Fin, GT.gt, Ne, LE.le, Eq, totalDeg, IsLogConcaveUpTo, HAdd.hAdd, h_seq, ite, GE.ge, reduced_monomial, HSub.hSub
Proof uses: Membership.mem, Finset, Finset.Ioo, And.left, LT.lt, Iff.mp, And, Finset.mem_Ioo, Int, H_seq, diff2, diff2_H_seq_le_two, HPow.hPow, diff, diff2_H_seq_eq_one_implies, HMul.hMul, diff2_H_seq_eq_two_implies, Nat.cast_nonneg, log_concave_core, diff_eq and 81 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma sum_log_concave_helper {m1 m2 : Monomial 3} (x : Fin 3)
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) (h_deg : totalDeg m1 = totalDeg m2) :
    IsLogConcaveUpTo (totalDeg m1) (fun d =>
      h_seq m1 d + if d ≥ m1 x + 1 then h_seq (reduced_monomial m1 m2 x) (d - (m1 x + 1)) else 0) := by
…
```
Mentions: Monomial, totalDeg, IsLogConcaveUpTo, h_seq, reduced_monomial
lemma pureOSeq_eq_sum Identify the original pure O-sequence with the decomposed sequence line 2120 source
L4DEL explanation
H(d) := hΓ (d) = hm1 (d) + 1d≥c hMred (d − c).
— Human-written Hilbert-functions proof companion
If the two named monomials are exactly the maximal elements and satisfy the chosen coordinate orientation, the pure O-sequence of the order ideal equals the principal-plus-shifted-residual formula at every degree.
1. ideal_carrier_eq_union replaces the carrier with the union of the two divisor sets.
2. pureOSeq_decomposition then supplies the degreewise equality, and function extensionality upgrades it to equality of the whole sequences.
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: PureOrderIdeal, OfNat.ofNat, Nat, Monomial, Fin, Eq, Finset, maximalMonomials, PureOrderIdeal.ideal, Insert.insert, Singleton.singleton, GT.gt, Ne, LE.le, pureOSequence, HAdd.hAdd, h_seq, ite, GE.ge, reduced_monomial and 1 more
Proof uses: funext, id, Finset.card, Finset.filter, totalDeg, OrderIdeal.carrier, Union.union, divisorsFinset, ideal_carrier_eq_union, Eq.mpr, congrArg, pureOSeq_decomposition
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma pureOSeq_eq_sum {P : PureOrderIdeal 3} {m1 m2 : Monomial 3} (x : Fin 3)
    (h_max_eq : maximalMonomials P.ideal = {m1, m2})
    (h_gt : m2 x > m1 x) (h_le : ∀ y, y ≠ x → m2 y ≤ m1 y) :
    pureOSequence P.ideal = fun d =>
      h_seq m1 d + if d ≥ m1 x + 1 then h_seq (reduced_monomial m1 m2 x) (d - (m1 x + 1)) else 0 := by
…
```
Mentions: PureOrderIdeal, Monomial, maximalMonomials, pureOSequence, h_seq, reduced_monomial
theorem P5 Pure O-sequences of codimension 3 and type 2 are log-concave line 2132 source
L4DEL explanation
Every pure O-sequence of codimension 3 and type 2 is log-concave.
— 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)
A pure order ideal in three variables with exactly two maximal monomials has a degree-counting sequence h satisfying h(i-1)·h(i+1) ≤ h(i)² at every internal degree. This closes the codimension-3, type-2 pure O-sequence case identified as open in the cited literature.
1. Purity and type two express the order ideal as the union of the divisor sets of two distinct maximal monomials of equal total degree.
2. After choosing a coordinate on which the two generators differ, the proof decomposes the degree counts into one principal divisor sequence plus a shifted reduced sequence.
3. Explicit first- and second-difference formulas reduce log-concavity to inequalities for those two sequences, handled across their lower and upper degree regions.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written Hilbert-functions proof companion, Richard P. Stanley, Hilbert functions of graded algebras (1978), Boij, Migliore, Miró-Roig, Nagel, and Zanello, On the Shape of a Pure O-Sequence, Fabrizio Zanello, Log-concavity of level Hilbert functions and pure O-sequences
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ProblemP5
Proof uses: PureOrderIdeal, OfNat.ofNat, Nat, Eq, typePO, Exists, Monomial, And, Ne, Finset, maximalMonomials, PureOrderIdeal.ideal, Insert.insert, Fin, Singleton.singleton, type_two_implies_two_maximals, IsLogConcaveUpTo, socleDegree, pureOSequence, totalDeg and 27 more
21 instances, coercions and auxiliary constants left out.

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

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
theorem P5 : ProblemP5 := by
…
```
Mentions: ProblemP5