Unrestricted linearized solutions for actual scalar recipes
Lax342547.ResponseSolvability · concepts/Lax342547/ResponseSolvability.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
The actual pure and allowed derivative response families are linear in their parameters. The proved full obstruction decomposition and finite-dimensional annihilator duality construct unrestricted solutions on the whole cut-profile pair space. Bounded derivative ranks are treated separately; compression and private-channel factorization remain further obligations.
Concept map
Evidence
This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.
1 dual_range proven
2 full_add proven
3 full_smul proven
4 obstruction_correct proven
5 recipe_solution proven
6 selected_part_correct proven
7 solvable_of_annihilator_zero proven
8 unrestricted_solution proven
Lean source view on GitHub
| 1 | import Lax342547.EffectiveObstructions |
| 2 | import Lax342547.RecipeResiduals |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Unrestricted linearized solutions for actual scalar recipes |
| 7 | type: lemma |
| 8 | --- |
| 9 | The actual pure and allowed derivative response families are linear in their |
| 10 | parameters. The proved full obstruction decomposition and finite-dimensional |
| 11 | annihilator duality construct unrestricted solutions on the whole cut-profile |
| 12 | pair space. Bounded derivative ranks are treated separately; compression |
| 13 | and private-channel factorization remain further obligations. |
| 14 | -/ |
| 15 | |
| 16 | namespace Lax342547.ResponseSolvability |
| 17 | |
| 18 | |
| 19 | open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry |
| 20 | open Lax342547.ConcreteCut Lax342547.CutProfiles Lax342547.PairedWitnesses |
| 21 | open Lax342547.ExactPins Lax342547.PairedAnnihilators Lax342547.BarredSpaces |
| 22 | open Lax342547.ChannelChanges Lax342547.TableContractions Lax342547.DerivativeResponses |
| 23 | open Lax342547.TableSpaces |
| 24 | |
| 25 | open Lax342547.SelectedRemoval Lax342547.PairedRecipes Lax342547.RecipeResiduals |
| 26 | open Lax342547.PinLabelExclusions Lax342547.ProjectedPins Lax342547.RawBaselines |
| 27 | |
| 28 | variable {k n b degree r : ℕ} {hr : 2 * r ≤ n} {H N : Type} [Fintype H] |
| 29 | |
| 30 | abbrev Parameters (W : Lists k n b degree r hr) |
| 31 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 32 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) (z : Fin 2) := |
| 33 | Lax342547.PureObstructions.Parameters W P U V × |
| 34 | (PlusParameters W P Q U z × MinusParameters W P Q V z) |
| 35 | |
| 36 | axiom full_add (W : Lists k n b degree r hr) |
| 37 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 38 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 39 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (z : Fin 2) |
| 40 | (β β' : Lax342547.PureObstructions.Parameters W P U V) |
| 41 | (δ δ' : PlusParameters W P Q U z) (ε ε' : MinusParameters W P Q V z) : |
| 42 | fullResponse W P Q U V F z (β + β') (δ + δ') (ε + ε') = |
| 43 | fullResponse W P Q U V F z β δ ε + fullResponse W P Q U V F z β' δ' ε' |
| 44 | |
| 45 | axiom full_smul (W : Lists k n b degree r hr) |
| 46 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 47 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 48 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (z : Fin 2) |
| 49 | (a : Binary) (β : Lax342547.PureObstructions.Parameters W P U V) |
| 50 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z) : |
| 51 | fullResponse W P Q U V F z (a • β) (a • δ) (a • ε) = |
| 52 | a • fullResponse W P Q U V F z β δ ε |
| 53 | |
| 54 | axiom dual_range {K A X : Type} [Field K] [AddCommGroup A] [Module K A] |
| 55 | [AddCommGroup X] [Module K X] [FiniteDimensional K X] |
| 56 | (R : A →ₗ[K] Module.Dual K X) (t : Module.Dual K X) |
| 57 | (h : ∀ x, (∀ a, R a x = 0) → t x = 0) : ∃ a, R a = t |
| 58 | |
| 59 | axiom solvable_of_annihilator_zero (W : Lists k n b degree r hr) |
| 60 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 61 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 62 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (z : Fin 2) |
| 63 | (t : Module.Dual Binary (Fin 2 → Profile k n b degree)) |
| 64 | (h : ∀ x, Annihilates W P Q U V F z x → t x = 0) : |
| 65 | ∃ β δ ε, fullResponse W P Q U V F z β δ ε = t |
| 66 | |
| 67 | axiom selected_part_correct (W : Lists k n b degree r hr) |
| 68 | (P : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 69 | (c : ∀ i : Fin 2, (Σ z, Fin (W.length i z)) → Binary) (i : Fin 2) : |
| 70 | selectedPart W c i ∈ correctSpace W P i |
| 71 | |
| 72 | axiom obstruction_correct {K : ℕ} (hk : 0 < k) (W : Lists k n b degree r hr) |
| 73 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 74 | (hK : P.rank ≤ K) (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A (2 * K + 28)) |
| 75 | (hfresh : ∀ i z t, (W.left i z t).label ∉ A i) |
| 76 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 77 | (hU : ∀ e j, IsCompl (protectedChannel P j (e, true)) (U e j)) |
| 78 | (hV : ∀ e j, IsCompl (protectedChannel P j (e, false)) (V e j)) |
| 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 | (hdegree : 6 * (2 * K + 28) + 4 ≤ degree) : |
| 83 | ∀ i, x i ∈ correctSpace W P i |
| 84 | |
| 85 | axiom unrestricted_solution {K : ℕ} (hk : 0 < k) (W : Lists k n b degree r hr) |
| 86 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 87 | (hK : P.rank ≤ K) (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A (2 * K + 28)) |
| 88 | (hfresh : ∀ i z t, (W.left i z t).label ∉ A i) |
| 89 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 90 | (hU : ∀ e j, IsCompl (protectedChannel P j (e, true)) (U e j)) |
| 91 | (hV : ∀ e j, IsCompl (protectedChannel P j (e, false)) (V e j)) |
| 92 | (T : Lax342547.SmallTables.Table P Q) (hT : Lax342547.SmallTables.Injecting T) |
| 93 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (hF : Extends F T) (z : Fin 2) |
| 94 | (hdegree : 6 * (2 * K + 28) + 4 ≤ degree) |
| 95 | (t : Fin 2 → Module.Dual Binary (Profile k n b degree)) |
| 96 | (ht : ∀ i, correctSpace W P i ≤ LinearMap.ker (t i)) : |
| 97 | ∃ β δ ε, fullResponse W P Q U V F z β δ ε = ∑ i, (t i).comp (LinearMap.proj i) |
| 98 | |
| 99 | axiom recipe_solution [Fintype N] {K : ℕ} {E : Moment k n b degree} |
| 100 | (hk : 0 < k) (W : Lists k n b degree r hr) |
| 101 | (D : Testers (k := k) (b := b) (degree := degree) hr) {copies : ℕ} |
| 102 | (L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 103 | (oA oB : Unit (H := H) (N := N) (E := E)) |
| 104 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 105 | (hK : P.rank ≤ K) (A B : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A (2 * K + 28)) |
| 106 | (hfresh : ∀ i z t, (W.left i z t).label ∉ A i) |
| 107 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 108 | (hU : ∀ e j, IsCompl (protectedChannel P j (e, true)) (U e j)) |
| 109 | (hV : ∀ e j, IsCompl (protectedChannel P j (e, false)) (V e j)) |
| 110 | (T : Lax342547.SmallTables.Table P Q) (hT : Lax342547.SmallTables.Injecting T) |
| 111 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (hF : Extends F T) |
| 112 | (hrecipe : ScalarRecipe W D L R oA oB T A B) |
| 113 | (hfrozen : Frozen F W P Q oA oB) (hkeys : MatchedKeys W oA oB) |
| 114 | (hgradients : ∀ i, Lax342547.ConcreteRecipes.RecipeGradients D L R (endpointAtoms W i) (oppositeP W oB i)) |
| 115 | (hdegree : 6 * (2 * K + 28) + 4 ≤ degree) (z : Fin 2) : |
| 116 | ∃ β δ ε, fullResponse W P Q U V F z β δ ε = |
| 117 | ∑ i, (residual W D L R F i z).comp (LinearMap.proj i) |
| 118 | |
| 119 | end Lax342547.ResponseSolvability |
| 120 |
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