Output shifts of ASP permutations and transmission witnesses

Changing the ASP shift while keeping the inversion set fixed translates every output value. We use the convention

outputShift τ c (n) = τ n - c.

Thus its slipface is translated in the first coordinate, (outputShift τ c).s a b = τ.s (a + c) b. A transmission witness for τ therefore becomes one for outputShift τ c by adding c chips at the first marked point. This is the useful normalization convention because both the slipface inequality and the prescribed degree move by the same integer c.

noncomputable def Utilities.outputShift (τ : AspPerm) (c : ℤ) : AspPerm

Change the output normalization of an ASP permutation, leaving its inversion set unchanged. Positive c subtracts c from every output.

Equations

• Utilities.outputShift τ c = (AspSet.ofAspPerm τ).toAspPerm (τ.χ + c)

@[simp]

theorem Utilities.inv_set_outputShift (τ : AspPerm) (c : ℤ) : invSet (outputShift τ c).func = invSet τ.func

Output shifts preserve the inversion set.

@[simp]

theorem Utilities.outputShift_chi (τ : AspPerm) (c : ℤ) : (outputShift τ c).χ = τ.χ + c

The ASP shift parameter increases by the output-shift amount.

@[simp]

theorem Utilities.outputShift_apply (τ : AspPerm) (c n : ℤ) : (outputShift τ c).func n = τ.func n - c

Pointwise form of the output-shift convention.

@[simp]

theorem Utilities.outputShift_s (τ : AspPerm) (c a b : ℤ) : (outputShift τ c).s.func a b = τ.s.func (a + c) b

The slipface of an output-shifted permutation is translated in its first coordinate.

@[simp]

theorem Utilities.outputShift_zero (τ : AspPerm) : outputShift τ 0 = τ

Output shifts form an additive action on ASP permutations.

@[simp]

theorem Utilities.outputShift_add (τ : AspPerm) (c d : ℤ) : outputShift (outputShift τ c) d = outputShift τ (c + d)

Successive output shifts add.

theorem Utilities.outputShift_injective (τ : AspPerm) : Function.Injective (outputShift τ)

For a fixed ASP permutation, the output-shift parameter is faithful.

theorem Utilities.outputShift_neg_add (τ : AspPerm) (c : ℤ) : outputShift (outputShift τ c) (-c) = τ

The inverse shift cancels an output shift.

noncomputable def Utilities.shiftZeroPerm (τ : AspPerm) : AspPerm

Canonical shift-zero representative of the fixed inversion set of τ.

Equations

• Utilities.shiftZeroPerm τ = Utilities.outputShift τ (-τ.χ)

@[simp]

theorem Utilities.shiftZeroPerm_chi (τ : AspPerm) : (shiftZeroPerm τ).χ = 0

@[simp]

theorem Utilities.inv_set_shiftZeroPerm (τ : AspPerm) : invSet (shiftZeroPerm τ).func = invSet τ.func

@[simp]

theorem Utilities.shiftZeroPerm_restore (τ : AspPerm) : outputShift (shiftZeroPerm τ) τ.χ = τ

Recovering the original output normalization from its shift-zero representative.

theorem Utilities.transmissionInequality_outputShift {G : CFGraph} (u v : G.V) (τ : AspPerm) (D : CFDiv G) (c a b : ℤ) : TransmissionInequality G u v (outputShift τ c) (D + c • oneChip u) a b ↔ TransmissionInequality G u v τ D (a + c) b

A single transmission inequality is transported by an output shift after adding the same number of chips at the first mark.

theorem Utilities.satisfiesTransmission_outputShift {G : CFGraph} (u v : G.V) (τ : AspPerm) (D : CFDiv G) (c : ℤ) (h : SatisfiesTransmission G u v τ D) : SatisfiesTransmission G u v (outputShift τ c) (D + c • oneChip u)

Adding c chips at the first mark transports a full transmission witness to the output-shifted permutation.

theorem Utilities.satisfiesTransmission_outputShift_iff {G : CFGraph} (u v : G.V) (τ : AspPerm) (D : CFDiv G) (c : ℤ) : SatisfiesTransmission G u v (outputShift τ c) (D + c • oneChip u) ↔ SatisfiesTransmission G u v τ D

Output shifting is an equivalence on transmission witnesses.

theorem Utilities.transmissionExists_outputShift_iff {G : CFGraph} (u v : G.V) (τ : AspPerm) (c : ℤ) : TransmissionExists G u v (outputShift τ c) ↔ TransmissionExists G u v τ

Existence is invariant under output normalization.

theorem Utilities.transmissionExists_shiftZeroPerm_iff {G : CFGraph} (u v : G.V) (τ : AspPerm) : TransmissionExists G u v (shiftZeroPerm τ) ↔ TransmissionExists G u v τ

Every transmission-existence problem is canonically equivalent to its shift-zero representative. This is the normal form a finite search should use.