Finite factorization through shared summaries

This is the finite-sum identity underlying Lemma 3.2 (pp. 22–23) of [OAI26c], The Exponential Time Hypothesis is False, manuscript revised October 25, 2026, source openai/math@7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a.

A factor may depend on all coordinates, provided that inside a fixed measurement fiber it depends only on its own coordinate. We enumerate a supplied finite measurement box, including unrealizable tuples. Representatives come from unrestricted fibers, not from the local restrictions. Empty restricted fibers contribute zero; unrealizable tuples also contribute zero.

These are mathematical finite sums. A representative-selection function is explicit data, not an efficient oracle or a machine certificate. The kernel-shift lemma supplies the rational locality implication. Integer box bounds and scan/runtime analysis remain separate obligations.

Main definitions

• Cslib.SharedSummaries.fiberContribution: a product of restricted local sums, or zero for an unrealizable measurement tuple.

Main results

• Cslib.SharedSummaries.fiberContribution_eq: the contribution is independent of valid unrestricted representatives.
• Cslib.SharedSummaries.sum_prod_eq_sum_measurement_fibers: factorization over the full supplied finite measurement box.
• Cslib.SharedSummaries.fiber_locality_of_kernel_shifts: the paper’s rational-kernel invariance implies fiber locality.

noncomputable def Cslib.SharedSummaries.fiberContribution {G : Type u_1} [Fintype G] [DecidableEq G] {X : G → Type u_2} {Y : G → Type u_3} [(g : G) → Fintype (X g)] [(g : G) → DecidableEq (Y g)] {A : Type u_4} [CommRing A] (measure : (g : G) → X g → Y g) (allowed : (g : G) → Finset (X g)) (factor : G → ((g : G) → X g) → A) (representative : (y : (g : G) → Y g) → (∀ (g : G), ∃ (u : X g), measure g u = y g) → (g : G) → X g) (y : (g : G) → Y g) : A

The contribution at y, using representatives of its unrestricted measurement fibers. The selector need not respect allowed. No selector is invoked for an unrealizable tuple.

theorem Cslib.SharedSummaries.fiberContribution_eq {G : Type u_1} [Fintype G] [DecidableEq G] {X : G → Type u_2} {Y : G → Type u_3} [(g : G) → Fintype (X g)] [(g : G) → DecidableEq (Y g)] {A : Type u_4} [CommRing A] (measure : (g : G) → X g → Y g) (allowed : (g : G) → Finset (X g)) (factor : G → ((g : G) → X g) → A) (locality : ∀ (g : G) (x x' : (g : G) → X g), (∀ (h : G), measure h (x h) = measure h (x' h)) → x g = x' g → factor g x = factor g x') (representative representative' : (y : (g : G) → Y g) → (∀ (g : G), ∃ (u : X g), measure g u = y g) → (g : G) → X g) (valid : ∀ (y : (g : G) → Y g) (hy : ∀ (g : G), ∃ (u : X g), measure g u = y g) (g : G), measure g (representative y hy g) = y g) (valid' : ∀ (y : (g : G) → Y g) (hy : ∀ (g : G), ∃ (u : X g), measure g u = y g) (g : G), measure g (representative' y hy g) = y g) (y : (g : G) → Y g) : fiberContribution measure allowed factor representative y = fiberContribution measure allowed factor representative' y

On a fixed fiber, changing the unrestricted representatives does not change the contribution. Only the full measurement tuple and the local coordinate may affect a factor.

theorem Cslib.SharedSummaries.sum_prod_eq_sum_measurement_fibers {G : Type u_1} [Fintype G] [DecidableEq G] {X : G → Type u_2} {Y : G → Type u_3} [(g : G) → Fintype (X g)] [(g : G) → DecidableEq (Y g)] {A : Type u_4} [CommRing A] (measure : (g : G) → X g → Y g) (box : (g : G) → Finset (Y g)) (covers : ∀ (g : G) (u : X g), measure g u ∈ box g) (allowed : (g : G) → Finset (X g)) (factor : G → ((g : G) → X g) → A) (locality : ∀ (g : G) (x x' : (g : G) → X g), (∀ (h : G), measure h (x h) = measure h (x' h)) → x g = x' g → factor g x = factor g x') (representative : (y : (g : G) → Y g) → (∀ (g : G), ∃ (u : X g), measure g u = y g) → (g : G) → X g) (valid : ∀ (y : (g : G) → Y g) (hy : ∀ (g : G), ∃ (u : X g), measure g u = y g) (g : G), measure g (representative y hy g) = y g) : ∑ x ∈ Fintype.piFinset allowed, ∏ g : G, factor g x = ∑ y ∈ Fintype.piFinset box, fiberContribution measure allowed factor representative y

Finite shared-summary factorization. Every measurement tuple in the supplied box is examined, including tuples with an empty unrestricted fiber. Local restrictions are imposed only inside the sums; representatives need not satisfy them.

theorem Cslib.SharedSummaries.fiber_locality_of_kernel_shifts {G : Type u_1} [DecidableEq G] {A : Type u_4} [Finite G] {V : G → Type u_5} {W : G → Type u_6} [(g : G) → AddCommGroup (V g)] [(g : G) → Module ℚ (V g)] [(g : G) → AddCommGroup (W g)] [(g : G) → Module ℚ (W g)] (measure : (g : G) → V g →ₗ[ℚ] W g) (factor : G → ((g : G) → V g) → A) (shift : ∀ (g h : G), h ≠ g → ∀ (x : (g : G) → V g) (delta : V h), (measure h) delta = 0 → factor g (x + Pi.single h delta) = factor g x) (g : G) (x x' : (h : G) → V h) (sameMeasurements : ∀ (h : G), (measure h) (x h) = (measure h) (x' h)) (sameCoordinate : x g = x' g) : factor g x = factor g x'

Kernel-shift invariance implies fiber locality. Each change in another group is extended by zero to the full tuple. This is the rational linear-summary hypothesis of Lemma 3.2; no rank, representative-selection or runtime assumption is needed.