Exact physical representation boundary for the raw R-324 case density

The routed raw density is formed from norms of complete common-increment groups. The canonical high-mode selector, by contrast, is available only for Fourier configurations whose full endpoint integral is nonzero. This file records the exact overlap between those two representations and keeps the complementary endpoint-null series explicit.

No unrestricted projected covariance, primitive majorant, or total routed budget is introduced here. In particular, the endpoint-null remainder is not silently discarded when a norm has already been taken.

Concrete data carried by one raw refined index

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawMomentContraction {m : ℕ} (p : R324RefinedScheduleIndex m) (a : ℕ) : MomentContraction m

The actual contraction selected by one raw refined natural index.

Equations

• Anderson4D.SmoothCutoff.r324RefinedRawMomentContraction p a = ↑((Anderson4D.SmoothCutoff.r324NatEquivRefinedContractionConfigurations p) a).1

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawConfigurationNumber {m : ℕ} (p : R324RefinedScheduleIndex m) (a : ℕ) : ℕ

The natural covariance-configuration number carried by one raw refined index.

Equations

• Anderson4D.SmoothCutoff.r324RefinedRawConfigurationNumber p a = ((Anderson4D.SmoothCutoff.r324NatEquivRefinedContractionConfigurations p) a).2

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawFullPairing {m : ℕ} (p : R324RefinedScheduleIndex m) (a : ℕ) : R324FullPairingIndex m

The full doubled pairing attached to one raw refined index.

Equations

• Anderson4D.SmoothCutoff.r324RefinedRawFullPairing p a = (Anderson4D.momentContractionEquivFullPairing m) (Anderson4D.SmoothCutoff.r324RefinedRawMomentContraction p a)

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawCombinedConfiguration {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (a : ℕ) : R324CombinedFourierConfiguration (r324RefinedRawMomentContraction p a).fst (r324RefinedRawMomentContraction p a).snd.fst (r324RefinedRawMomentContraction p a).snd.snd

The actual dependent Fourier assignment attached to one raw refined index.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawFullPairingIntegral (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) : ℂ

The endpoint-integrated Fourier coefficient of one raw refined configuration.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawNonzeroCombinedConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) : ρ.R324NonzeroCombinedFourierConfiguration ε α β (r324RefinedRawMomentContraction p a).fst (r324RefinedRawMomentContraction p a).snd.fst (r324RefinedRawMomentContraction p a).snd.snd

Package an endpoint-nonzero raw member in the exact subtype used by the canonical high-mode selector.

Equations

• ρ.r324RefinedRawNonzeroCombinedConfiguration hm ε α β p a hne = ⟨Anderson4D.SmoothCutoff.r324RefinedRawCombinedConfiguration hm p a, hne⟩

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawSelectedResidualSlot (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) : R324ResidualCovarianceSlot (r324RefinedRawMomentContraction p a).fst

The canonical selected residual slot of an endpoint-nonzero raw member.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawSelectedConfigurationFiber (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) : ρ.R324SelectedCrossSlotConfigurationFiber ε α β (r324RefinedRawMomentContraction p a).fst (r324RefinedRawMomentContraction p a).snd.fst (r324RefinedRawMomentContraction p a).snd.snd hexternal hε hε1 hmtrunc (ρ.r324RefinedRawSelectedResidualSlot hm ε α β hexternal hε hε1 hmtrunc p a hne)

The same raw member, now carrying the proof that it belongs to the genuine fibre of its canonical selector.

Equations

• ρ.r324RefinedRawSelectedConfigurationFiber hm ε α β hexternal hε hε1 hmtrunc p a hne = ⟨ρ.r324RefinedRawNonzeroCombinedConfiguration hm ε α β p a hne, ⋯⟩

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawSelectorRestrictedSignedCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) (v : Fin (2 * m) → T4) : ℂ

The genuine selector-restricted signed physical core carried by one endpoint-nonzero raw member.

Equations

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

Exact local selector representation

theorem Anderson4D.SmoothCutoff.r324RefinedRawEndpointIntegrand_eq_selectedHigh (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) (x y z w : T4) (v : Fin (2 * m) → T4) : ρ.r324RefinedRawEndpointIntegrand hm ε α β p a x y z w v = ρ.r324SelectedHighFullPairingFourierIntegrand ε α β (r324RefinedRawMomentContraction p a).fst (r324RefinedRawMomentContraction p a).snd.fst (r324RefinedRawMomentContraction p a).snd.snd hexternal hε hε1 hmtrunc (ρ.r324RefinedRawNonzeroCombinedConfiguration hm ε α β p a hne) x y z w v

Every endpoint-nonzero raw refined Fourier integrand is literally its canonically selected high-mode physical integrand. This is the first point at which the existing selector bridge applies.

