The bounded pure remainder of an actual scalar recipe
Lax342547.ResidualRealization · concepts/Lax342547/ResidualRealization.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
Projected target forms and the bounded derivative product are removed from the actual recipe solution on the entire cut-profile pair space. The remaining pure response has per-individual matrix rank at most 14K+140. Compression and final channel factorization are separate obligations.
Concept map
Evidence
This concept declares 10 statements. Each proof establishes one of them relative to its assumptions.
1 baseline_response proven
2 bounded_remainder proven
3 derivative_response proven
4 matrix_response_sub proven
5 matrixPair_sub proven
6 paired_matrix_representation proven
7 product_response proven
8 projected_target proven
9 pure_response_sub proven
10 recipe_remainder proven
Lean source view on GitHub
| 1 | import Lax342547.RankedProjection |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The bounded pure remainder of an actual scalar recipe |
| 6 | type: lemma |
| 7 | --- |
| 8 | Projected target forms and the bounded derivative product are removed from |
| 9 | the actual recipe solution on the entire cut-profile pair space. The |
| 10 | remaining pure response has per-individual matrix rank at most 14K+140. |
| 11 | Compression and final channel factorization are separate obligations. |
| 12 | -/ |
| 13 | |
| 14 | namespace Lax342547.ResidualRealization |
| 15 | |
| 16 | open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry |
| 17 | open Lax342547.ConcreteCut Lax342547.CutProfiles Lax342547.PairedWitnesses |
| 18 | open Lax342547.ExactPins Lax342547.ProjectedPins Lax342547.PairedAnnihilators |
| 19 | open Lax342547.BarredSpaces Lax342547.ChannelChanges Lax342547.TableContractions |
| 20 | open Lax342547.DerivativeResponses Lax342547.ResponseMatrices Lax342547.RawBaselines |
| 21 | open Lax342547.TableSpaces |
| 22 | |
| 23 | variable {k n b degree r : ℕ} {hr : 2 * r ≤ n} {H N : Type} [Fintype H] |
| 24 | |
| 25 | noncomputable def matrixResponse {Comp B : Type} [Fintype Comp] [Fintype B] |
| 26 | (X : Submodule Binary (Comp → Matrix B B Binary)) (M : Fin 2 → Comp → Matrix B B Binary) : |
| 27 | Module.Dual Binary (Fin 2 → X) := |
| 28 | ∑ i, (∑ e, (matrixPair (M i e)).comp ((LinearMap.proj e).comp X.subtype)).comp (LinearMap.proj i) |
| 29 | |
| 30 | axiom matrixPair_sub {B : Type} [Fintype B] (M Q : Matrix B B Binary) : |
| 31 | matrixPair (M - Q) = matrixPair M - matrixPair Q |
| 32 | |
| 33 | axiom matrix_response_sub {Comp B : Type} [Fintype Comp] [Fintype B] |
| 34 | (X : Submodule Binary (Comp → Matrix B B Binary)) (M Q : Fin 2 → Comp → Matrix B B Binary) : |
| 35 | matrixResponse X (M - Q) = matrixResponse X M - matrixResponse X Q |
| 36 | |
| 37 | axiom projected_target [Fintype H] (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 | {K : ℕ} (hK : P.rank ≤ K) |
| 40 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 41 | (M : Fin 2 → Component (Tag k) → Moment k n b degree) : |
| 42 | ∃ (Q : Fin 2 → Component (Tag k) → Moment k n b degree) |
| 43 | (β : Lax342547.PureObstructions.Parameters W P U V), |
| 44 | Lax342547.PureObstructions.response W P U V β = matrixResponse (Profile k n b degree) Q ∧ |
| 45 | (∀ e, Module.finrank Binary (LinearMap.range (β e)) ≤ ∑ i, (M i e).rank) ∧ |
| 46 | ∀ i e, (M i e - Q i e).rank ≤ 2 * K + 28 ∧ (Q i e).rank ≤ (M i e).rank |
| 47 | |
| 48 | noncomputable def baselineMatrices |
| 49 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (z : Fin 2) : |
| 50 | Fin 2 → Component (Tag k) → Moment k n b degree := |
| 51 | fun i e => coefficients (fullPlus F e i z) (fullMinus F e i z) |
| 52 | |
| 53 | axiom baseline_response |
| 54 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (z : Fin 2) : |
| 55 | matrixResponse (Profile k n b degree) (baselineMatrices F z) = |
| 56 | ∑ i, (fullContraction F (Profile k n b degree) i z).comp (LinearMap.proj i) |
| 57 | |
| 58 | noncomputable def derivativeMatrices (W : Lists k n b degree r hr) |
| 59 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 60 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 61 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (z : Fin 2) |
| 62 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z) : |
| 63 | Fin 2 → Component (Tag k) → Moment k n b degree := |
| 64 | fun i e => coefficients |
| 65 | (restriction (barred W P (U e) (e, true)) (protectedChannel Q z (e, false)) (δ e) i) |
| 66 | (fullMinus F e i z) + coefficients (fullPlus F e i z) |
| 67 | (restriction (barred W P (V e) (e, false)) (protectedChannel Q z (e, true)) (ε e) i) |
| 68 | |
| 69 | axiom derivative_response (W : Lists k n b degree r hr) |
| 70 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 71 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 72 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (z : Fin 2) |
| 73 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z) : |
| 74 | matrixResponse (Profile k n b degree) (derivativeMatrices W P Q U V F z δ ε) = |
| 75 | response W P Q U V F z δ ε |
| 76 | |
| 77 | noncomputable def extraFamily (W : Lists k n b degree r hr) |
| 78 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 79 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) (z : Fin 2) |
| 80 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z) : |
| 81 | Lax342547.PureObstructions.Parameters W P U V := |
| 82 | fun e => extraProduct (barred W P (U e) (e, true)) (barred W P (V e) (e, false)) |
| 83 | (protectedChannel Q z (e, false)) (protectedChannel Q z (e, true)) (δ e) (ε e) |
| 84 | |
| 85 | noncomputable def productMatrices (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 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) (z : Fin 2) |
| 88 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z) : |
| 89 | Fin 2 → Component (Tag k) → Moment k n b degree := |
| 90 | fun i e => coefficients |
| 91 | (restriction (barred W P (U e) (e, true)) (protectedChannel Q z (e, false)) (δ e) i) |
| 92 | (restriction (barred W P (V e) (e, false)) (protectedChannel Q z (e, true)) (ε e) i) |
| 93 | |
| 94 | axiom product_response (W : Lists k n b degree r hr) |
| 95 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 96 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) (z : Fin 2) |
| 97 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z) : |
| 98 | Lax342547.PureObstructions.response W P U V (extraFamily W P Q U V z δ ε) = |
| 99 | matrixResponse (Profile k n b degree) (productMatrices W P Q U V z δ ε) |
| 100 | |
| 101 | axiom pure_response_sub (W : Lists k n b degree r hr) |
| 102 | (P : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 103 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 104 | (β γ : Lax342547.PureObstructions.Parameters W P U V) : |
| 105 | Lax342547.PureObstructions.response W P U V (β - γ) = |
| 106 | Lax342547.PureObstructions.response W P U V β - Lax342547.PureObstructions.response W P U V γ |
| 107 | |
| 108 | axiom bounded_remainder {K : ℕ} (W : Lists k n b degree r hr) |
| 109 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 110 | (hK : P.rank ≤ K) (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 111 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (hF : Bounded F K) (z : Fin 2) |
| 112 | (M : Fin 2 → Component (Tag k) → Moment k n b degree) |
| 113 | (β : Lax342547.PureObstructions.Parameters W P U V) |
| 114 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z) |
| 115 | (hδ : ∀ e, Module.finrank Binary (LinearMap.range (δ e)) ≤ 3 * K + 28) |
| 116 | (hsol : fullResponse W P Q U V F z β δ ε = matrixResponse (Profile k n b degree) M - |
| 117 | ∑ i, (fullContraction F (Profile k n b degree) i z).comp (LinearMap.proj i)) : |
| 118 | ∃ (M0 R0 : Fin 2 → Component (Tag k) → Moment k n b degree) |
| 119 | (β0 β1 : Lax342547.PureObstructions.Parameters W P U V), |
| 120 | Lax342547.PureObstructions.response W P U V β0 = matrixResponse (Profile k n b degree) M0 ∧ |
| 121 | (∀ e, Module.finrank Binary (LinearMap.range (β0 e)) ≤ ∑ i, (M i e).rank) ∧ |
| 122 | (∀ i e, (M0 i e).rank ≤ (M i e).rank) ∧ |
| 123 | Lax342547.PureObstructions.response W P U V β1 = matrixResponse (Profile k n b degree) R0 ∧ |
| 124 | (∀ i e, (R0 i e).rank ≤ 14 * K + 140) ∧ |
| 125 | β0 + β1 + extraFamily W P Q U V z δ ε = β |
| 126 | |
| 127 | axiom paired_matrix_representation {Comp B : Type} [Fintype Comp] [Fintype B] |
| 128 | (X : Submodule Binary (Comp → Matrix B B Binary)) (t : Fin 2 → Module.Dual Binary X) : |
| 129 | ∃ M : Fin 2 → Comp → Matrix B B Binary, |
| 130 | matrixResponse X M = ∑ i, (t i).comp (LinearMap.proj i) |
| 131 | |
| 132 | axiom recipe_remainder [Fintype N] {K : ℕ} {E : Moment k n b degree} |
| 133 | (hk : 0 < k) (W : Lists k n b degree r hr) |
| 134 | (D : Testers (k := k) (b := b) (degree := degree) hr) {copies : ℕ} |
| 135 | (L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 136 | (oA oB : Unit (H := H) (N := N) (E := E)) |
| 137 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 138 | (hK : P.rank ≤ K) (A B : Fin 2 → Finset (Fin b → Binary)) |
| 139 | (hA : Lax342547.PinLabelExclusions.Covers P A (2 * K + 28)) |
| 140 | (hfresh : ∀ i z t, (W.left i z t).label ∉ A i) |
| 141 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 142 | (hU : ∀ e j, IsCompl (protectedChannel P j (e, true)) (U e j)) |
| 143 | (hV : ∀ e j, IsCompl (protectedChannel P j (e, false)) (V e j)) |
| 144 | (T : Lax342547.SmallTables.Table P Q) (hT : Lax342547.SmallTables.Injecting T) |
| 145 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) |
| 146 | (hF : Extends F T) (hbounded : Bounded F K) |
| 147 | (hrecipe : ScalarRecipe W D L R oA oB T A B) |
| 148 | (hfrozen : Frozen F W P Q oA oB) (hkeys : MatchedKeys W oA oB) |
| 149 | (hgradients : ∀ i, Lax342547.ConcreteRecipes.RecipeGradients D L R |
| 150 | (Lax342547.PairedRecipes.endpointAtoms W i) (Lax342547.PairedRecipes.oppositeP W oB i)) |
| 151 | (hdegree : 6 * (2 * K + 28) + 4 ≤ degree) (z : Fin 2) |
| 152 | (M : Fin 2 → Component (Tag k) → Moment k n b degree) |
| 153 | (hM : matrixResponse (Profile k n b degree) M = |
| 154 | ∑ i, (D.role + gradient D L R (leftWitness W i z)).comp (LinearMap.proj i)) : |
| 155 | ∃ (M0 R0 : Fin 2 → Component (Tag k) → Moment k n b degree) |
| 156 | (β0 β1 : Lax342547.PureObstructions.Parameters W P U V) |
| 157 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z), |
| 158 | Lax342547.PureObstructions.response W P U V β0 = matrixResponse (Profile k n b degree) M0 ∧ |
| 159 | (∀ e, Module.finrank Binary (LinearMap.range (β0 e)) ≤ ∑ i, (M i e).rank) ∧ |
| 160 | (∀ i e, (M0 i e).rank ≤ (M i e).rank) ∧ |
| 161 | Lax342547.PureObstructions.response W P U V β1 = matrixResponse (Profile k n b degree) R0 ∧ |
| 162 | (∀ i e, (R0 i e).rank ≤ 14 * K + 140) ∧ |
| 163 | (∀ e, Module.finrank Binary (LinearMap.range (δ e)) ≤ 3 * K + 28 ∧ |
| 164 | Module.finrank Binary (LinearMap.range (ε e)) ≤ 3 * K + 28) ∧ |
| 165 | fullResponse W P Q U V F z (β0 + β1 + extraFamily W P Q U V z δ ε) δ ε = |
| 166 | ∑ i, (Lax342547.RecipeResiduals.residual W D L R F i z).comp (LinearMap.proj i) |
| 167 | |
| 168 | end Lax342547.ResidualRealization |
| 169 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments