Exponential residual-chain signatures for R-324

After the two within-half endpoint signatures have been fixed, paper Section 4.2 Step 3 fixes the nested intervals which cross the central cut. Recording the interval list itself would obscure the exponential counting ledger. A nested inside-to-outside chain is instead determined by the finite sets of its left and right endpoints: the left endpoints occur in strictly decreasing order and the right endpoints in strictly increasing order.

This file packages that endpoint signature, proves its rigidity, and regroups a fixed moment-signature fibre by at most 4^(2m) residual signatures. Within each refined fibre the complete primitive-block schedule is literally identical.

def Anderson4D.momentResidualChainSignature {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Finset (Fin (2 * m)) × Finset (Fin (2 * m))

Endpoint-role signature of the nested residual chain.

Equations

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

theorem Anderson4D.momentResidualIntervalChain_left_pairwise {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Pairwise (fun (a b : Fin (2 * m)) => b < a) (List.map Prod.fst (momentResidualIntervalChain κp κm π))

theorem Anderson4D.momentResidualIntervalChain_right_pairwise {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Pairwise (fun (a b : Fin (2 * m)) => a < b) (List.map Prod.snd (momentResidualIntervalChain κp κm π))

theorem Anderson4D.momentResidualIntervalChain_eq_of_signature_eq {m : ℕ} (e e' : MomentContraction m) (hsignature : momentResidualChainSignature e.fst e.snd.fst e.snd.snd = momentResidualChainSignature e'.fst e'.snd.fst e'.snd.snd) : momentResidualIntervalChain e.fst e.snd.fst e.snd.snd = momentResidualIntervalChain e'.fst e'.snd.fst e'.snd.snd

The two endpoint sets determine the canonical residual interval chain exactly.

def Anderson4D.momentResidualChainSignatures (m : ℕ) : Finset (Finset (Fin (2 * m)) × Finset (Fin (2 * m)))

Residual endpoint signatures realized by all order-m contraction entities.

Equations

• Anderson4D.momentResidualChainSignatures m = Finset.image (fun (e : Anderson4D.MomentContraction m) => Anderson4D.momentResidualChainSignature e.fst e.snd.fst e.snd.snd) Finset.univ

theorem Anderson4D.card_momentResidualChainSignatures_le (m : ℕ) : (momentResidualChainSignatures m).card ≤ 4 ^ (2 * m)

Fixing the cross-cut nested intervals costs only an exponential 4^(2m) factor.

def Anderson4D.momentResidualChainSignaturesInFiber {m : ℕ} (e₀ : MomentContraction m) : Finset (Finset (Fin (2 * m)) × Finset (Fin (2 * m)))

Residual endpoint signatures realized inside one fixed within-half moment-signature fibre.

Equations

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

theorem Anderson4D.card_momentResidualChainSignaturesInFiber_le {m : ℕ} (e₀ : MomentContraction m) : (momentResidualChainSignaturesInFiber e₀).card ≤ 4 ^ (2 * m)

theorem Anderson4D.sum_momentSignatureFiber_by_residualChainSignature {m : ℕ} (e₀ : MomentContraction m) {A : Type u_1} [AddCommMonoid A] (F : MomentSignatureFiberAt e₀ → A) : ∑ r ∈ momentResidualChainSignaturesInFiber e₀, ∑ e : MomentSignatureFiberAt e₀ with momentResidualChainSignature (↑e).fst (↑e).snd.fst (↑e).snd.snd = r, F e = ∑ e : MomentSignatureFiberAt e₀, F e

Exact regrouping of one moment-signature fibre by its residual-chain endpoint signature.

theorem Anderson4D.momentNonemptyPrimitiveBlocks_eq_of_signatures_eq {m : ℕ} (e e' : MomentContraction m) (hmoment : momentContractionSignature e = momentContractionSignature e') (hresidual : momentResidualChainSignature e.fst e.snd.fst e.snd.snd = momentResidualChainSignature e'.fst e'.snd.fst e'.snd.snd) : momentNonemptyPrimitiveBlocks e.fst e.snd.fst e.snd.snd = momentNonemptyPrimitiveBlocks e'.fst e'.snd.fst e'.snd.snd

Equal within-half and residual endpoint signatures give the identical complete primitive-block schedule.