theorem Anderson4D.SmoothCutoff.r324RefinedRawEndpointIntegrand_eq_selectorRestrictedSigned (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) (x y z w : T4) (v : Fin (2 * m) → T4) : ρ.r324RefinedRawEndpointIntegrand hm ε α β p a x y z w v = r324EndpointSeparatedIntegrand α β (r324ContractionEndpointAnchors hm (r324RefinedRawMomentContraction p a) v) (r324ContractionEndpointFlags (r324RefinedRawMomentContraction p a)) (ρ.r324RefinedRawSelectorRestrictedSignedCore hm ε α β hexternal hε hε1 hmtrunc p a hne v) x y z w

Endpoint-separated form of the preceding equality. The supplied core is the actual restricted signed physical mode, not an unrestricted single-projected covariance product.

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawSelectorRestrictedPhysicalIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

Named physical integrand supplied by the exact local selector representation.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedRawEndpointIntegrand_eq_selectorPhysical (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) (x y z w : T4) (v : Fin (2 * m) → T4) : ρ.r324RefinedRawEndpointIntegrand hm ε α β p a x y z w v = ρ.r324RefinedRawSelectorRestrictedPhysicalIntegrand hm ε α β hexternal hε hε1 hmtrunc p a hne x y z w v

theorem Anderson4D.SmoothCutoff.integrable_r324Flatten_refinedRawSelectorRestrictedPhysicalIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) : MeasureTheory.Integrable (r324Flatten (ρ.r324RefinedRawSelectorRestrictedPhysicalIntegrand hm ε α β hexternal hε hε1 hmtrunc p a hne)) (r324PhysicalMeasure m)

theorem Anderson4D.SmoothCutoff.integral_r324Flatten_refinedRawSelectorRestrictedPhysical_eq_five (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) : ∫ (q : R324PhysicalPoint m), r324Flatten (ρ.r324RefinedRawSelectorRestrictedPhysicalIntegrand hm ε α β hexternal hε hε1 hmtrunc p a hne) q ∂r324PhysicalMeasure m = ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), ρ.r324RefinedRawSelectorRestrictedPhysicalIntegrand hm ε α β hexternal hε hε1 hmtrunc p a hne x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure

Genuine five-group Fubini identity for the local selector-restricted physical integrand.

theorem Anderson4D.SmoothCutoff.integral_r324Flatten_refinedRawEndpointIntegrand_eq_rawFullPairingIntegral (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) : ∫ (q : R324PhysicalPoint m), r324Flatten (ρ.r324RefinedRawEndpointIntegrand hm ε α β p a) q ∂r324PhysicalMeasure m = ρ.r324RefinedRawFullPairingIntegral hm ε α β p a

The physical integral of a raw refined member is exactly the coefficient used to decide selector eligibility.

theorem Anderson4D.SmoothCutoff.integral_r324Flatten_refinedRawSelectorPhysical_eq_rawFullPairingIntegral (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0) : ∫ (q : R324PhysicalPoint m), r324Flatten (ρ.r324RefinedRawSelectorRestrictedPhysicalIntegrand hm ε α β hexternal hε hε1 hmtrunc p a hne) q ∂r324PhysicalMeasure m = ρ.r324RefinedRawFullPairingIntegral hm ε α β p a

The selector-restricted physical representative has exactly the same full physical integral as its original raw member.

The separate unrestricted marked-physical expansion

