Finite cell decomposition with one open pairing edge

For the selected R-324 covariance edge the two endpoint cells must remain independent. Every other covariance edge retains the copied-cell assignment used in the proof of Proposition 4.1. This file constructs that mixed assignment as an honest finite measurable partition and specializes it to the genuine marked residual cross edge.

def Anderson4D.RespectsPairingExcept {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (y : Fin m → Z4) : Prop

A lattice word respects every pairing edge except the two endpoints of one selected edge.

Equations

• Anderson4D.RespectsPairingExcept κ a b y = ∀ (i : Fin m), i ≠ a → i ≠ b → y (κ i) = y i

@[implicit_reducible]

instance Anderson4D.instDecidableRespectsPairingExcept {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (y : Fin m → Z4) : Decidable (RespectsPairingExcept κ a b y)

Equations

• Anderson4D.instDecidableRespectsPairingExcept κ a b y = Anderson4D.instDecidableRespectsPairingExcept._aux_1 κ a b y

noncomputable def Anderson4D.openEdgeCellAssignment {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (ε : ℝ) (x : Fin m → T4) : Fin m → Z4

Use the actual floor cells at the selected endpoints and the usual copied anchor cell everywhere else.

Equations

• Anderson4D.openEdgeCellAssignment κ a b ε x i = if i = a then Anderson4D.torusFloorCell ε (x i) else if i = b then Anderson4D.torusFloorCell ε (x i) else Anderson4D.pairedCellAssignment κ ε x i

@[simp]

theorem Anderson4D.openEdgeCellAssignment_left {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (ε : ℝ) (x : Fin m → T4) : openEdgeCellAssignment κ a b ε x a = torusFloorCell ε (x a)

@[simp]

theorem Anderson4D.openEdgeCellAssignment_right {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (ε : ℝ) (x : Fin m → T4) : openEdgeCellAssignment κ a b ε x b = torusFloorCell ε (x b)

theorem Anderson4D.pairing_ne_selected_of_ne_endpoints {m : ℕ} (κ : PartialPairing (Fin m)) (a b i : Fin m) (hκab : κ a = b) (hia : i ≠ a) (hib : i ≠ b) : κ i ≠ a ∧ κ i ≠ b

No unselected endpoint can be paired into the selected edge.

theorem Anderson4D.openEdgeCellAssignment_respectsExcept {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (ε : ℝ) (x : Fin m → T4) : RespectsPairingExcept κ a b (openEdgeCellAssignment κ a b ε x)

Every unselected edge still receives one copied label.

theorem Anderson4D.measurable_openEdgeCellAssignment {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (ε : ℝ) : Measurable (openEdgeCellAssignment κ a b ε)

The mixed assignment is measurable.

theorem Anderson4D.openEdgeCellAssignment_mem_piFinset {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) {ε : ℝ} (hε : 0 < ε) (x : Fin m → T4) : openEdgeCellAssignment κ a b ε x ∈ Fintype.piFinset fun (x : Fin m) => torusGrid ε

Every mixed assignment lies in the finite torus grid.

noncomputable def Anderson4D.openEdgeTorusGridCells {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (ε : ℝ) (hε : 0 < ε) : FiniteMeasurableCells (Fin m → T4) (Fin m → Z4)

The actual finite measurable partition for one open edge. Its index set already enforces the unmarked copied-label predicate, so no later enlargement is needed.

Equations

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

theorem Anderson4D.integral_eq_sum_openEdgeTorusGridCells {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (ε : ℝ) (hε : 0 < ε) (f : (Fin m → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)) : (∫ (x : Fin m → T4), f x ∂MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure) = ∑ y ∈ (openEdgeTorusGridCells κ a b hκab ε hε).indices, ∫ (x : Fin m → T4) in (openEdgeTorusGridCells κ a b hκab ε hε).index ⁻¹' {y}, f x ∂MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure

Exact finite cell decomposition for every integrable real majorant on the physical coordinates of one open pairing edge.

Specialization to the genuine selected residual edge

noncomputable def Anderson4D.r324MarkedResidualOpenEdgeCells {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) : FiniteMeasurableCells (Fin (2 * m) → T4) (Fin (2 * m) → Z4)

The marked residual cross edge supplies the exact open-edge cell partition needed by the selected configuration fibre.

Equations

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

theorem Anderson4D.r324MarkedResidualOpenEdgeCells_index_respects {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (x : Fin (2 * m) → T4) : RespectsPairingExcept (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324ResidualMarkedUpperEndpoint π selected) ((r324MarkedResidualOpenEdgeCells κp κm π selected ε hε).index x)

Every cell word occurring in the genuine selected residual partition respects every unmarked covariance edge.