Selected R-324 fibre to the one-open-edge consumer

This file joins four already exact boundaries without enlarging the canonical selector fibre:

• its selected Fourier pair is the genuine marked residual cross edge;
• the selected fixed-mode product factors at precisely that edge;
• the spare ε⁴ from the selected cutoff mode pays the two appended lattice-chain edges; and
• the augmented word is primitive and is therefore a genuine input to Proposition 5.7.

No unrestricted projected-covariance fibre and no diagnostic pairing-dependent marker sum is introduced.

The canonical selector is the genuine marked residual edge

theorem Anderson4D.SmoothCutoff.r324SelectedHighPairModeFactor_selected_eq_marked (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ρ.r324SelectedHighPairModeFactor ε L κp κm π q selected v (r324CrossSlotPairIndex κp κm π selected) = ρ.r324HighCovarianceModeTerm ε L (v (r324ResidualMarkedLowerEndpoint selected) - v (r324ResidualMarkedUpperEndpoint π selected)) (q (r324CrossSlotPairIndex κp κm π selected))

The selected pair-mode factor in the exact selector fibre is the high-mode term on the endpoints of the unique marked residual edge.

noncomputable def Anderson4D.SmoothCutoff.r324SelectedHighUnselectedPairModeProduct (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ℂ

Product of every fixed Fourier pair mode except the canonical selected cross slot. This retains the restricted configuration coordinate verbatim.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedHighCovarianceConfigurationTerm_eq_marked_mul_unselected (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ρ.r324SelectedHighCovarianceConfigurationTerm ε L κp κm π q selected v = ρ.r324HighCovarianceModeTerm ε L (v (r324ResidualMarkedLowerEndpoint selected) - v (r324ResidualMarkedUpperEndpoint π selected)) (q (r324CrossSlotPairIndex κp κm π selected)) * ρ.r324SelectedHighUnselectedPairModeProduct ε L κp κm π q selected v

Exact factorization of the restricted fixed-mode covariance product at its canonical selected slot.

Paying the two appended chain edges

theorem Anderson4D.SmoothCutoff.eps_four_mul_boxPenalty_sq_le {ε : ℝ} {M : ℕ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hM : ↑M ≤ ε⁻¹) : ε ^ 4 * (1 + (2 * ↑M) ^ 2) ^ 2 ≤ 25

If the cell box has the natural ultraviolet size M ≤ ε⁻¹, the spare ε⁴ pays both inverse lattice-edge factors with a uniform constant.

theorem Anderson4D.SmoothCutoff.exists_boxPenalty_sq_mul_covarianceModeCoeff_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε L : ℝ} {M : ℕ} {k : Z4}, 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → 1 ≤ ε ^ 2 * L → k ∈ r324HighModeSet ε L → ↑M ≤ ε⁻¹ → (1 + (2 * ↑M) ^ 2) ^ 2 * ‖ρ.covarianceModeCoeff ε k‖ ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L)

Covariance-coefficient form of the complete scalar ledger: the canonical high mode times both box penalties is uniformly bounded by the paper's eighth-order routed decay.

Primitive-word consumer

theorem Anderson4D.SmoothCutoff.exists_selectedOpenEdgePrimitiveConsumer (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {t : PlaneTree} {m M : ℕ} {κ : PartialPairing (Fin m)} {a b : Fin m} {w : Fin m → HeppLeaf t} {Nm : t.HeppMarking} {z : HeppLeaf t → Fin 4 → ℤ} {ε L : ℝ} {k : Z4}, 0 < m → κ a = b → a < b → κ.IsFull → IsPrimitive κ → (∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) → IsAdmissible Nm M z → 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → 1 ≤ ε ^ 2 * L → k ∈ r324HighModeSet ε L → ↑M ≤ ε⁻¹ → NoProperLeafBlock (openEdgeAugmentedWord w a b) ∧ ‖ρ.covarianceModeCoeff ε k‖ * heppChainWeight z w ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L) * heppChainWeight z (openEdgeAugmentedWord w a b)

The concrete one-open-edge consumer used before Proposition 5.7. It simultaneously certifies that the dummy-closed word is primitive and that the selected high-frequency coefficient, including both appended chain-edge costs, leaves exactly the routed eighth-order decay.

The pairing and marker are fixed inputs here; there is no pairing-dependent arbitrary marker family.