Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-30
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Hall inner product on symmetric functions

Definition

The Hall inner product is the graded Z-bilinear form on the stable ring Λ (The stable graded ring of symmetric functions) characterized by ⟨hλ,mμ⟩H=δλμ for all partitions λ,μ (Partitions, English diagrams, and conjugation, Elementary and complete families freely generate the stable ring, The monomial symmetric functions form the integral stable basis), where δλμ=1 if λ=μ and 0 otherwise. In particular, homogeneous components of unequal degrees are orthogonal. For the empty partition, h∅=m∅=1, so ⟨1,1⟩H=1.

For each d≥0, the proven integral bases give unique finite expansions fd=∑λ⊢daλhλ,gd=∑μ⊢dbμmμ for fd,gd∈Λd. Define their degree-d pairing by ⟨fd,gd⟩H:=∑λ,μ⊢daλbμδλμ. For f=∑dfd and g=∑dgd in the algebraic direct sum Λ, set ⟨f,g⟩H:=∑d⟨fd,gd⟩H. Only finitely many d contribute because f and g have finite degree support. The unique expansions in the two integral bases make this a well-defined Z-bilinear form; the displayed basis rule determines it uniquely on all of Λ.

Depends on

Used by

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources