Exact primitive-pairing sums on one R-324 block

This file specializes PartialPairing.closedOnEquiv to an increasingly enumerated even block. Pairings whose restriction to the block is primitive are exactly:

• one member of the paper's primitiveFullPairings q, and
• an arbitrary pairing on the complementary carrier.

Thus a sum over ambient pairings can be reindexed as the primitive pairing sum first, with no multiplicity and no termwise cardinality loss.

def Anderson4D.orderedClosedBlockPairing {n k : ℕ} (B : Finset (Fin n)) (e : Fin k ≃o ↥B) (κ : PartialPairing.ClosedOn B) : PartialPairing (Fin k)

Increasingly reindex the restriction of a pairing carrying only a closure certificate on B.

Equations

• Anderson4D.orderedClosedBlockPairing B e κ = (Anderson4D.PartialPairing.congr e.symm.toEquiv) ((↑κ).restrictTo ⋯)

def Anderson4D.closedOnOrderedEquiv {n k : ℕ} (B : Finset (Fin n)) (e : Fin k ≃o ↥B) : PartialPairing.ClosedOn B ≃ PartialPairing (Fin k) × PartialPairing { i : Fin n // i ∉ B }

Exact decomposition with the block restriction already transported to its standard increasing Fin k carrier.

Equations

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

@[simp]

theorem Anderson4D.closedOnOrderedEquiv_apply_fst {n k : ℕ} (B : Finset (Fin n)) (e : Fin k ≃o ↥B) (κ : PartialPairing.ClosedOn B) : ((closedOnOrderedEquiv B e) κ).1 = orderedClosedBlockPairing B e κ

@[simp]

theorem Anderson4D.closedOnOrderedEquiv_apply_snd {n k : ℕ} (B : Finset (Fin n)) (e : Fin k ≃o ↥B) (κ : PartialPairing.ClosedOn B) : ((closedOnOrderedEquiv B e) κ).2 = (↑κ).restrictCompl ⋯

def Anderson4D.subtypeProdFstEquiv {α : Type u_1} {β : Type u_2} (p : α → Prop) : { x : α × β // p x.1 } ≃ { a : α // p a } × β

Pulling a predicate on the first component out of a product subtype.

Equations

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

def Anderson4D.subtypeProdSndEquiv {α : Type u_1} {β : Type u_2} (p : β → Prop) : { x : α × β // p x.2 } ≃ α × { b : β // p b }

Pulling a predicate on the second component out of a product subtype.

Equations

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

@[reducible, inline]

abbrev Anderson4D.PrimitiveClosedOn {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) : Type

Ambient pairings preserving B and primitive on the increasingly reindexed block.

Equations

• Anderson4D.PrimitiveClosedOn q B e = { κ : Anderson4D.PartialPairing.ClosedOn B // Anderson4D.orderedClosedBlockPairing B e κ ∈ Anderson4D.primitiveFullPairings q }

def Anderson4D.primitiveClosedOnEquiv {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) : PrimitiveClosedOn q B e ≃ ↥(primitiveFullPairings q) × PartialPairing { i : Fin n // i ∉ B }

A primitive closed ambient pairing is exactly a primitive standard block pairing together with an arbitrary complementary pairing.

Equations

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

@[simp]

theorem Anderson4D.primitiveClosedOnEquiv_apply_snd {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) (κ : PrimitiveClosedOn q B e) : ((primitiveClosedOnEquiv q B e) κ).2 = (↑↑κ).restrictCompl ⋯

theorem Anderson4D.PrimitiveClosedOn.isFullyPairedOn {n q : ℕ} {B : Finset (Fin n)} {e : Fin (2 * q) ≃o ↥B} (κ : PrimitiveClosedOn q B e) : IsFullyPairedOn (↑↑κ) B

Membership in PrimitiveClosedOn supplies the concrete IsFullyPairedOn certificate on the ambient sparse block.

theorem Anderson4D.PrimitiveClosedOn.isRelPrimitiveOn {n q : ℕ} {B : Finset (Fin n)} {e : Fin (2 * q) ≃o ↥B} (κ : PrimitiveClosedOn q B e) : IsRelPrimitiveOn (↑↑κ) B

Standard primitivity of the increasingly transported block pairing pulls back to relative primitivity on the ambient sparse block.

def Anderson4D.primitiveClosedOnOfFullyPairedPrimitive {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (hprim : IsRelPrimitiveOn κ B) : PrimitiveClosedOn (residualBlockOrder B) B (residualPrimitiveBlockOrderIso κ B hB)

The canonical closed primitive-block element cut out of an ambient pairing. Its first component is definitionally the standard residual primitive pairing used by the R-324 block decomposition.

Equations

• Anderson4D.primitiveClosedOnOfFullyPairedPrimitive κ B hB hprim = ⟨⟨κ, ⋯⟩, ⋯⟩

@[simp]

theorem Anderson4D.primitiveClosedOnOfFullyPairedPrimitive_val {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (hprim : IsRelPrimitiveOn κ B) : ↑↑(primitiveClosedOnOfFullyPairedPrimitive κ B hB hprim) = κ

@[simp]

theorem Anderson4D.primitiveClosedOnEquiv_canonical_fst {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (hprim : IsRelPrimitiveOn κ B) : ↑((primitiveClosedOnEquiv (residualBlockOrder B) B (residualPrimitiveBlockOrderIso κ B hB)) (primitiveClosedOnOfFullyPairedPrimitive κ B hB hprim)).1 = residualPrimitiveBlockPairing κ B hB

theorem Anderson4D.PrimitiveClosedOn.isFull_iff_complement {n q : ℕ} {B : Finset (Fin n)} {e : Fin (2 * q) ≃o ↥B} (κ : PrimitiveClosedOn q B e) : (↑↑κ).IsFull ↔ ((primitiveClosedOnEquiv q B e) κ).2.IsFull

For a primitive closed block, fullness of the ambient pairing is equivalent to fullness of the complementary restriction. Fullness on the block itself is already supplied by primitive-pairing membership.

def Anderson4D.fullPrimitiveClosedOnEquiv {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) : { κ : PrimitiveClosedOn q B e // (↑↑κ).IsFull } ≃ ↥(primitiveFullPairings q) × { κ : PartialPairing { i : Fin n // i ∉ B } // κ.IsFull }

Full ambient pairings primitive on B are exactly a primitive pairing on the standard block together with a full pairing on the complement.

Equations

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

theorem Anderson4D.sum_fullPrimitiveClosedOn_eq_sum_block_complement {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) {M : Type u_1} [AddCommMonoid M] (F : { κ : PrimitiveClosedOn q B e // (↑↑κ).IsFull } → M) : ∑ κ : { κ : PrimitiveClosedOn q B e // (↑↑κ).IsFull }, F κ = ∑ κB : ↥(primitiveFullPairings q), ∑ κC : { κ : PartialPairing { i : Fin n // i ∉ B } // κ.IsFull }, F ((fullPrimitiveClosedOnEquiv q B e).symm (κB, κC))

Exact finite-sum reindexing for full pairings primitive on one block. This is the form used by successive R-324 block replacement: after summing the whole primitive block fiber, the remaining index is again a full pairing on the complementary carrier.

def Anderson4D.primitiveClosedOnFiberEquiv {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) (κB₀ : ↥(primitiveFullPairings q)) (P : PrimitiveClosedOn q B e → Prop) (hinvariant : ∀ (κB κB' : ↥(primitiveFullPairings q)) (κC : PartialPairing { i : Fin n // i ∉ B }), P ((primitiveClosedOnEquiv q B e).symm (κB, κC)) ↔ P ((primitiveClosedOnEquiv q B e).symm (κB', κC))) : { κ : PrimitiveClosedOn q B e // P κ } ≃ ↥(primitiveFullPairings q) × { κC : PartialPairing { i : Fin n // i ∉ B } // P ((primitiveClosedOnEquiv q B e).symm (κB₀, κC)) }

If a predicate on primitive closed pairings depends only on the complementary coordinate, its fiber is exactly the full primitive block coordinate times one complementary fiber. This packages the recursive fixed-signature factorization used by R-324.

Equations

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

theorem Anderson4D.sum_primitiveClosedOnFiber_eq_sum_block_complement {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) (κB₀ : ↥(primitiveFullPairings q)) (P : PrimitiveClosedOn q B e → Prop) [DecidablePred P] (hinvariant : ∀ (κB κB' : ↥(primitiveFullPairings q)) (κC : PartialPairing { i : Fin n // i ∉ B }), P ((primitiveClosedOnEquiv q B e).symm (κB, κC)) ↔ P ((primitiveClosedOnEquiv q B e).symm (κB', κC))) {M : Type u_1} [AddCommMonoid M] (F : { κ : PrimitiveClosedOn q B e // P κ } → M) : ∑ κ : { κ : PrimitiveClosedOn q B e // P κ }, F κ = ∑ κB : ↥(primitiveFullPairings q), ∑ κC : { κC : PartialPairing { i : Fin n // i ∉ B } // P ((primitiveClosedOnEquiv q B e).symm (κB₀, κC)) }, F ((primitiveClosedOnFiberEquiv q B e κB₀ P hinvariant).symm (κB, κC))

Exact finite-sum factorization attached to primitiveClosedOnFiberEquiv.

Canonical elements supplied by the three R-324 block families

def Anderson4D.momentLeftExtractionFullPrimitiveClosedOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentLeftExtractionBlocks κp) : { κ : PrimitiveClosedOn (residualBlockOrder B) B (residualPrimitiveBlockOrderIso (momentCombinedPairing κp κm π) B ⋯) // (↑↑κ).IsFull }

A within-left extraction block, viewed in the full primitive-closed pairing type on the doubled carrier.

Equations

• Anderson4D.momentLeftExtractionFullPrimitiveClosedOn κp κm π B hB = ⟨Anderson4D.primitiveClosedOnOfFullyPairedPrimitive (Anderson4D.momentCombinedPairing κp κm π) B ⋯ ⋯, ⋯⟩

def Anderson4D.momentRightExtractionFullPrimitiveClosedOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentRightExtractionBlocks κm) : { κ : PrimitiveClosedOn (residualBlockOrder B) B (residualPrimitiveBlockOrderIso (momentCombinedPairing κp κm π) B ⋯) // (↑↑κ).IsFull }

A within-right extraction block, viewed in the full primitive-closed pairing type on the doubled carrier.

Equations

• Anderson4D.momentRightExtractionFullPrimitiveClosedOn κp κm π B hB = ⟨Anderson4D.primitiveClosedOnOfFullyPairedPrimitive (Anderson4D.momentCombinedPairing κp κm π) B ⋯ ⋯, ⋯⟩

def Anderson4D.momentResidualCollapseFullPrimitiveClosedOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentResidualCollapseBlocks κp κm π) : { κ : PrimitiveClosedOn (residualBlockOrder B) B (residualPrimitiveBlockOrderIso (momentCombinedPairing κp κm π) B ⋯) // (↑↑κ).IsFull }

A residual collapse block, viewed in the full primitive-closed pairing type on the doubled carrier.

Equations

• Anderson4D.momentResidualCollapseFullPrimitiveClosedOn κp κm π B hB = ⟨Anderson4D.primitiveClosedOnOfFullyPairedPrimitive (Anderson4D.momentCombinedPairing κp κm π) B ⋯ ⋯, ⋯⟩

@[simp]

theorem Anderson4D.momentLeftExtractionFullPrimitiveClosedOn_val {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentLeftExtractionBlocks κp) : ↑↑↑(momentLeftExtractionFullPrimitiveClosedOn κp κm π B hB) = momentCombinedPairing κp κm π

@[simp]

theorem Anderson4D.momentRightExtractionFullPrimitiveClosedOn_val {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentRightExtractionBlocks κm) : ↑↑↑(momentRightExtractionFullPrimitiveClosedOn κp κm π B hB) = momentCombinedPairing κp κm π

@[simp]

theorem Anderson4D.momentResidualCollapseFullPrimitiveClosedOn_val {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentResidualCollapseBlocks κp κm π) : ↑↑↑(momentResidualCollapseFullPrimitiveClosedOn κp κm π B hB) = momentCombinedPairing κp κm π

theorem Anderson4D.pairingCovarianceProductOn_eq_orderedClosedBlock {n q : ℕ} {B : Finset (Fin n)} {e : Fin (2 * q) ≃o ↥B} (ρ : SmoothCutoff) (ε : ℝ) (κ : PrimitiveClosedOn q B e) (v : Fin n → T4) : pairingCovarianceProductOn ρ ε (↑↑κ) B v = primitiveCovarianceProduct ρ ε q (orderedClosedBlockPairing B e ↑κ) fun (i : Fin (2 * q)) => v ↑(e i)

The ambient covariance factor on a primitive closed block is exactly the standard primitive covariance product of the first component exposed by primitiveClosedOnEquiv.

theorem Anderson4D.sum_primitiveClosedOn_eq_sum_block_complement {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) {M : Type u_1} [AddCommMonoid M] (F : PrimitiveClosedOn q B e → M) : ∑ κ : PrimitiveClosedOn q B e, F κ = ∑ κB : ↥(primitiveFullPairings q), ∑ κC : PartialPairing { i : Fin n // i ∉ B }, F ((primitiveClosedOnEquiv q B e).symm (κB, κC))

Exact finite-sum reindexing which exposes the complete primitive pairing sum on the block before the complement sum.

theorem Anderson4D.sum_primitiveClosedOn_mul_factors {n : ℕ} (q : ℕ) (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) {R : Type u_1} [CommSemiring R] (fB : ↥(primitiveFullPairings q) → R) (fC : PartialPairing { i : Fin n // i ∉ B } → R) : ∑ κ : PrimitiveClosedOn q B e, fB ((primitiveClosedOnEquiv q B e) κ).1 * fC ((primitiveClosedOnEquiv q B e) κ).2 = (∑ κB : ↥(primitiveFullPairings q), fB κB) * ∑ κC : PartialPairing { i : Fin n // i ∉ B }, fC κC

If the summand separates into a block factor and a complement factor, the complete primitive block sum factors exactly as a product of sums.