Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324MarkedBlockOpenWord

The open word on the marked R-324 primitive block #

The genuine selected cell word is indexed on the full doubled moment. Only the unique residual primitive block containing the selected cross edge enters the R-324 high-frequency permutation estimate. This file restricts the full word along the canonical increasing enumeration of that block.

The restricted pairing is full and primitive, the selected endpoints remain a genuine ordered pairing edge, and every other edge still has equal cell labels. No multiplicity lower bound is imposed on the input word: singleton endpoint labels are allowed before dummy augmentation.

Canonical marked-block data #

source
theorem Anderson4D.r324MarkedResidualBlock_isFullyPairedOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
IsFullyPairedOn (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected)

Closedness of the unique marked residual block.

source
theorem Anderson4D.r324MarkedResidualBlock_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
IsRelPrimitiveOn (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected)

Relative primitivity of the unique marked residual block.

source
noncomputable def Anderson4D.r324MarkedResidualLowerPosition {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected))

Position of the selected lower endpoint in the canonical increasing enumeration of the marked residual block.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Anderson4D.r324MarkedResidualUpperPosition {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
    Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected))

    Position of the selected upper endpoint in the canonical increasing enumeration of the marked residual block.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Anderson4D.r324MarkedResidualBlockOrderIso_lower {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
      ↑((residualPrimitiveBlockOrderIso (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) ⋯) (r324MarkedResidualLowerPosition κp κm π selected)) = r324ResidualMarkedLowerEndpoint selected
      source
      @[simp]
      theorem Anderson4D.r324MarkedResidualBlockOrderIso_upper {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
      ↑((residualPrimitiveBlockOrderIso (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) ⋯) (r324MarkedResidualUpperPosition κp κm π selected)) = r324ResidualMarkedUpperEndpoint π selected
      source
      theorem Anderson4D.r324MarkedResidualBlockPairing_lower {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
      (residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) ⋯) (r324MarkedResidualLowerPosition κp κm π selected) = r324MarkedResidualUpperPosition κp κm π selected

      The selected endpoints remain a genuine edge after canonical restriction to the marked primitive block.

      source
      theorem Anderson4D.r324MarkedResidualLowerPosition_lt_upper {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
      r324MarkedResidualLowerPosition κp κm π selected < r324MarkedResidualUpperPosition κp κm π selected

      The selected edge remains ordered after increasing reindexing.

      source
      noncomputable def Anderson4D.r324MarkedResidualBlockWord {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) :
      Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected)) → Z4

      Restrict an ambient doubled-moment cell word to the unique marked primitive block in canonical increasing order.

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

        Transport of the open-edge constraint #

        source
        theorem Anderson4D.r324MarkedResidualBlockWord_respectsExcept {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) (hy : RespectsPairingExcept (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324ResidualMarkedUpperEndpoint π selected) y) :
        RespectsPairingExcept (residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) ⋯) (r324MarkedResidualLowerPosition κp κm π selected) (r324MarkedResidualUpperPosition κp κm π selected) (r324MarkedResidualBlockWord κp κm π selected y)

        Restricting an ambient open-edge word to the marked primitive block preserves the equality on every unmarked local pairing edge.

        source
        theorem Anderson4D.r324MarkedResidualBlockPairing_mem_primitiveFullPairings {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) :
        residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) ⋯ ∈ primitiveFullPairings (residualBlockOrder (r324MarkedResidualBlock κp κm π selected))

        The marked block pairing belongs to the exact primitive full-pairing fibre required by the permutation estimate.