Exact local-to-cumulative identity

Centered representatives turn the quotient-level fibre partition into the integer-transition identity in Section 4. Only local lifted weights occur on the right-hand side. Boundedness at the upper node prevents a transition of a nonzero local lift from wrapping around modulo p.

noncomputable def EGZ.FlagDecompositionRaw.localIntegerMassBelow {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)) : ℕ

Local lifted masses below a node, transported by the integer transition maps and summed over the finite centered boxes.

Equations

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

theorem EGZ.FlagDecompositionRaw.sum_transitionFibres_eq_sum_localLift {p d : ℕ} [NeZero p] {F : ConvexFlag} (hp : Odd p) (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) {y x : F.Node} (h : y ≤ x) (c : FpCoord p (F.rank x)) : (∑ a : FpCoord p (F.rank y), if ((F.transition h).modp p) a = c then affineFibreMass (pieces y) (⇑(R.map y)) a else 0) = ∑ z ∈ latticeBox (F.rank y) ((p - 1) / 2), if IntCoord.mod p ((F.transition h).integer z) = c then localLift R pieces y z else 0

A residue fibre can be summed over centered integer representatives in the source.

theorem EGZ.FlagDecompositionRaw.transition_mod_eq_iff_of_localLift_ne_zero {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) {y x : F.Node} (h : y ≤ x) (z : IntCoord (F.rank y)) (q : IntCoord (F.rank x)) (hq : IsCenteredLift p q) (hcentered : localLift R pieces y z ≠ 0 → IsCenteredLift p ((F.transition h).integer z)) (hz : localLift R pieces y z ≠ 0) : IntCoord.mod p ((F.transition h).integer z) = IntCoord.mod p q ↔ (F.transition h).integer z = q

If a transition stays in the centered box on the local support, congruence to a centered upper point is equality of integer coordinates.

theorem EGZ.FlagDecompositionRaw.localTransitionMassBelow_eq_localIntegerMassBelow {p d : ℕ} [NeZero p] {F : ConvexFlag} (hp : Odd p) (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) (hq : IsCenteredLift p q) (hcentered : ∀ (y : F.Node) (h : y ≤ x) (z : IntCoord (F.rank y)), localLift R pieces y z ≠ 0 → IsCenteredLift p ((F.transition h).integer z)) : localTransitionMassBelow R pieces x (IntCoord.mod p q) = localIntegerMassBelow R pieces x q

The quotient-level partition is the exact integer-transition partition when nonzero local lifts remain centered after transition.

theorem EGZ.FlagDecompositionRaw.hat_eq_localIntegerMassBelow_of_centered {p d : ℕ} [NeZero p] {F : ConvexFlag} (hp : Odd p) (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) (hcentered : ∀ (y : F.Node) (h : y ≤ x) (z : IntCoord (F.rank y)), localLift R pieces y z ≠ 0 → IsCenteredLift p ((F.transition h).integer z)) : hat R pieces x q = localIntegerMassBelow R pieces x q

Exact local-to-cumulative identity using local lifted weights.

theorem EGZ.FlagDecompositionRaw.localIntegerMassBelow_eq_zero_of_not_centered {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)) (hq : ¬IsCenteredLift p q) (hcentered : ∀ (y : F.Node) (h : y ≤ x) (z : IntCoord (F.rank y)), localLift R pieces y z ≠ 0 → IsCenteredLift p ((F.transition h).integer z)) : localIntegerMassBelow R pieces x q = 0

The local integer-transition sum has no mass outside the centered upper box if all transitions of its nonzero local terms stay centered.

theorem EGZ.FlagDecompositionRaw.hat_eq_localIntegerMassBelow {p d : ℕ} [NeZero p] {F : ConvexFlag} (hp : Odd p) (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)) (hcentered : ∀ (y : F.Node) (h : y ≤ x) (z : IntCoord (F.rank y)), localLift R pieces y z ≠ 0 → IsCenteredLift p ((F.transition h).integer z)) : hat R pieces x q = localIntegerMassBelow R pieces x q

The exact local-to-cumulative identity holds for every integer upper coordinate; outside the centered box both sides vanish.

theorem EGZ.FlagDecomposition.isCenteredLift_transition_of_localLift_ne_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (K : Φ.flag.Node → ℕ) (hbounded : Φ.IsKBounded K) {y x : Φ.flag.Node} (h : y ≤ x) (hK : 2 * K x < p) (z : IntCoord (Φ.flag.rank y)) (hz : Φ.localLift y z ≠ 0) : IsCenteredLift p ((Φ.flag.transition h).integer z)

At an upper node of radius less than p / 2, every nonzero local lift below it has centered integer transition coordinates.

theorem EGZ.FlagDecomposition.hat_eq_sum_localLift_of_centered {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (hp : Odd p) (Φ : FlagDecomposition p d f) (K : Φ.flag.Node → ℕ) (hbounded : Φ.IsKBounded K) (x : Φ.flag.Node) (hK : 2 * K x < p) (q : IntCoord (Φ.flag.rank x)) (hq : IsCenteredLift p q) : Φ.hat x q = ∑ y : Φ.flag.Node, if h : y ≤ x then ∑ z ∈ latticeBox (Φ.flag.rank y) ((p - 1) / 2), if (Φ.flag.transition h).integer z = q then Φ.localLift y z else 0 else 0

Section 4's corrected identity: the cumulative lift at q is the sum of local lifts at all lower nodes whose integer transitions equal q.

theorem EGZ.FlagDecomposition.hat_eq_sum_localLift {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (hp : Odd p) (Φ : FlagDecomposition p d f) (K : Φ.flag.Node → ℕ) (hbounded : Φ.IsKBounded K) (x : Φ.flag.Node) (hK : 2 * K x < p) (q : IntCoord (Φ.flag.rank x)) : Φ.hat x q = ∑ y : Φ.flag.Node, if h : y ≤ x then ∑ z ∈ latticeBox (Φ.flag.rank y) ((p - 1) / 2), if (Φ.flag.transition h).integer z = q then Φ.localLift y z else 0 else 0

The corrected local-to-cumulative identity for arbitrary integer coordinates, with the large-prime condition expressed by 2 * K x < p.