Pushforward Composition
Abstract
Indicator-weighted fiber sums compose over any additive commutative monoid.
The module Entropy/Forgetting/CapacityMonotone defines pushforward f p as fun y => sum x, if f x = y then p x else 0, for [Fintype X], and it is imported here. Only the source type is finite; the target carries no finiteness.
sum_indicator_comp is the indicator-weighted form of Mathlib’s Finset.sum_fiberwise_eq_sum_filter, obtained from it by taking the target index set to be the fiber of g over target. The mathematical content is Mathlib’s. What this module supplies is the bridge between that filter form and the indicator-weighted idiom used throughout this development, and the named consequence for pushforward.
For a finite source type Omega, a real nonnegative normalized mass q and an actual window map a:Omega->Window, p=pushforward(a,q) is the five-mode atom law. CompletionEntropyMinimality.pushforward_is_law proves its normalization. For each source outcome the initialized high-to-low reader performs the literal word [a(outcome)]; all five first letters are legal. This literal one-window history retains its atom and carries the derived actual reader state. Its atom projection pushes q to p, while native_execution identifies the carried state with the natural singleton history.
Composition with the low-bit, high-bit or middle indicator yields the source event masses X=p(low)+p(ends), Y=p(high)+p(ends) and Z=p(middle). The same pushforward_comp identity applies to the parity of the first actual reply and to the pair consisting of that parity and the next total Option reply. For the fixed same-state high suffix, summing this joint table on the odd-reply event and dividing by its positive mass gives the continuation distribution. The intermediate alphabet is finite, while the integer Option output may be infinite; the theorem requires only the finite intermediate alphabet and finite original source.
The source map, mass and reply are parts of one declared realization. A marginal atom law cannot reconstruct distinctions lost by its pushforward, and it supplies no multiwindow joint law. A normalized empirical mass from a nonempty finite archive is a law of that archive; neither normalization nor compositional pushforward certifies the unknown physical law or independent sampling. The fiberwise identities are applications of the existing summation theorem, with no acquisition or copying claim.
Prior art in pinned Mathlib: Finset.sum_fiberwise_eq_sum_filter, in Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean, states the fiberwise decomposition over an arbitrary commutative monoid. It is generated by to_additive from prod_fiberwise_eq_prod_filter, so no declaration line carries the additive name: a name search restricted to declaration keywords misses it, while a plain name search finds it at its use sites. sum_indicator_comp applies that lemma rather than reproving it.
Theorem 1.1 (Indicator-weighted finite sums compose).
Proof. Machine-checked in Lean as D5/S3/Entropy/Forgetting/PushforwardComposition.sum_indicator_comp (✓ std3). ∎
Source. Repository-derived.
Commentary.
The types X, Y, Z, and M are arbitrary. Only X and Y are finite, and M is an additive commutative monoid. For arbitrary p, f, g, and target, the outer indicator and the inner fiber indicator collapse to the indicator for the composite fiber. There are no further hypotheses.
Theorem 1.2 (Pushforwards compose).
Proof. Machine-checked in Lean as D5/S3/Entropy/Forgetting/PushforwardComposition.pushforward_comp (✓ std3). ∎
Source. Repository-derived.
Commentary.
For finite X and Y, a real-valued function p can be pushed first through f and then through g, or directly through their composite. There are no hypotheses on p, and Z has no Fintype instance.