Exact signed factorization on a canonical selector fibre

The canonical first-large-slot selector depends on every Fourier mode in a configuration. Consequently its fibre must not be replaced by an unrestricted projected-covariance series. This module keeps the existing selector subtype literally in every declaration and performs only the termwise signed factorization at the selected mode.

The resulting restricted tsum is exact. Passing from it to the complete physical complement is a later inequality, proved block by block; no such enlargement is encoded here.

noncomputable def Anderson4D.SmoothCutoff.r324SelectorRestrictedSignedInteriorMode (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : R324ResidualCovarianceSlot κp) (ω : ρ.R324SelectedCrossSlotConfigurationFiber ε α β κp κm π hexternal hε hε1 hmtrunc i) (v : Fin (2 * m) → T4) : ℂ

One signed interior mode on the genuine canonical-selector subtype. The selected high mode is exposed, while the product of all other fixed modes remains intact and inside the same signed term.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedEndpointCore_eq_selectorRestrictedSignedInteriorMode (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : R324ResidualCovarianceSlot κp) (ω : ρ.R324SelectedCrossSlotConfigurationFiber ε α β κp κm π hexternal hε hε1 hmtrunc i) (v : Fin (2 * m) → T4) : have selected := ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ↑ω; ρ.r324SelectedEndpointCore ε κp κm π (↑↑ω) selected ‖z4EuclideanFrequency (α + β)‖ v = ρ.r324SelectorRestrictedSignedInteriorMode ε α β κp κm π hexternal hε hε1 hmtrunc i ω v

Every member of the restricted selector fibre is exactly its signed selected-mode factorization. The subtype proof is neither discarded nor weakened.

theorem Anderson4D.SmoothCutoff.tsum_r324SelectedEndpointCore_eq_selectorRestrictedSigned (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : (∑' (ω : ρ.R324SelectedCrossSlotConfigurationFiber ε α β κp κm π hexternal hε hε1 hmtrunc i), have selected := ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ↑ω; ρ.r324SelectedEndpointCore ε κp κm π (↑↑ω) selected ‖z4EuclideanFrequency (α + β)‖ v) = ∑' (ω : ρ.R324SelectedCrossSlotConfigurationFiber ε α β κp κm π hexternal hε hε1 hmtrunc i), ρ.r324SelectorRestrictedSignedInteriorMode ε α β κp κm π hexternal hε hε1 hmtrunc i ω v

Subtype-retaining exact series bridge. The restricted signed selector series is unchanged by exposing its selected high mode termwise. No summability hypothesis is needed for this termwise tsum identity.