Rigidity of reduction endpoint signatures

The endpoint signature records the left- and right-bracket positions of the laminar interval family produced by Definition 3.1. A priori this forgets which left endpoint is matched to which right endpoint. This file proves that no information is lost: a laminar perfect matching with every edge oriented to the right is uniquely determined by its two endpoint sets.

The proof uses a maximal-disagreement argument. If two such matchings send the greatest disagreeing left endpoint to different right endpoints, pulling the smaller right endpoint back through the other matching either gives a larger disagreement or forces two intervals to cross.

The endpoint equivalence carried by an extraction list

theorem Anderson4D.exists_extractedPairOfLeftEndpoint {m : ℕ} (κ : PartialPairing (Fin m)) (a : ↥(leftEndpoints κ)) : ∃ p ∈ extract κ, p.1 = ↑a

noncomputable def Anderson4D.extractedPairOfLeftEndpoint {m : ℕ} (κ : PartialPairing (Fin m)) (a : ↥(leftEndpoints κ)) : Fin m × Fin m

The extracted interval chosen by a given left endpoint.

Equations

• Anderson4D.extractedPairOfLeftEndpoint κ a = Classical.choose ⋯

theorem Anderson4D.extractedPairOfLeftEndpoint_mem {m : ℕ} (κ : PartialPairing (Fin m)) (a : ↥(leftEndpoints κ)) : extractedPairOfLeftEndpoint κ a ∈ extract κ

@[simp]

theorem Anderson4D.extractedPairOfLeftEndpoint_fst {m : ℕ} (κ : PartialPairing (Fin m)) (a : ↥(leftEndpoints κ)) : (extractedPairOfLeftEndpoint κ a).1 = ↑a

theorem Anderson4D.exists_extractedPairOfRightEndpoint {m : ℕ} (κ : PartialPairing (Fin m)) (b : ↥(rightEndpoints κ)) : ∃ p ∈ extract κ, p.2 = ↑b

noncomputable def Anderson4D.extractedPairOfRightEndpoint {m : ℕ} (κ : PartialPairing (Fin m)) (b : ↥(rightEndpoints κ)) : Fin m × Fin m

The extracted interval chosen by a given right endpoint.

Equations

• Anderson4D.extractedPairOfRightEndpoint κ b = Classical.choose ⋯

theorem Anderson4D.extractedPairOfRightEndpoint_mem {m : ℕ} (κ : PartialPairing (Fin m)) (b : ↥(rightEndpoints κ)) : extractedPairOfRightEndpoint κ b ∈ extract κ

@[simp]

theorem Anderson4D.extractedPairOfRightEndpoint_snd {m : ℕ} (κ : PartialPairing (Fin m)) (b : ↥(rightEndpoints κ)) : (extractedPairOfRightEndpoint κ b).2 = ↑b

theorem Anderson4D.extractedPair_eq_of_fst_eq {m : ℕ} (κ : PartialPairing (Fin m)) {p q : Fin m × Fin m} (hp : p ∈ extract κ) (hq : q ∈ extract κ) (hfst : p.1 = q.1) : p = q

theorem Anderson4D.extractedPair_eq_of_snd_eq {m : ℕ} (κ : PartialPairing (Fin m)) {p q : Fin m × Fin m} (hp : p ∈ extract κ) (hq : q ∈ extract κ) (hsnd : p.2 = q.2) : p = q

noncomputable def Anderson4D.extractedEndpointEquiv {m : ℕ} (κ : PartialPairing (Fin m)) : ↥(leftEndpoints κ) ≃ ↥(rightEndpoints κ)

The extraction list is a perfect matching from its left endpoint set to its right endpoint set.

Equations

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

@[simp]

theorem Anderson4D.extractedEndpointEquiv_apply {m : ℕ} (κ : PartialPairing (Fin m)) (a : ↥(leftEndpoints κ)) : ↑((extractedEndpointEquiv κ) a) = (extractedPairOfLeftEndpoint κ a).2

theorem Anderson4D.extractedEndpointEquiv_lt {m : ℕ} (κ : PartialPairing (Fin m)) (a : ↥(leftEndpoints κ)) : ↑a < ↑((extractedEndpointEquiv κ) a)

theorem Anderson4D.extractedIntervals_laminar {m : ℕ} (κ : PartialPairing (Fin m)) {p q : Fin m × Fin m} (hp : p ∈ extract κ) (hq : q ∈ extract κ) (hpq : p ≠ q) : ReductionIntervalsLaminar p q

Public membership form of the pairwise laminarity theorem.

theorem Anderson4D.extractedEndpointEquiv_laminar {m : ℕ} (κ : PartialPairing (Fin m)) {a d : ↥(leftEndpoints κ)} (had : a ≠ d) : ReductionIntervalsLaminar (↑a, ↑((extractedEndpointEquiv κ) a)) (↑d, ↑((extractedEndpointEquiv κ) d))

Uniqueness of a laminar endpoint matching