theorem Anderson4D.SmoothCutoff.r324SingleProjectedResidualPhysicalInteriorCore_eq_tsum_markedModes (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ρ.r324SingleProjectedResidualPhysicalInteriorCore ε L κp κm π selected v = ∑' (k : Z4), ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k

Once an unrestricted single-projected residual core has genuinely been constructed, the existing physical representation chain is exact: it is the tsum of modes of the one marked residual covariance.

This theorem intentionally has no selector-fibre argument. It must not be used to identify a restricted selector series with the unrestricted single-projected product.

Exact selector-eligible / endpoint-null split of one key group

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324RefinedRawIncrementKeyFiber {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (b : ℕ) : Type

Raw natural configurations sharing one complete increment key.

Equations

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

def Anderson4D.SmoothCutoff.r324RefinedRawEndpointNonzeroKeySet (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) : Set (R324RefinedRawIncrementKeyFiber hm p b)

Members of one key fibre on which the canonical physical selector is actually defined.

Equations

• ρ.r324RefinedRawEndpointNonzeroKeySet hm ε α β p b = {a : Anderson4D.SmoothCutoff.R324RefinedRawIncrementKeyFiber hm p b | ρ.r324RefinedRawFullPairingIntegral hm ε α β p ↑a ≠ 0}

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawSelectorEligibleKeyCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (v : Fin (2 * m) → T4) : ℂ

Signed internal key core consisting only of endpoint-nonzero raw members.

Equations

• ρ.r324RefinedRawSelectorEligibleKeyCore hm ε α β p b v = ∑' (a : ↑(ρ.r324RefinedRawEndpointNonzeroKeySet hm ε α β p b)), ρ.r324RefinedRawEndpointCore hm ε p (↑↑a) v

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawEndpointNullKeyCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (v : Fin (2 * m) → T4) : ℂ

The complementary signed internal key core. Its full endpoint integral vanishes termwise, but its pointwise internal values need not vanish and therefore cannot be deleted after taking a norm.

Equations

• ρ.r324RefinedRawEndpointNullKeyCore hm ε α β p b v = ∑' (a : ↑(ρ.r324RefinedRawEndpointNonzeroKeySet hm ε α β p b)ᶜ), ρ.r324RefinedRawEndpointCore hm ε p (↑↑a) v

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawSelectorEligibleKeyPhysicalIntegral (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (b : ℕ) : ℂ

Sum of the genuine restricted physical integrals in the selector-eligible part of one increment-key fibre.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedRawSelectorEligibleKeyPhysicalIntegral_eq_tsum_raw (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (b : ℕ) : ρ.r324RefinedRawSelectorEligibleKeyPhysicalIntegral hm ε α β hexternal hε hε1 hmtrunc p b = ∑' (a : ↑(ρ.r324RefinedRawEndpointNonzeroKeySet hm ε α β p b)), ρ.r324RefinedRawFullPairingIntegral hm ε α β p ↑↑a

Exact key-fibre regrouping of the genuine selector-restricted physical integrals.

theorem Anderson4D.SmoothCutoff.integral_r324Flatten_refinedRawEndpointIntegrand_eq_zero_of_null (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (a : ↑(ρ.r324RefinedRawEndpointNonzeroKeySet hm ε α β p b)ᶜ) : ∫ (q : R324PhysicalPoint m), r324Flatten (ρ.r324RefinedRawEndpointIntegrand hm ε α β p ↑↑a) q ∂r324PhysicalMeasure m = 0

Endpoint-null members vanish only after the complete physical integration.

theorem Anderson4D.SmoothCutoff.summable_r324RefinedRawEndpointCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : Summable fun (x : ℕ) => ρ.r324RefinedRawEndpointCore hm ε p x v

theorem Anderson4D.SmoothCutoff.r324KeyGroupedRefinedEndpointCore_eq_selectorEligible_add_null (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (v : Fin (2 * m) → T4) : ρ.r324KeyGroupedRefinedEndpointCore hm ε p b v = ρ.r324RefinedRawSelectorEligibleKeyCore hm ε α β p b v + ρ.r324RefinedRawEndpointNullKeyCore hm ε α β p b v

A full common-increment core is exactly the sum of its selector-eligible and endpoint-null parts. No triangle inequality is used and the null part remains signed.

theorem Anderson4D.SmoothCutoff.r324RawCaseDensityTerm_eq_selectorEligible_add_null (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (i : Fin m) (cases : R324EndpointReductionPattern) (p : R324RefinedScheduleIndex m × ℕ) (v : Fin (2 * m) → T4) : ρ.r324RawCaseDensityTerm lam hm ε i cases p v = if r324RefinedEndpointReductionCase p.1 = cases then |lamEps lam ε| ^ (2 * m) * ‖ρ.r324RefinedRawSelectorEligibleKeyCore hm ε α β p.1 p.2 v + ρ.r324RefinedRawEndpointNullKeyCore hm ε α β p.1 p.2 v‖ * r324GroupedIncrementCost hm p.2 i else 0

Exact raw-density term after exposing the first missing physical representation boundary. The endpoint-null remainder is deliberately inside the same norm as the selector-eligible core.

theorem Anderson4D.SmoothCutoff.r324RawCaseDensity_eq_tsum_selectorEligible_add_null (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (i : Fin m) (cases : R324EndpointReductionPattern) (v : Fin (2 * m) → T4) : ρ.r324RawCaseDensity lam hm ε i cases v = ∑' (p : R324RefinedScheduleIndex m × ℕ), if r324RefinedEndpointReductionCase p.1 = cases then |lamEps lam ε| ^ (2 * m) * ‖ρ.r324RefinedRawSelectorEligibleKeyCore hm ε α β p.1 p.2 v + ρ.r324RefinedRawEndpointNullKeyCore hm ε α β p.1 p.2 v‖ * r324GroupedIncrementCost hm p.2 i else 0

Patternwise raw density with the exact selector/null split exposed under the original countable sum.

theorem Anderson4D.SmoothCutoff.integral_r324RawCaseDensity_eq_integral_tsum_selector_add_null (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (i : Fin m) (cases : R324EndpointReductionPattern) : (∫ (v : Fin (2 * m) → T4), ρ.r324RawCaseDensity lam hm ε i cases v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = ∫ (v : Fin (2 * m) → T4), ∑' (p : R324RefinedScheduleIndex m × ℕ), if r324RefinedEndpointReductionCase p.1 = cases then |lamEps lam ε| ^ (2 * m) * ‖ρ.r324RefinedRawSelectorEligibleKeyCore hm ε α β p.1 p.2 v + ρ.r324RefinedRawEndpointNullKeyCore hm ε α β p.1 p.2 v‖ * r324GroupedIncrementCost hm p.2 i else 0 ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

The preceding patternwise identity survives integration on the full internal product space. This is the exact Fubini boundary seen by the raw case output; the endpoint-null core has not been removed.