Grace/Cumulus/Cardinal/InversionExchange.g17

Open in Workbench Download source

Imports

PermutationExchange · Counting

Declarations

Source

1-- Inversion pairs under exchanges of permutation inputs (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.InversionExchange8import PermutationExchange9import Counting1011theorem inversions.pair (I p i j : Set)12  shows (i, j) ∈ inversions(I, p) ↔ i ∈ I ∧ j ∈ I ∧ i ∈ j ∧ p(j) ∈ p(i)13proof14  constructor15  . intro member16    obtain ⟨bound, a, ha, b, hb, shape, ordered, reversed⟩ := inversions.forward with member17    have coordinates := orderedPair.injective with shape18    rw [coordinates.left, coordinates.right]19    refine ⟨ha, hb, ordered, reversed⟩20  . intro data21    obtain ⟨hi, hj, ordered, reversed⟩ := data22    have pair := product.pair with hi, hj23    have witness : ∃ a ∈ I, ∃ b ∈ I, (i, j) = (a, b) ∧ a ∈ b ∧ p(b) ∈ p(a)24      refine ⟨i, hi, j, hj, rfl, ordered, reversed⟩25    apply inversions.backward26    constructor27    . exact pair28    . exact witness2930theorem productMap.involution (I t : Set)31  requires involution : InvolutionOn(t, I)32  shows InvolutionOn(productMap(t, t, I, I, I, I), I × I)33proof34  have function := InvolutionOn.function with involution35  have product := productMap.function with *36  unfold InvolutionOn37  refine ⟨product, ?_⟩38  intros q member39  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with member40  have imageI := FunctionBetween.apply_closed with function, hi41  have imageJ := FunctionBetween.apply_closed with function, hj42  have first := productMap.apply with hi, hj43  have second := productMap.apply at t, t, I, I, I, I, t(i), t(j) with *44  have inverseI := InvolutionOn.apply with involution, hi45  have inverseJ := InvolutionOn.apply with involution, hj46  cc4748-- An adjacent swap preserves the order of every pair other than its own.49theorem transposition.adjacent_order (n a i j : Nat)50  requires ha : a ∈ n51  requires hb : succ(a) ∈ n52  requires hi : i ∈ n53  requires hj : j ∈ n54  requires ordered : i < j55  requires other : ¬(i = a ∧ j = succ(a))56  shows transposition(n, a, succ(a))(i) < transposition(n, a, succ(a))(j)57proof58  have atFirst := transposition.first at n, a, succ(a) with *59  have atSecond := transposition.second at n, a, succ(a) with *60  have casesI : i = a ∨ i = succ(a) ∨ (i ≠ a ∧ i ≠ succ(a)) by tauto61  have casesJ : j = a ∨ j = succ(a) ∨ (j ≠ a ∧ j ≠ succ(a)) by tauto62  cases casesI with firstI | remainingI63  . rw [firstI, atFirst]64    cases casesJ with firstJ | remainingJ65    . have impossible : i < i66        arith67      have excluded := Less.irreflexive at i with *68      exfalso69      exact excluded with impossible70    . cases remainingJ with secondJ | outsideJ71      . exfalso72        apply other73        refine ⟨firstI, secondJ⟩74      . have unchanged := transposition.other with ha, hb, hj, outsideJ.left, outsideJ.right75        rw unchanged76        have below : a < j by arith77        have separated := outsideJ.right78        exact Less.successor_lower_of_ne with *79  . cases remainingI with secondI | outsideI80    . rw [secondI, atSecond]81      cases casesJ with firstJ | remainingJ82      . have impossible : i < i83          arith84        have excluded := Less.irreflexive at i with *85        exfalso86        exact excluded with impossible87      . cases remainingJ with secondJ | outsideJ88        . have impossible : i < i89            arith90          have excluded := Less.irreflexive at i with *91          exfalso92          exact excluded with impossible93        . have unchanged := transposition.other with ha, hb, hj, outsideJ.left, outsideJ.right94          rw unchanged95          arith96    . have unchangedI := transposition.other with ha, hb, hi, outsideI.left, outsideI.right97      rw unchangedI98      cases casesJ with firstJ | remainingJ99      . rw [firstJ, atFirst]100        arith101      . cases remainingJ with secondJ | outsideJ102        . rw [secondJ, atSecond]103          have below : i < succ(a) by arith104          have separated := outsideI.left105          exact Less.of_successor_upper_ne with *106        . have unchangedJ := transposition.other with ha, hb, hj, outsideJ.left, outsideJ.right107          rwa unchangedJ108109-- Remove the distinguished pair before transporting inversion pairs.110theorem inversions.adjacent_transport (n a : Nat) (p q : Set)111  requires ha : a ∈ n112  requires hb : succ(a) ∈ n113  requires permutation : p ∈ permutations(n)114  requires member : q ∈ inversions(n, p) ∖ {(a, succ(a))}115  shows productMap(transposition(n, a, succ(a)), transposition(n, a, succ(a)), n, n, n, n)(q) ∈ inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))}116proof117  have data := difference.membership.forward with member118  have bound : q ∈ n × n by simp [inversions]119  obtain ⟨productBound, i, hi, j, hj, shape⟩ := product.membership.forward with bound120  have inversion := data.left121  rw shape at inversion122  have facts := inversions.pair.forward with inversion123  have naturals := natural.member at n with *124  have ni := naturals with i, hi125  have nj := naturals with j, hj126  have orderBridge := Less.of_membership at i, j with *127  have ordered := orderBridge with facts.right.right.left128  have other : ¬(i = a ∧ j = succ(a)) by simp129  have orderedSwap := transposition.adjacent_order with *130  have function := transposition.function at n, a, succ(a) with *131  have involution := transposition.involution at n, a, succ(a) with *132  have imageI := FunctionBetween.apply_closed with function, hi133  have imageJ := FunctionBetween.apply_closed with function, hj134  have naturalI := naturals with transposition(n, a, succ(a))(i), imageI135  have naturalJ := naturals with transposition(n, a, succ(a))(j), imageJ136  have swappedOrder := membership.of_Less with naturalI, naturalJ, orderedSwap137  have inverseI := InvolutionOn.apply with involution, hi138  have inverseJ := InvolutionOn.apply with involution, hj139  have firstValue := transposition.first at n, a, succ(a) with *140  have secondValue := transposition.second at n, a, succ(a) with *141  have evaluatedI := permutationExchange.apply at n, a, succ(a), p, transposition(n, a, succ(a))(i) with *142  have evaluatedJ := permutationExchange.apply at n, a, succ(a), p, transposition(n, a, succ(a))(j) with *143  have pairedValue := productMap.apply with hi, hj144  have swappedInversion : (transposition(n, a, succ(a))(i), transposition(n, a, succ(a))(j)) ∈ inversions(n, permutationExchange(n, a, succ(a))(p)) by simp [inversions.pair, facts.right.right]145  have notDistinguished : ¬((transposition(n, a, succ(a))(i), transposition(n, a, succ(a))(j)) ∈ {(a, succ(a))})146    intro singleton147    have equal := singleton.membership.forward with singleton148    have coordinates := orderedPair.injective with equal149    have reversedI : i = succ(a) by cc150    have reversedJ : j = a by cc151    have reverse := ordered152    rw [reversedI, reversedJ] at reverse153    have successorMember := membership.self_successor at a with *154    have increaseBridge := Less.of_membership at a, succ(a) with *155    have increase := increaseBridge with successorMember156    have impossible := Less.transitive at a, succ(a), a with *157    have excluded := Less.irreflexive at a with *158    exact excluded with impossible159  rw [shape, pairedValue]160  exact difference.membership.backward with ⟨swappedInversion, notDistinguished⟩161162theorem inversions.adjacent_count_off_pair (n a : Nat) (p : Set)163  requires ha : a ∈ n164  requires hb : succ(a) ∈ n165  requires permutation : p ∈ permutations(n)166  shows cardinality(inversions(n, p) ∖ {(a, succ(a))}) = cardinality(inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))})167proof168  have exchange := permutationExchange.function at n, a, succ(a) with *169  have paired := FunctionBetween.apply_closed with exchange, permutation170  have exchangeInvolution := permutationExchange.involution at n, a, succ(a) with *171  have twice := InvolutionOn.apply with exchangeInvolution, permutation172  have swap := transposition.involution at n, a, succ(a) with *173  have product := productMap.involution with swap174  have subsetS : inversions(n, p) ∖ {(a, succ(a))} ⊆ n × n by simp [Subset, difference.membership, inversions]175  have subsetT : inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))} ⊆ n × n176    simp [Subset, difference.membership, inversions]177  have forward : ∀ q ∈ inversions(n, p) ∖ {(a, succ(a))}, productMap(transposition(n, a, succ(a)), transposition(n, a, succ(a)), n, n, n, n)(q) ∈ inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))} by simp [inversions.adjacent_transport]178  have backward : ∀ q ∈ inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))}, productMap(transposition(n, a, succ(a)), transposition(n, a, succ(a)), n, n, n, n)(q) ∈ inversions(n, p) ∖ {(a, succ(a))}179    intros q member180    have transport := inversions.adjacent_transport with *181    rwa twice at transport182  have bijective := InvolutionOn.restrict_between with product, subsetS, subsetT, forward, backward183  have finite := Finite.natural at n with *184  have square := Finite.product with finite, finite185  have finiteS := Finite.subset with square, subsetS186  exact cardinality.bijective with finiteS, bijective187188theorem inversions.exchange_distinguished (n a b : Nat) (p : Set)189  requires ha : a ∈ n190  requires hb : b ∈ n191  requires ordered : a < b192  requires permutation : p ∈ permutations(n)193  shows (a, b) ∈ inversions(n, permutationExchange(n, a, b)(p)) ↔ ¬((a, b) ∈ inversions(n, p))194proof195  have bijective := permutations.mem_iff.forward with permutation196  have injective := Bijective.injective with bijective197  have function := Injective.function with injective198  have imageA := FunctionBetween.apply_closed with function, ha199  have imageB := FunctionBetween.apply_closed with function, hb200  have naturals := natural.member at n with *201  have naturalA := naturals with p(a), imageA202  have naturalB := naturals with p(b), imageB203  have distinct : p(a) ≠ p(b)204    intro same205    have edgeA := FunctionBetween.relates_apply with function, ha206    have edgeB := FunctionBetween.relates_apply with function, hb207    rw same at edgeA208    have equal := Injective.cancel at p, n, n, a, b, p(b) with *209    arith210  have first := permutationExchange.apply at n, a, b, p, a with *211  have second := permutationExchange.apply at n, a, b, p, b with *212  have swapA := transposition.first at n, a, b with *213  have swapB := transposition.second at n, a, b with *214  rw swapA at first215  rw swapB at second216  have indexOrder := membership.of_Less at a, b with *, ordered217  constructor218  . intros inverted original219    have left := inversions.pair.forward with inverted220    have right := inversions.pair.forward with original221    have forwardMember := left.right.right.right222    rw [first, second] at forwardMember223    have forwardBridge := Less.of_membership at p(a), p(b) with *224    have reverseBridge := Less.of_membership at p(b), p(a) with *225    have forward := forwardBridge with forwardMember226    have reverse := reverseBridge with right.right.right.right227    arith228  . intro absent229    have comparison := Less.trichotomy at p(a), p(b) with *230    have forward : p(a) < p(b) by simp [membership.of_Less, inversions.pair]231    have forwardMember := membership.of_Less with naturalA, naturalB, forward232    apply inversions.pair.backward233    refine ⟨ha, hb, indexOrder, ?_⟩234    rwa [first, second]235236theorem inversions.adjacent_count (n a : Nat) (p : Set)237  requires ha : a ∈ n238  requires hb : succ(a) ∈ n239  requires permutation : p ∈ permutations(n)240  shows cardinality(inversions(n, permutationExchange(n, a, succ(a))(p))) = succ(cardinality(inversions(n, p))) ∨ cardinality(inversions(n, p)) = succ(cardinality(inversions(n, permutationExchange(n, a, succ(a))(p))))241proof242  have finite := Finite.natural at n with *243  have originalFinite := inversions.finite at n, p with finite244  have pairedFinite := inversions.finite at n, permutationExchange(n, a, succ(a))(p) with finite245  have ordered : a < succ(a) by arith246  have flip := inversions.exchange_distinguished with *247  have rest := inversions.adjacent_count_off_pair with *248  have alternatives : (a, succ(a)) ∈ inversions(n, p) ∨ ¬((a, succ(a)) ∈ inversions(n, p)) by tauto249  cases alternatives with present | absent250  . have pairedAbsent : ¬((a, succ(a)) ∈ inversions(n, permutationExchange(n, a, succ(a))(p)))251      tauto252    have unchanged : inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))} = inversions(n, permutationExchange(n, a, succ(a))(p))253      ext q254      simp255    have removed := cardinality.remove at inversions(n, p), (a, succ(a)) with *256    right257    cc258  . have pairedPresent : (a, succ(a)) ∈ inversions(n, permutationExchange(n, a, succ(a))(p))259      tauto260    have unchanged : inversions(n, p) ∖ {(a, succ(a))} = inversions(n, p)261      ext q262      simp263    have removed := cardinality.remove at inversions(n, permutationExchange(n, a, succ(a))(p)), (a, succ(a)) with *264    left265    cc266