Local-to-cumulative mass over residue classes

The correction in Section 4 distinguishes the local summands f_x from the cumulative function f_{≤ x}. This file proves the first, purely finite-sum part of equation local-to-cumulative: a cumulative fibre mass is exactly the sum of the contributions of the local summands below the node.

The statement deliberately keeps every local contribution in the coordinate fibre of the upper representation map. Passing from this quotient-level identity to the paper's sum over local flag points additionally uses uniqueness of centered representatives for odd p.

noncomputable def EGZ.FlagDecompositionRaw.localFibreMassBelow {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (c : FpCoord p (F.rank x)) : ℕ

Sum of the local masses below x, grouped using the fibre of the upper representation map.

Equations

• EGZ.FlagDecompositionRaw.localFibreMassBelow R pieces x c = ∑ y : F.Node, if y ≤ x then EGZ.FlagDecompositionRaw.affineFibreMass (pieces y) (⇑(R.map x)) c else 0

noncomputable def EGZ.FlagDecompositionRaw.localToCumulativeMass {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) : ℕ

Quotient-level local-to-cumulative expression for a lattice coordinate.

Equations

• EGZ.FlagDecompositionRaw.localToCumulativeMass R pieces x q = if EGZ.IsCenteredLift p q then EGZ.FlagDecompositionRaw.localFibreMassBelow R pieces x (EGZ.IntCoord.mod p q) else 0

noncomputable def EGZ.FlagDecompositionRaw.localTransitionMassBelow {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (c : FpCoord p (F.rank x)) : ℕ

The same local mass sum, now partitioned by residue classes in the source lattice fibre and transported along the flag map.

Equations

• One or more equations did not get rendered due to their size.

theorem EGZ.FlagDecompositionRaw.affineFibreMass_cumulativeWeight {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (c : FpCoord p (F.rank x)) : affineFibreMass (cumulativeWeight pieces x) (⇑(R.map x)) c = localFibreMassBelow R pieces x c

The fibre mass of a cumulative weight is the sum of the corresponding fibre masses of the local pieces below the node.

This is the finite-sum core of equation local-to-cumulative; importantly, the right-hand side uses pieces y, not the cumulative weight at y.

theorem EGZ.FlagDecompositionRaw.affineFibreMass_eq_sum_transitionFibres {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) {y x : F.Node} (h : y ≤ x) (hsupported : ∀ (v : FpCoord p d), pieces y v ≠ 0 → v ∈ R.space y) (c : FpCoord p (F.rank x)) : affineFibreMass (pieces y) (⇑(R.map x)) c = ∑ a : FpCoord p (F.rank y), if ((F.transition h).modp p) a = c then affineFibreMass (pieces y) (⇑(R.map y)) a else 0

On a local summand supported in space y, an upper fibre is the disjoint union of the lower fibres whose residue classes map to it. This is where compatibility of the finite-field representation enters the local-to-cumulative calculation.

theorem EGZ.FlagDecompositionRaw.localFibreMassBelow_eq_localTransitionMassBelow {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (hsupported : ∀ (y : F.Node) (v : FpCoord p d), pieces y v ≠ 0 → v ∈ R.space y) (x : F.Node) (c : FpCoord p (F.rank x)) : localFibreMassBelow R pieces x c = localTransitionMassBelow R pieces x c

Fully quotient-level local-to-cumulative identity. It partitions each local summand by its own lattice residue and then applies the transition map to the upper residue.

theorem EGZ.FlagDecompositionRaw.hat_eq_sum_localFibreMass {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) : hat R pieces x q = localToCumulativeMass R pieces x q

The cumulative centered lift is obtained from the same local fibre-mass sum whenever the displayed lattice coordinate is centered.

theorem EGZ.FlagDecompositionRaw.hat_eq_localTransitionMassBelow_of_centered {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (hsupported : ∀ (y : F.Node) (v : FpCoord p d), pieces y v ≠ 0 → v ∈ R.space y) (x : F.Node) (q : IntCoord (F.rank x)) (hq : IsCenteredLift p q) : hat R pieces x q = localTransitionMassBelow R pieces x (IntCoord.mod p q)

For a centered upper coordinate, cumulative lifted mass is the sum of the local quotient masses below it, partitioned through the transition maps. This is the strongest form of the local-to-cumulative identity that does not yet choose centered representatives in every lower lattice fibre.