Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324MomentFiberReindex

Exact coordinate reindexing of an R-324 moment fibre #

A fixed doubled moment signature is exactly a left reduction-endpoint fibre, a right reduction-endpoint fibre, and a bijection between the two remaining single sets. This module records that equivalence and exposes the first primitive coordinate of the left fibre without taking an absolute value or paying a pairing-cardinality factor.

source
theorem Anderson4D.momentContractionSignature_eq_of_reductionEndpointSignatures_eq {m : ℕ} (e e' : MomentContraction m) (hleft : reductionEndpointSignature e.fst = reductionEndpointSignature e'.fst) (hright : reductionEndpointSignature e.snd.fst = reductionEndpointSignature e'.snd.fst) :
momentContractionSignature e = momentContractionSignature e'

Converse to the signature-separation lemma: equality of the two ordinary endpoint signatures gives equality of the doubled moment signature.

source
@[reducible, inline]
abbrev Anderson4D.MomentSignatureFiberAt {m : ℕ} (e₀ : MomentContraction m) :
Type

The finite fibre of contraction entities with the same doubled within-half signature as a reference entity.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Anderson4D.MomentSignatureCoordinates {m : ℕ} (e₀ : MomentContraction m) :
    Type

    Separated coordinates of one doubled moment-signature fibre.

    Equations
    Instances For
      source
      def Anderson4D.momentSignatureFiberEquivCoordinates {m : ℕ} (e₀ : MomentContraction m) :
      MomentSignatureFiberAt e₀ ≃ MomentSignatureCoordinates e₀

      Exact separation of a doubled moment-signature fibre into its two within-half endpoint fibres and the residual cross-single bijection.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Anderson4D.sum_momentSignatureFiber_eq_coordinates {m : ℕ} (e₀ : MomentContraction m) {A : Type u_1} [AddCommMonoid A] (F : MomentSignatureFiberAt e₀ → A) :
        ∑ e : MomentSignatureFiberAt e₀, F e = ∑ κp : ReductionEndpointFiberAt e₀.fst, ∑ κm : ReductionEndpointFiberAt e₀.snd.fst, ∑ π : ↥(↑κp).singles ≃ ↥(↑κm).singles, F ((momentSignatureFiberEquivCoordinates e₀).symm ⟨κp, ⟨κm, π⟩⟩)

        Finite-sum form of momentSignatureFiberEquivCoordinates.

        source
        theorem Anderson4D.sum_momentSignatureFiber_eq_firstLeftBlock {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) {A : Type u_1} [AddCommMonoid A] (F : MomentSignatureFiberAt e₀ → A) :
        ∑ e : MomentSignatureFiberAt e₀, F e = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))), ∑ κC : ExtractionComplementFiberAt e₀.fst (m - 1) Finset.univ hleft, ∑ κm : ReductionEndpointFiberAt e₀.snd.fst, ∑ π : ↥(↑((reductionEndpointFiberEquivBlockComplement e₀.fst hleft).symm (κB, κC))).singles ≃ ↥(↑κm).singles, F ((momentSignatureFiberEquivCoordinates e₀).symm ⟨(reductionEndpointFiberEquivBlockComplement e₀.fst hleft).symm (κB, κC), ⟨κm, π⟩⟩)

        The exact first left primitive-block coordinate of a fixed doubled moment fibre. The remaining right pairing and cross-single equivalence stay dependent on the reconstructed left complement, so no transport or multiplicity is hidden.

        source
        theorem Anderson4D.sum_momentSignatureFiber_eq_firstRightBlock {m : ℕ} (e₀ : MomentContraction m) (hright : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.snd.fst Finset.univ a b) {A : Type u_1} [AddCommMonoid A] (F : MomentSignatureFiberAt e₀ → A) :
        ∑ e : MomentSignatureFiberAt e₀, F e = ∑ κp : ReductionEndpointFiberAt e₀.fst, ∑ κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock e₀.snd.fst Finset.univ hright))), ∑ κC : ExtractionComplementFiberAt e₀.snd.fst (m - 1) Finset.univ hright, ∑ π : ↥(↑κp).singles ≃ ↥(↑((reductionEndpointFiberEquivBlockComplement e₀.snd.fst hright).symm (κB, κC))).singles, F ((momentSignatureFiberEquivCoordinates e₀).symm ⟨κp, ⟨(reductionEndpointFiberEquivBlockComplement e₀.snd.fst hright).symm (κB, κC), π⟩⟩)

        The exact first right primitive-block coordinate of a fixed doubled moment fibre. This is the right-hand analogue of sum_momentSignatureFiber_eq_firstLeftBlock.

        source
        theorem Anderson4D.sum_momentSignatureFiber_eq_firstLeftRightBlocks {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (hright : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.snd.fst Finset.univ a b) {A : Type u_1} [AddCommMonoid A] (F : MomentSignatureFiberAt e₀ → A) :
        ∑ e : MomentSignatureFiberAt e₀, F e = ∑ κBp : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))), ∑ κCp : ExtractionComplementFiberAt e₀.fst (m - 1) Finset.univ hleft, ∑ κBm : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock e₀.snd.fst Finset.univ hright))), ∑ κCm : ExtractionComplementFiberAt e₀.snd.fst (m - 1) Finset.univ hright, ∑ π : ↥(↑((reductionEndpointFiberEquivBlockComplement e₀.fst hleft).symm (κBp, κCp))).singles ≃ ↥(↑((reductionEndpointFiberEquivBlockComplement e₀.snd.fst hright).symm (κBm, κCm))).singles, F ((momentSignatureFiberEquivCoordinates e₀).symm ⟨(reductionEndpointFiberEquivBlockComplement e₀.fst hleft).symm (κBp, κCp), ⟨(reductionEndpointFiberEquivBlockComplement e₀.snd.fst hright).symm (κBm, κCm), π⟩⟩)

        Simultaneous exact exposure of the first primitive coordinate in both endpoint fibres. In particular, the residual cross-single equivalence remains dependent on both reconstructed complements; no cardinality factor or non-canonical transport is introduced.