Full response obstructions are effective profiles plus selected atoms
Lax342547.EffectiveObstructions · concepts/Lax342547/EffectiveObstructions.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The actual two derivative tests force both residual contractions to zero. Double annihilation gives row and column membership in pin-plus-key spaces. Unselected sparse support removes the keys. Linear retractions identify the remaining row/column constraints with tensor-space membership, giving the actual effective remainder after selected subtraction.
Concept map
Evidence
This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.
1 effective_component proven
2 obstruction_decomposition proven
3 rows_of_contraction_zero proven
4 sparse_columns proven
5 tensor_of_columns_rows proven
6 transpose_blocks proven
7 unselected_tensor proven
8 unselected_vector proven
Lean source view on GitHub
| 1 | import Lax342547.DerivativeResponses |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Full response obstructions are effective profiles plus selected atoms |
| 6 | type: theorem |
| 7 | --- |
| 8 | The actual two derivative tests force both residual contractions to zero. |
| 9 | Double annihilation gives row and column membership in pin-plus-key spaces. |
| 10 | Unselected sparse support removes the keys. Linear retractions identify |
| 11 | the remaining row/column constraints with tensor-space membership, giving |
| 12 | the actual effective remainder after selected subtraction. |
| 13 | -/ |
| 14 | |
| 15 | namespace Lax342547.EffectiveObstructions |
| 16 | |
| 17 | open Lax342547.MomentSpace Lax342547.ProjectedPins Lax342547.PrimalContractions |
| 18 | open Lax342547.TensorAnnihilators |
| 19 | open Lax342547.TagGeometry Lax342547.ConcreteGeometry Lax342547.ConcreteCut |
| 20 | open Lax342547.CutProfiles |
| 21 | open Lax342547.PairedWitnesses Lax342547.ExactPins Lax342547.PinLabelExclusions |
| 22 | open Lax342547.SparsePins Lax342547.BarredSpaces Lax342547.ResidualLabels |
| 23 | open Lax342547.TableSpaces Lax342547.TableContractions Lax342547.DerivativeResponses |
| 24 | |
| 25 | axiom rows_of_contraction_zero {B : Type} [Fintype B] |
| 26 | (M : Matrix B B Binary) (T : Submodule Binary (B → Binary)) |
| 27 | (h : ∀ ψ : Module.Dual Binary (B → Binary), T ≤ LinearMap.ker ψ → |
| 28 | M.mulVecLin (coordinates ψ) = 0) : ∀ i, (fun j => M i j) ∈ T |
| 29 | |
| 30 | axiom tensor_of_columns_rows {B : Type} [Fintype B] |
| 31 | (M : Matrix B B Binary) (S T : Submodule Binary (B → Binary)) |
| 32 | (hcol : ∀ j, (fun i => M i j) ∈ S) (hrow : ∀ i, (fun j => M i j) ∈ T) : |
| 33 | M ∈ tensorSpace S T |
| 34 | |
| 35 | axiom unselected_vector {k n b degree r R : ℕ} {hr : 2 * r ≤ n} {H N : Type} |
| 36 | (W : Lists k n b degree r hr) |
| 37 | (P : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 38 | (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R) |
| 39 | (i : Fin 2) (a : Component (Tag k) × Bool) (L : Finset (Fin b → Binary)) |
| 40 | (hL : L.card ≤ R) (v : (Fin b → Binary) → Option (Base k n) → Binary) |
| 41 | (hdisjoint : Disjoint L (chosenLabels W i)) |
| 42 | (hfresh : ∀ z t, (W.left i z t).label ∉ A i) |
| 43 | (h : (∑ s ∈ L, labelTensor (selectorEval (degree := degree)) s (v s)) ∈ |
| 44 | projected P i a ⊔ individualKeys W i a.1) : |
| 45 | (∑ s ∈ L, labelTensor (selectorEval (degree := degree)) s (v s)) ∈ projected P i a |
| 46 | |
| 47 | axiom sparse_columns {Label Coord Base : Type} [Fintype Coord] [Fintype Base] |
| 48 | (p : Label → Coord → Binary) (L : Finset Label) |
| 49 | (Z : Label → Matrix Base Base Binary) (j : Coord × Base) : |
| 50 | ∃ v : Label → Base → Binary, |
| 51 | (fun a => (∑ s ∈ L, Lax342547.TensorBlocks.block p s (Z s)) a j) = |
| 52 | ∑ s ∈ L, labelTensor p s (v s) |
| 53 | |
| 54 | axiom transpose_blocks {Label Coord Base : Type} |
| 55 | (p : Label → Coord → Binary) (L : Finset Label) |
| 56 | (Z : Label → Matrix Base Base Binary) : |
| 57 | (∑ s ∈ L, Lax342547.TensorBlocks.block p s (Z s)).transpose = |
| 58 | ∑ s ∈ L, Lax342547.TensorBlocks.block p s ((Z s).transpose) |
| 59 | |
| 60 | axiom unselected_tensor {k n b degree r R : ℕ} {hr : 2 * r ≤ n} {H N : Type} |
| 61 | (W : Lists k n b degree r hr) |
| 62 | (P : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 63 | (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R) |
| 64 | (i : Fin 2) (e : Component (Tag k)) (L : Finset (Fin b → Binary)) (hL : L.card ≤ R) |
| 65 | (hdisjoint : Disjoint L (chosenLabels W i)) |
| 66 | (hfresh : ∀ z t, (W.left i z t).label ∉ A i) |
| 67 | (Z : (Fin b → Binary) → Matrix (Option (Base k n)) (Option (Base k n)) Binary) |
| 68 | (M : Moment k n b degree) (hM : M = ∑ s ∈ L, Lax342547.TensorBlocks.block selectorEval s (Z s)) |
| 69 | (hcol : ∀ j, (fun a => M a j) ∈ projected P i (e, true) ⊔ individualKeys W i e) |
| 70 | (hrow : ∀ a, (fun j => M a j) ∈ projected P i (e, false) ⊔ individualKeys W i e) : |
| 71 | M ∈ tensorSpace (projected P i (e, true)) (projected P i (e, false)) |
| 72 | |
| 73 | axiom effective_component {k n b degree r R : ℕ} {hr : 2 * r ≤ n} {H N : Type} [Fintype H] |
| 74 | (W : Lists k n b degree r hr) |
| 75 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 76 | (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R) |
| 77 | (hfresh : ∀ i z t, (W.left i z t).label ∉ A i) |
| 78 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 79 | (T : Lax342547.SmallTables.Table P Q) (hT : Lax342547.SmallTables.Injecting T) |
| 80 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (hF : Extends F T) (z : Fin 2) |
| 81 | (x : Fin 2 → Profile k n b degree) (h : Annihilates W P Q U V F z x) |
| 82 | (e : Component (Tag k)) (i : Fin 2) |
| 83 | (hU : ∀ j, IsCompl (protectedChannel P j (e, true)) (U e j)) |
| 84 | (hV : ∀ j, IsCompl (protectedChannel P j (e, false)) (V e j)) |
| 85 | (L : Finset (Fin b → Binary)) (hL : L.card ≤ R) (hdisjoint : Disjoint L (chosenLabels W i)) |
| 86 | (Z : (Fin b → Binary) → Matrix (Option (Base k n)) (Option (Base k n)) Binary) |
| 87 | (hM : (x i).val e = ∑ s ∈ L, Lax342547.TensorBlocks.block selectorEval s (Z s)) : |
| 88 | (x i).val e ∈ tensorSpace (projected P i (e, true)) (projected P i (e, false)) |
| 89 | |
| 90 | axiom obstruction_decomposition {k n b degree r K : ℕ} {hr : 2 * r ≤ n} {H N : Type} [Fintype H] |
| 91 | (hk : 0 < k) (W : Lists k n b degree r hr) |
| 92 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 93 | (hK : P.rank ≤ K) (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A (2 * K + 28)) |
| 94 | (hfresh : ∀ i z t, (W.left i z t).label ∉ A i) |
| 95 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 96 | (hU : ∀ e j, IsCompl (protectedChannel P j (e, true)) (U e j)) |
| 97 | (hV : ∀ e j, IsCompl (protectedChannel P j (e, false)) (V e j)) |
| 98 | (T : Lax342547.SmallTables.Table P Q) (hT : Lax342547.SmallTables.Injecting T) |
| 99 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (hF : Extends F T) (z : Fin 2) |
| 100 | (x : Fin 2 → Profile k n b degree) (h : Annihilates W P Q U V F z x) |
| 101 | (hdegree : 6 * (2 * K + 28) + 4 ≤ degree) : |
| 102 | ∃ c : ∀ i : Fin 2, (Σ z, Fin (W.length i z)) → Binary, |
| 103 | ∀ i, ((x - Lax342547.SelectedRemoval.selectedPart W c) i) ∈ |
| 104 | effective (Profile k n b degree) P i |
| 105 | |
| 106 | end Lax342547.EffectiveObstructions |
| 107 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments