Exact signature fibres of the selected R-324 cells

The finite physical cell index is regrouped by the data that remain constant when the marked primitive word is sent to Proposition 5.7:

• its finite occupied support;
• its literal multiset of labels (equivalently, every raw count); and
• the two selected endpoint labels.

The decomposition in this file is an exact equality. The overlapping Hepp-tree cover is applied separately as the first nonnegative enlargement.

A decidable raw word signature

def Anderson4D.rawWordBag {q : ℕ} (w : Fin q → Z4) : Multiset Z4

The multiset of values of a finite word.

Equations

• Anderson4D.rawWordBag w = Multiset.map w Finset.univ.val

structure Anderson4D.OpenEdgeCellWordSignature (q : ℕ) : Type

Support, raw occurrence profile, and the two open-edge endpoint labels. The support is retained explicitly because it indexes the occupied-label realization.

• support : Finset Z4
• rawBag : Multiset Z4
• leftLabel : Z4
• rightLabel : Z4

def Anderson4D.instDecidableEqOpenEdgeCellWordSignature.decEq {q✝ : ℕ} (x✝ x✝¹ : OpenEdgeCellWordSignature q✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Anderson4D.instDecidableEqOpenEdgeCellWordSignature {q✝ : ℕ} : DecidableEq (OpenEdgeCellWordSignature q✝)

Equations

• Anderson4D.instDecidableEqOpenEdgeCellWordSignature = Anderson4D.instDecidableEqOpenEdgeCellWordSignature.decEq

def Anderson4D.openEdgeCellWordSignature {q : ℕ} (a b : Fin q) (w : Fin q → Z4) : OpenEdgeCellWordSignature q

Signature carried by one open-edge lattice word.

Equations

• Anderson4D.openEdgeCellWordSignature a b w = { support := Anderson4D.tupleSupport w, rawBag := Anderson4D.rawWordBag w, leftLabel := w a, rightLabel := w b }

theorem Anderson4D.rawWordBag_count {q : ℕ} (w : Fin q → Z4) (x : Z4) : Multiset.count x (rawWordBag w) = wordFiberCount w x

Raw occurrence count is the multiplicity in rawWordBag.

theorem Anderson4D.tupleSupport_eq_of_openEdgeCellWordSignature_eq {q : ℕ} (a b : Fin q) {reference w : Fin q → Z4} (h : openEdgeCellWordSignature a b w = openEdgeCellWordSignature a b reference) : tupleSupport w = tupleSupport reference

Equality of signatures gives equality of occupied supports.

theorem Anderson4D.wordFiberCount_eq_of_openEdgeCellWordSignature_eq {q : ℕ} (a b : Fin q) {reference w : Fin q → Z4} (h : openEdgeCellWordSignature a b w = openEdgeCellWordSignature a b reference) (x : Z4) : wordFiberCount w x = wordFiberCount reference x

Equality of signatures gives equality of every literal raw count.

theorem Anderson4D.leftLabel_eq_of_openEdgeCellWordSignature_eq {q : ℕ} (a b : Fin q) {reference w : Fin q → Z4} (h : openEdgeCellWordSignature a b w = openEdgeCellWordSignature a b reference) : w a = reference a

Equality of signatures fixes the selected lower endpoint label.

theorem Anderson4D.rightLabel_eq_of_openEdgeCellWordSignature_eq {q : ℕ} (a b : Fin q) {reference w : Fin q → Z4} (h : openEdgeCellWordSignature a b w = openEdgeCellWordSignature a b reference) : w b = reference b

Equality of signatures fixes the selected upper endpoint label.

Generic exact finite regrouping

theorem Anderson4D.sum_eq_sum_openEdgeCellWordSignature_fibers {ι : Type u_1} {R : Type u_2} [AddCommMonoid R] {q : ℕ} (s : Finset ι) (word : ι → Fin q → Z4) (a b : Fin q) (F : ι → R) : ∑ i ∈ s, F i = ∑ sig ∈ Finset.image (fun (i : ι) => openEdgeCellWordSignature a b (word i)) s, ∑ i ∈ s with openEdgeCellWordSignature a b (word i) = sig, F i

Any finite sum splits exactly into the fibres of an open-word signature.

The genuine selected physical cell carrier

noncomputable def Anderson4D.r324SelectedMarkedCellWord {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) : Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected)) → Z4

Restrict one ambient cell index to the canonical marked block.

Equations

• Anderson4D.r324SelectedMarkedCellWord κp κm π selected y = Anderson4D.r324MarkedResidualBlockWord κp κm π selected y

noncomputable def Anderson4D.r324SelectedMarkedCellSignature {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) : OpenEdgeCellWordSignature (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected))

Signature of the marked-block word carried by one genuine ambient cell index.

Equations

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

noncomputable def Anderson4D.r324SelectedPhysicalCellSignatures {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) : Finset (OpenEdgeCellWordSignature (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected)))

The finite set of signatures that actually occur in the selected physical cell partition.

Equations

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

noncomputable def Anderson4D.r324SelectedPhysicalCellSignatureFiber {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (sig : OpenEdgeCellWordSignature (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected))) : Finset (Fin (2 * m) → Z4)

Actual ambient physical cell indices in one marked-word signature fibre.

Equations

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

theorem Anderson4D.sum_selectedPhysicalCells_eq_signatureFibers {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {R : Type u_1} [AddCommMonoid R] (F : (Fin (2 * m) → Z4) → R) : ∑ y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices, F y = ∑ sig ∈ r324SelectedPhysicalCellSignatures κp κm π selected ε hε, ∑ y ∈ r324SelectedPhysicalCellSignatureFiber κp κm π selected ε hε sig, F y

Exact decomposition of the genuine selected physical cell-index sum by support/raw-profile/endpoint signatures.

theorem Anderson4D.respectsExcept_of_mem_r324SelectedPhysicalOpenEdgeCells {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) : RespectsPairingExcept (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324ResidualMarkedUpperEndpoint π selected) y

Every actual selected physical cell index satisfies the ambient one-open-edge constraint.

theorem Anderson4D.selectedMarkedCellWord_respectsExcept_of_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (sig : OpenEdgeCellWordSignature (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected))) {y : Fin (2 * m) → Z4} (hy : y ∈ r324SelectedPhysicalCellSignatureFiber κp κm π selected ε hε sig) : RespectsPairingExcept (residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) ⋯) (r324MarkedResidualLowerPosition κp κm π selected) (r324MarkedResidualUpperPosition κp κm π selected) (r324SelectedMarkedCellWord κp κm π selected y)

Consequently, every word in an actual signature fibre obeys the local unmarked pairing constraint on the unique marked block.