TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Summable formal families may be regrouped and rearranged, distribute over multiplication, and have well-defined locally finite products

Statement

Let $(f_{i})_{i \in I}$ be a summable family in $R ⟦ x ⟧$ .

A bijection of its index set does not change its sum. A partition $I = ⨆_{j \in J} I_{j}$ gives summable subfamilies, a summable family $(\sum_{i \in I_{j}} f_{i})_{j \in J}$ , and $\sum_{i \in I} f_{i} = \sum_{j \in J} \sum_{i \in I_{j}} f_{i} .$
For every $h \in R ⟦ x ⟧$ , the family $(h f_{i})_{i \in I}$ is summable and $h \sum_{i \in I} f_{i} = \sum_{i \in I} h f_{i} .$
If ${ord}_{x} (u_{k}) \to + \infty$ , the partial products $\prod_{k < M} (1 + u_{k})$ stabilize modulo each $x^{N}$ . The resulting infinite product is unchanged by a permutation of the factors or by finite regrouping.

The assertions include the empty sum and empty product.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

A family is summable exactly when, below every degree cutoff $N$ , only finitely many members have a nonzero coefficient (Summable families of formal series are locally finite in every coefficient range).

[F2]

When ${ord}_{x} (u_{k}) \to + \infty$ , the product $\prod_{k \geq 0} (1 + u_{k})$ is defined by stabilization of finite partial products modulo every $x^{N}$ (Summable families of formal series are locally finite in every coefficient range).

[F3]

Two formal series are equal if and only if all their coefficients are equal (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[F4]

A finite sum over $S \times T$ equals either iterated finite sum, and finite sums are invariant under bijective reindexing (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

Proof

technique · reduce every coefficient range to a finite calculation

1.1

Fix $N$ . Only finitely many members of the family survive modulo $x^{N}$ , so bijective reindexing and regrouping are finite operations there. Finite reindexing gives the same coefficients below $N$ ; coefficient extensionality, as $N$ is arbitrary, proves clause 1.

givenF1F3F4

1.2

The coefficient of $h f_{i}$ below $N$ uses only coefficients of $f_{i}$ below $N$ , so only finitely many indices contribute. Finite distributivity gives the displayed identity coefficient by coefficient.

givenF1F4

1.3

For fixed $N$ , eventually every $u_{k}$ has order at least $N$ , so $1 + u_{k} \equiv 1 (m o d x^{N})$ . All later factors therefore leave the partial product unchanged modulo $x^{N}$ . A permutation or finite grouping merely reorders the finitely many factors that matter, and multiplication is commutative and associative.

givenF2

2.1

At an empty index set, the same arguments read $0 = 0$ and $1 = 1$ . Steps 1.1-1.3 prove all clauses.

step 1.1step 1.2step 1.3∎

Depends on

Used by

Cited to discharge well-definedness by Summable families of formal series are locally finite in every coefficient range.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 47 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Benjamin Sambale, An Invitation to Formal Power Series (standard reference, not scraped)