Grace/Cumulus/Algebra/CoefficientSingle.g17

Open in Workbench Download source

Imports

Coefficients

Declarations

• singleValue defunique
• singleValue.closed theorem derivation
• singleValue.same theorem derivation
• singleValue.other theorem derivation
• singleValue.zero theorem derivation
• singleValue.iterated theorem derivation
• coefficientSingle defgraph
• coefficientSingle.same theorem derivation
• coefficientSingle.other theorem derivation
• coefficientSingle.support_membership theorem derivation
• coefficientSingle.support theorem derivation
• CoefficientMap.single theorem derivation
• coefficientSingle.support_nonzero theorem derivation

Source

1-- Single-index coefficient maps and their exact support (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.Algebra.CoefficientSingle8import Coefficients910defunique singleValue (A z a j i : Set) (value ∈ A) :=11  (i = j → value = a) ∧ (i ≠ j → value = z)12requires zeroIn : z ∈ A13requires coefficient : a ∈ A14proof15  have casesI : i = j ∨ i ≠ j16    tauto17  cases casesI with same | different18  . witness a19    refine ⟨coefficient, _, _⟩20    . intro equal21      rfl22    . intro impossible23      exfalso24      exact impossible with same25  . witness z26    refine ⟨zeroIn, _, _⟩27    . intro impossible28      exfalso29      exact different with impossible30    . intro unequal31      rfl32uniqueness33  intros u uIn first v vIn second34  have casesI : i = j ∨ i ≠ j35    tauto36  cases casesI with same | different37  . have uValue : u = a38      tauto39    have vValue : v = a40      tauto41    cc42  . have uValue : u = z43      tauto44    have vValue : v = z45      tauto46    cc4748theorem singleValue.closed (A z a j i : Set)49  requires zeroIn : z ∈ A50  requires coefficient : a ∈ A51  shows singleValue(A, z, a, j, i) ∈ A52proof53  have selected := singleValue.selected at A, z, a, j, i with *54  exact selected.left5556theorem singleValue.same (A z a j i : Set)57  requires zeroIn : z ∈ A58  requires coefficient : a ∈ A59  requires equal : i = j60  shows singleValue(A, z, a, j, i) = a61proof62  have selected := singleValue.selected at A, z, a, j, i with *63  tauto6465theorem singleValue.other (A z a j i : Set)66  requires zeroIn : z ∈ A67  requires coefficient : a ∈ A68  requires different : i ≠ j69  shows singleValue(A, z, a, j, i) = z70proof71  have selected := singleValue.selected at A, z, a, j, i with *72  tauto7374-- Selecting a zero coefficient remains zero for either branch.75theorem singleValue.zero (A z j i : Set)76  requires zeroIn : z ∈ A77  shows singleValue(A, z, z, j, i) = z78proof79  have alternatives : i = j ∨ i ≠ j by tauto80  cases alternatives with same | different81  . exact singleValue.same with *82  . exact singleValue.other with *8384-- Filtering before grouping agrees with filtering the selected group.85theorem singleValue.iterated (A z a k x c b : Set)86  requires zeroIn : z ∈ A87  requires coefficient : a ∈ A88  shows singleValue(A, z, singleValue(A, z, a, k(x), b), x, c) =89    singleValue(A, z, singleValue(A, z, a, x, c), k(c), b)90proof91  have alternatives : c = x ∨ c ≠ x by tauto92  cases alternatives with same | different93  . have left := singleValue.same at A, z, singleValue(A, z, a, k(x), b), x, c with *94    have right := singleValue.same at A, z, a, x, c with *95    cc96  . have left := singleValue.other at A, z, singleValue(A, z, a, k(x), b), x, c with *97    have innerRight := singleValue.other at A, z, a, x, c with *98    have right := singleValue.zero at A, z, k(c), b with *99    cc100101defgraph coefficientSingle (I A z a j : Set) (i ∈ I) : A := singleValue(A, z, a, j, i)102requires zeroIn : z ∈ A103requires coefficient : a ∈ A104proof105  exact singleValue.closed with *106107theorem coefficientSingle.same (I A z a j : Set)108  requires zeroIn : z ∈ A109  requires coefficient : a ∈ A110  requires index : j ∈ I111  shows coefficientSingle(I, A, z, a, j)(j) = a112proof113  have value := coefficientSingle.value at I, A, z, a, j, j with *114  have equal : j = j by rfl115  have selected := singleValue.same at A, z, a, j, j with *116  cc117118theorem coefficientSingle.other (I A z a j i : Set)119  requires zeroIn : z ∈ A120  requires coefficient : a ∈ A121  requires index : i ∈ I122  requires different : i ≠ j123  shows coefficientSingle(I, A, z, a, j)(i) = z124proof125  have value := coefficientSingle.value at I, A, z, a, j, i with *126  have selected := singleValue.other at A, z, a, j, i with *127  cc128129theorem coefficientSingle.support_membership (I A z a j i : Set)130  requires zeroIn : z ∈ A131  requires coefficient : a ∈ A132  shows i ∈ functionSupport(coefficientSingle(I, A, z, a, j), I, z) ↔ i ∈ I ∧ i = j ∧ a ≠ z133proof134  constructor135  . intro member136    have data := functionSupport.membership.forward with member137    have equal : i = j138      have alternatives : i = j ∨ i ≠ j by tauto139      cases alternatives with same | different140      . exact same141      . have value := coefficientSingle.other at I, A, z, a, j, i with *142        have contradiction := data.right with value143        tauto144    have nonzero : a ≠ z145      intro vanishes146      have atIndex : j ∈ I147        rw ← equal148        exact data.left149      have value := coefficientSingle.same at I, A, z, a, j with *150      have vanishing : coefficientSingle(I, A, z, a, j)(i) = z by cc151      exact data.right with vanishing152    refine ⟨data.left, equal, nonzero⟩153  . intro data154    rcases data with ⟨index, equal, nonzero⟩155    have atIndex : j ∈ I by rwa ← equal156    have value := coefficientSingle.same at I, A, z, a, j with *157    have different : coefficientSingle(I, A, z, a, j)(i) ≠ z158      intro vanishing159      have impossible : a = z by cc160      exact nonzero with impossible161    exact functionSupport.membership.backward with ⟨index, different⟩162163theorem coefficientSingle.support (I A z a j : Set)164  requires zeroIn : z ∈ A165  requires coefficient : a ∈ A166  shows functionSupport(coefficientSingle(I, A, z, a, j), I, z) ⊆ {j}167proof168  intros i hi169  have data := coefficientSingle.support_membership.forward with *170  exact singleton.membership.backward with data.right.left171172theorem CoefficientMap.single (I A z a j : Set)173  requires zeroIn : z ∈ A174  requires coefficient : a ∈ A175  shows CoefficientMap(coefficientSingle(I, A, z, a, j), I, A, z)176proof177  have function := coefficientSingle.function at I, A, z, a, j with *178  have support := coefficientSingle.support at I, A, z, a, j with *179  have finiteSingleton := Finite.singleton at j180  have finite := Finite.subset with finiteSingleton, support181  unfold CoefficientMap182  refine ⟨function, finite⟩183184theorem coefficientSingle.support_nonzero (I A z a j : Set)185  requires zeroIn : z ∈ A186  requires coefficient : a ∈ A187  requires index : j ∈ I188  requires nonzero : a ≠ z189  shows functionSupport(coefficientSingle(I, A, z, a, j), I, z) = {j}190proof191  ext i192  constructor193  . intro member194    have data := coefficientSingle.support_membership.forward with *195    exact singleton.membership.backward with data.right.left196  . intro member197    have equal := singleton.membership.forward with member198    rw equal199    apply coefficientSingle.support_membership.backward with zeroIn, coefficient200    refine ⟨index, rfl, nonzero⟩201