theorem Anderson4D.rightOrientedLaminarEquiv_unique {m : ℕ} {L R : Finset (Fin m)} (f g : ↥L ≃ ↥R) (hf_lt : ∀ (a : ↥L), ↑a < ↑(f a)) (hg_lt : ∀ (a : ↥L), ↑a < ↑(g a)) (hf_laminar : ∀ {a d : ↥L}, a ≠ d → ReductionIntervalsLaminar (↑a, ↑(f a)) (↑d, ↑(f d))) (hg_laminar : ∀ {a d : ↥L}, a ≠ d → ReductionIntervalsLaminar (↑a, ↑(g a)) (↑d, ↑(g d))) : f = g

Two right-oriented laminar perfect matchings on the same endpoint sets are equal.

Rigidity consequences for extraction

def Anderson4D.finsetSubtypeEquivOfEq {α : Type u_1} [DecidableEq α] {A B : Finset α} (h : A = B) : ↥A ≃ ↥B

Equality of finsets induces the value-preserving equivalence of their element subtypes.

Equations

• Anderson4D.finsetSubtypeEquivOfEq h = { toFun := fun (a : ↥A) => ⟨↑a, ⋯⟩, invFun := fun (b : ↥B) => ⟨↑b, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Anderson4D.finsetSubtypeEquivOfEq_apply_val {α : Type u_1} [DecidableEq α] {A B : Finset α} (h : A = B) (a : ↥A) : ↑((finsetSubtypeEquivOfEq h) a) = ↑a

noncomputable def Anderson4D.transportedExtractedEndpointEquiv {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hleft : leftEndpoints κ = leftEndpoints κ') (hright : rightEndpoints κ = rightEndpoints κ') : ↥(leftEndpoints κ) ≃ ↥(rightEndpoints κ)

Transport the endpoint matching of κ' back to the endpoint subtype of κ.

Equations

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

@[simp]

theorem Anderson4D.transportedExtractedEndpointEquiv_apply_val {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hleft : leftEndpoints κ = leftEndpoints κ') (hright : rightEndpoints κ = rightEndpoints κ') (a : ↥(leftEndpoints κ)) : ↑((transportedExtractedEndpointEquiv κ κ' hleft hright) a) = ↑((extractedEndpointEquiv κ') ((finsetSubtypeEquivOfEq hleft) a))

theorem Anderson4D.extractedEndpointEquiv_eq_transport {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hleft : leftEndpoints κ = leftEndpoints κ') (hright : rightEndpoints κ = rightEndpoints κ') : extractedEndpointEquiv κ = transportedExtractedEndpointEquiv κ κ' hleft hright

Equal endpoint sets force equality after the canonical subtype transport.

theorem Anderson4D.mem_extract_iff_exists_extractedEndpoint {m : ℕ} (κ : PartialPairing (Fin m)) (p : Fin m × Fin m) : p ∈ extract κ ↔ ∃ (a : ↥(leftEndpoints κ)), p = (↑a, ↑((extractedEndpointEquiv κ) a))

Every extracted interval is the graph of the endpoint equivalence.

theorem Anderson4D.mem_extract_of_endpointSets_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hleft : leftEndpoints κ = leftEndpoints κ') (hright : rightEndpoints κ = rightEndpoints κ') {p : Fin m × Fin m} (hp : p ∈ extract κ) : p ∈ extract κ'

Equality of endpoint sets transports membership in the extraction interval family.

theorem Anderson4D.extract_perm_of_endpointSets_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hleft : leftEndpoints κ = leftEndpoints κ') (hright : rightEndpoints κ = rightEndpoints κ') : (extract κ).Perm (extract κ')

The interval lists attached to equal endpoint signatures contain exactly the same intervals. Their recursion order is irrelevant for all commutative Green products used in the closed formula.

theorem Anderson4D.extract_perm_of_reductionEndpointSignature_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hsignature : reductionEndpointSignature κ = reductionEndpointSignature κ') : (extract κ).Perm (extract κ')

Reduction endpoint signatures determine the extraction interval family up to the immaterial list order.

theorem Anderson4D.extractedRightEdges_eq_of_extract_perm {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hperm : (extract κ).Perm (extract κ')) : extractedRightEdges κ = extractedRightEdges κ'

Replaced chain-edge sets depend only on the extraction interval family, not on its list order.

theorem Anderson4D.renormalizedGreenSkeleton_eq_of_extract_perm {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hperm : (extract κ).Perm (extract κ')) : renormalizedGreenSkeleton κ = renormalizedGreenSkeleton κ'

The commutative Green skeleton is invariant under a permutation of the extraction interval list.

theorem Anderson4D.renormalizedGreenSkeleton_eq_of_reductionEndpointSignature_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hsignature : reductionEndpointSignature κ = reductionEndpointSignature κ') : renormalizedGreenSkeleton κ = renormalizedGreenSkeleton κ'

Endpoint signatures therefore determine the entire signed Green skeleton used in the closed renormalized integrand.