Selected tensor blocks of actual pure obstructions
Lax342547.SelectedBlocks · concepts/Lax342547/SelectedBlocks.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
Freshness of the actual lists leaves one possible individual key ray at a selected label. Extracting its block through the pin-plus-key quotients forces a scalar point moment on its tag star and zero off that star. Agreement of those scalars across components is a subsequent obligation.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax342547.TensorBlocks |
| 2 | import Lax342547.QuotientExtractors |
| 3 | import Lax342547.PureObstructions |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Selected tensor blocks of actual pure obstructions |
| 8 | type: lemma |
| 9 | --- |
| 10 | Freshness of the actual lists leaves one possible individual key ray at |
| 11 | a selected label. Extracting its block through the pin-plus-key quotients |
| 12 | forces a scalar point moment on its tag star and zero off that star. |
| 13 | Agreement of those scalars across components is a subsequent obligation. |
| 14 | -/ |
| 15 | |
| 16 | namespace Lax342547.SelectedBlocks |
| 17 | |
| 18 | open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry |
| 19 | open Lax342547.ConcreteCut Lax342547.CutProfiles Lax342547.PairedWitnesses Lax342547.WitnessAtoms |
| 20 | open Lax342547.ExactPins Lax342547.ProjectedPins Lax342547.PinLabelExclusions |
| 21 | open Lax342547.BarredSpaces Lax342547.PairedAnnihilators Lax342547.BaseMoments |
| 22 | |
| 23 | variable {k n b degree r : ℕ} {hr : 2 * r ≤ n} {H N : Type} |
| 24 | |
| 25 | noncomputable def keyBase (W : Lists k n b degree r hr) (i : Fin 2) |
| 26 | (e : Component (Tag k)) (t : Σ z, Fin (W.length i z)) : Option (Base k n) → Binary := by |
| 27 | classical |
| 28 | exact if (W.left i t.1 t.2).tag ∈ e.val then baseEval (W.left i t.1 t.2).base else 0 |
| 29 | |
| 30 | noncomputable def individualRay (W : Lists k n b degree r hr) (i : Fin 2) |
| 31 | (e : Component (Tag k)) (t : Σ z, Fin (W.length i z)) : |
| 32 | Submodule Binary (Option (Base k n) → Binary) := by |
| 33 | classical |
| 34 | exact if (W.left i t.1 t.2).tag ∈ e.val then |
| 35 | Submodule.span Binary {baseEval (W.left i t.1 t.2).base} else ⊥ |
| 36 | |
| 37 | axiom individual_extractor {R : ℕ} (W : Lists k n b degree r hr) |
| 38 | (P : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 39 | (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R) |
| 40 | (i : Fin 2) (a : Component (Tag k) × Bool) (L : Finset (Fin b → Binary)) |
| 41 | (hL : L.card ≤ R) (u : Σ z, Fin (W.length i z)) |
| 42 | (hs : (W.left i u.1 u.2).label ∈ L) (hfresh : (W.left i u.1 u.2).label ∉ A i) : |
| 43 | ∃ q : (Vector k n b degree ⧸ (projected P i a ⊔ individualKeys W i a.1)) →ₗ[Binary] |
| 44 | ((Option (Base k n) → Binary) ⧸ individualRay W i a.1 u), |
| 45 | ∀ t ∈ L, ∀ v, q (Submodule.Quotient.mk |
| 46 | (Lax342547.SparsePins.labelTensor (selectorEval (degree := degree)) t v)) = |
| 47 | if t = (W.left i u.1 u.2).label then (individualRay W i a.1 u).mkQ v else 0 |
| 48 | |
| 49 | axiom selected_component {R : ℕ} (W : Lists k n b degree r hr) |
| 50 | (P : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 51 | (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R) |
| 52 | (U V : Fin 2 → Submodule Binary (H → Binary)) (e : Component (Tag k)) |
| 53 | (M : Fin 2 → Moment k n b degree) |
| 54 | (h : PairedAnnihilates M (barred W P U (e, true)) (barred W P V (e, false))) |
| 55 | (i : Fin 2) (L : Finset (Fin b → Binary)) (hL : L.card ≤ R) |
| 56 | (Z : (Fin b → Binary) → Matrix (Option (Base k n)) (Option (Base k n)) Binary) |
| 57 | (hM : M i = ∑ t ∈ L, Lax342547.TensorBlocks.block selectorEval t (Z t)) |
| 58 | (u : Σ z, Fin (W.length i z)) (hs : (W.left i u.1 u.2).label ∈ L) |
| 59 | (hfresh : (W.left i u.1 u.2).label ∉ A i) |
| 60 | (hZ : IsBaseMoment (Z (W.left i u.1 u.2).label)) : |
| 61 | Z (W.left i u.1 u.2).label = |
| 62 | if (W.left i u.1 u.2).tag ∈ e.val then |
| 63 | Z (W.left i u.1 u.2).label none none • baseMoment (W.left i u.1 u.2).base else 0 |
| 64 | |
| 65 | axiom selected_obstruction {R : ℕ} (W : Lists k n b degree r hr) |
| 66 | (P : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 67 | (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R) |
| 68 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 69 | (x : Fin 2 → Profile k n b degree) (h : Lax342547.PureObstructions.Annihilates W P U V x) |
| 70 | (i : Fin 2) (e : Component (Tag k)) (L : Finset (Fin b → Binary)) (hL : L.card ≤ R) |
| 71 | (Z : (Fin b → Binary) → Matrix (Option (Base k n)) (Option (Base k n)) Binary) |
| 72 | (hM : ∀ a c, (x i).val e a c = |
| 73 | ∑ t ∈ L, selectorEval t a.1 * selectorEval t c.1 * Z t a.2 c.2) |
| 74 | (u : Σ z, Fin (W.length i z)) (hs : (W.left i u.1 u.2).label ∈ L) |
| 75 | (hfresh : (W.left i u.1 u.2).label ∉ A i) |
| 76 | (hZ : IsBaseMoment (Z (W.left i u.1 u.2).label)) : |
| 77 | Z (W.left i u.1 u.2).label = |
| 78 | if (W.left i u.1 u.2).tag ∈ e.val then |
| 79 | Z (W.left i u.1 u.2).label none none • baseMoment (W.left i u.1 u.2).base else 0 |
| 80 | |
| 81 | end Lax342547.SelectedBlocks |
| 82 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments