Selected label coefficients agree across the cut profile
Lax342547.SelectedScalars · concepts/Lax342547/SelectedScalars.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The three-edge cut relation separates by label. A coefficient supported on one tag star consequently has one scalar on the entire star. Applying the selected-block theorem to actual pure obstructions yields a single scalar multiple of each selected point atom.
Concept map
Evidence
This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.
1 obstruction_scalar proven
2 profile_triangle proven
3 selected_decomposition proven
4 selected_scalar proven
5 star_scalar proven
Lean source view on GitHub
| 1 | import Lax342547.SelectedBlocks |
| 2 | import Lax342547.LabelRelations |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Selected label coefficients agree across the cut profile |
| 7 | type: theorem |
| 8 | --- |
| 9 | The three-edge cut relation separates by label. A coefficient supported |
| 10 | on one tag star consequently has one scalar on the entire star. Applying |
| 11 | the selected-block theorem to actual pure obstructions yields a single |
| 12 | scalar multiple of each selected point atom. |
| 13 | -/ |
| 14 | |
| 15 | namespace Lax342547.SelectedScalars |
| 16 | |
| 17 | open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry |
| 18 | open Lax342547.ConcreteCut Lax342547.CutProfiles Lax342547.PairedWitnesses |
| 19 | open Lax342547.ExactPins Lax342547.PinLabelExclusions Lax342547.BaseMoments |
| 20 | open Lax342547.LabelRelations Lax342547.TensorBlocks |
| 21 | |
| 22 | axiom profile_triangle {k n b degree R : ℕ} (x : Profile k n b degree) |
| 23 | (L : Component (Tag k) → Finset (Fin b → Binary)) |
| 24 | (Z : Component (Tag k) → (Fin b → Binary) → Matrix (Option (Base k n)) (Option (Base k n)) Binary) |
| 25 | (hL : ∀ e, (L e).card ≤ R) (hdegree : 3 * R ≤ degree + 1) |
| 26 | (hM : ∀ e, x.val e = ∑ s ∈ L e, block selectorEval s (Z e s)) |
| 27 | (a b c : Tag k) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : |
| 28 | ∀ s, supported (L (edge a b hab)) (Z (edge a b hab)) s + |
| 29 | supported (L (edge b c hbc)) (Z (edge b c hbc)) s + |
| 30 | supported (L (edge a c hac)) (Z (edge a c hac)) s = 0 |
| 31 | |
| 32 | axiom star_scalar {Tag : Type} [DecidableEq Tag] [Nontrivial Tag] |
| 33 | (l : Tag) (c : Component Tag → Binary) |
| 34 | (htriangle : ∀ a b d (hab : a ≠ b) (hbd : b ≠ d) (had : a ≠ d), |
| 35 | c (edge a b hab) + c (edge b d hbd) + c (edge a d had) = 0) |
| 36 | (hout : ∀ e, l ∉ e.val → c e = 0) : |
| 37 | ∃ v : Binary, ∀ e, c e = if l ∈ e.val then v else 0 |
| 38 | |
| 39 | axiom selected_scalar {k n b degree R : ℕ} (hk : 0 < k) (x : Profile k n b degree) |
| 40 | (L : Component (Tag k) → Finset (Fin b → Binary)) |
| 41 | (Z : Component (Tag k) → (Fin b → Binary) → Matrix (Option (Base k n)) (Option (Base k n)) Binary) |
| 42 | (hL : ∀ e, (L e).card ≤ R) (hdegree : 3 * R ≤ degree + 1) |
| 43 | (hM : ∀ e, x.val e = ∑ s ∈ L e, block selectorEval s (Z e s)) |
| 44 | (s : Fin b → Binary) (l : Tag k) (z : Base k n → Binary) |
| 45 | (hshape : ∀ e, supported (L e) (Z e) s = if l ∈ e.val then |
| 46 | (supported (L e) (Z e) s) none none • baseMoment z else 0) : |
| 47 | ∃ v : Binary, ∀ e, supported (L e) (Z e) s = if l ∈ e.val then v • baseMoment z else 0 |
| 48 | |
| 49 | axiom obstruction_scalar {k n b degree r R : ℕ} {hr : 2 * r ≤ n} {H N : Type} |
| 50 | (hk : 0 < k) (W : Lists k n b degree r hr) |
| 51 | (P : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 52 | (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R) |
| 53 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 54 | (x : Fin 2 → Profile k n b degree) (h : Lax342547.PureObstructions.Annihilates W P U V x) |
| 55 | (i : Fin 2) (L : Component (Tag k) → Finset (Fin b → Binary)) |
| 56 | (Z : Component (Tag k) → (Fin b → Binary) → Matrix (Option (Base k n)) (Option (Base k n)) Binary) |
| 57 | (hL : ∀ e, (L e).card ≤ R) (hdegree : 3 * R ≤ degree + 1) |
| 58 | (hM : ∀ e, (x i).val e = ∑ s ∈ L e, block selectorEval s (Z e s)) |
| 59 | (hZ : ∀ e s, s ∈ L e → IsBaseMoment (Z e s)) |
| 60 | (u : Σ z, Fin (W.length i z)) (hfresh : (W.left i u.1 u.2).label ∉ A i) : |
| 61 | ∃ v : Binary, ∀ e, supported (L e) (Z e) (W.left i u.1 u.2).label = |
| 62 | if (W.left i u.1 u.2).tag ∈ e.val then v • baseMoment (W.left i u.1 u.2).base else 0 |
| 63 | |
| 64 | axiom selected_decomposition {k n b degree r K : ℕ} {hr : 2 * r ≤ n} {H N : Type} |
| 65 | [Fintype H] (hk : 0 < k) (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 | (hK : P.rank ≤ K) (A : Fin 2 → Finset (Fin b → Binary)) |
| 68 | (hA : Covers P A (2 * K + 28)) |
| 69 | (hfresh : ∀ i z t, (W.left i z t).label ∉ A i) |
| 70 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 71 | (x : Fin 2 → Profile k n b degree) (h : Lax342547.PureObstructions.Annihilates W P U V x) |
| 72 | (hdegree : 6 * (2 * K + 28) + 4 ≤ degree) (i : Fin 2) : |
| 73 | ∃ L : Component (Tag k) → Finset (Fin b → Binary), |
| 74 | ∃ Z : Component (Tag k) → (Fin b → Binary) → Matrix (Option (Base k n)) (Option (Base k n)) Binary, |
| 75 | ∃ c : (Σ z, Fin (W.length i z)) → Binary, |
| 76 | (∀ e, (L e).card ≤ 2 * K + 28 ∧ (∀ s ∈ L e, IsBaseMoment (Z e s)) ∧ |
| 77 | (∑ s ∈ L e, (Z e s).rank) ≤ 2 * K + 28 ∧ |
| 78 | ∀ a d, (x i).val e a d = ∑ s ∈ L e, |
| 79 | selectorEval s a.1 * selectorEval s d.1 * Z e s a.2 d.2) ∧ |
| 80 | ∀ u e, supported (L e) (Z e) (W.left i u.1 u.2).label = |
| 81 | if (W.left i u.1 u.2).tag ∈ e.val then c u • baseMoment (W.left i u.1 u.2).base else 0 |
| 82 | |
| 83 | end Lax342547.SelectedScalars |
| 84 |
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