Bounded allowed derivatives preserving the actual linearized response
Lax342547.BoundedDerivatives · concepts/Lax342547/BoundedDerivatives.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Sections of the observed baseline pairings compress derivative outputs inside their original perpendicular value spaces. The two actual derivative families retain their barred domain quotients, preserve the whole response, and have rank at most 3K+28 in an actual recipe solution. The residual matrix rank, pure correction and final channel factorization remain separate.
Concept map
Evidence
This concept declares 7 statements. Each proof establishes one of them relative to its assumptions.
1 allowed_projection proven
2 bounded_component proven
3 bounded_derivative proven
4 bounded_derivative_covectors proven
5 bounded_recipe_solution proven
6 bounded_response proven
7 observed_projection proven
Lean source view on GitHub
| 1 | import Lax342547.ResponseSolvability |
| 2 | import Mathlib.LinearAlgebra.Dimension.LinearMap |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Bounded allowed derivatives preserving the actual linearized response |
| 7 | type: theorem |
| 8 | --- |
| 9 | Sections of the observed baseline pairings compress derivative outputs |
| 10 | inside their original perpendicular value spaces. The two actual derivative |
| 11 | families retain their barred domain quotients, preserve the whole response, |
| 12 | and have rank at most 3K+28 in an actual recipe solution. The residual matrix |
| 13 | rank, pure correction and final channel factorization remain separate. |
| 14 | -/ |
| 15 | |
| 16 | namespace Lax342547.BoundedDerivatives |
| 17 | |
| 18 | open Lax342547.MomentSpace |
| 19 | open Lax342547.ChannelChanges |
| 20 | open Lax342547.PairedAnnihilators Lax342547.TableSpaces Lax342547.TableContractions |
| 21 | open Lax342547.DerivativeResponses Lax342547.NominalPrimal Lax342547.TensorAnnihilators |
| 22 | open Lax342547.BarredSpaces |
| 23 | open Lax342547.TagGeometry Lax342547.ConcreteGeometry Lax342547.ConcreteCut |
| 24 | open Lax342547.CutProfiles Lax342547.ExactPins Lax342547.PairedWitnesses Lax342547.RawBaselines |
| 25 | open Lax342547.PairedRecipes Lax342547.PinLabelExclusions |
| 26 | |
| 27 | axiom observed_projection {V X : Type} [AddCommGroup V] [Module Binary V] |
| 28 | [AddCommGroup X] [Module Binary X] [FiniteDimensional Binary V] |
| 29 | (L : V →ₗ[Binary] X) : |
| 30 | ∃ p : V →ₗ[Binary] V, L.comp p = L ∧ |
| 31 | Module.finrank Binary (LinearMap.range p) ≤ Module.finrank Binary (LinearMap.range L) |
| 32 | |
| 33 | axiom allowed_projection {H X : Type} [Fintype H] |
| 34 | [AddCommGroup X] [Module Binary X] [FiniteDimensional Binary X] |
| 35 | (S : Submodule Binary (H → Binary)) (G : X →ₗ[Binary] (H → Binary)) : |
| 36 | ∃ p : perpendicular S →ₗ[Binary] perpendicular S, |
| 37 | (∀ c x, dotProduct (p c).val (G x) = dotProduct c.val (G x)) ∧ |
| 38 | Module.finrank Binary (LinearMap.range p) ≤ Module.finrank Binary (LinearMap.range G) |
| 39 | |
| 40 | axiom bounded_derivative {D H X : Type} [AddCommGroup D] [Module Binary D] |
| 41 | [Fintype H] [AddCommGroup X] [Module Binary X] [FiniteDimensional Binary X] |
| 42 | (S : Submodule Binary (H → Binary)) (G : X →ₗ[Binary] (H → Binary)) |
| 43 | (δ : D →ₗ[Binary] perpendicular S) : |
| 44 | ∃ δ' : D →ₗ[Binary] perpendicular S, |
| 45 | (∀ v x, dotProduct (δ' v).val (G x) = dotProduct (δ v).val (G x)) ∧ |
| 46 | Module.finrank Binary (LinearMap.range δ') ≤ Module.finrank Binary (LinearMap.range G) |
| 47 | |
| 48 | axiom bounded_derivative_covectors {D H X : Type} [AddCommGroup D] [Module Binary D] |
| 49 | [Fintype H] [DecidableEq H] [AddCommGroup X] [Module Binary X] [FiniteDimensional Binary X] |
| 50 | (S : Submodule Binary (H → Binary)) (C : X →ₗ[Binary] Module.Dual Binary (H → Binary)) |
| 51 | (δ : D →ₗ[Binary] perpendicular S) : |
| 52 | ∃ δ' : D →ₗ[Binary] perpendicular S, |
| 53 | (∀ v x, dotProduct (δ' v).val (Lax342547.TensorAnnihilators.dualCoordinates (C x)) = |
| 54 | dotProduct (δ v).val (Lax342547.TensorAnnihilators.dualCoordinates (C x))) ∧ |
| 55 | Module.finrank Binary (LinearMap.range δ') ≤ Module.finrank Binary (LinearMap.range C) |
| 56 | |
| 57 | axiom bounded_component {Comp B H : Type} [Fintype B] [Fintype H] |
| 58 | (F : CrossForms Comp B H) (e : Comp) (z : Fin 2) |
| 59 | (D E : Submodule Binary (Nominal B H)) (S T : Submodule Binary (H → Binary)) |
| 60 | (R : ℕ) |
| 61 | (hplus : Module.finrank Binary (LinearMap.range ((F.forward e).compl₁₂ |
| 62 | (primal (B := B) (H := H)).subtype (channelEmbedding z))) ≤ R) |
| 63 | (hminus : Module.finrank Binary (LinearMap.range ((F.reverse e).flip.compl₁₂ |
| 64 | (primal (B := B) (H := H)).subtype (channelEmbedding z))) ≤ R) |
| 65 | (δ : (Nominal B H ⧸ D) →ₗ[Binary] perpendicular S) |
| 66 | (ε : (Nominal B H ⧸ E) →ₗ[Binary] perpendicular T) : |
| 67 | ∃ δ' ε', componentResponse F e z D E S T δ' ε' = componentResponse F e z D E S T δ ε ∧ |
| 68 | Module.finrank Binary (LinearMap.range δ') ≤ R ∧ |
| 69 | Module.finrank Binary (LinearMap.range ε') ≤ R |
| 70 | |
| 71 | axiom bounded_response {k n b degree r K : ℕ} {hr : 2 * r ≤ n} {H N : Type} [Fintype H] |
| 72 | (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 | (U V : Component (Tag k) → Fin 2 → Submodule Binary (H → Binary)) |
| 75 | (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (hF : Bounded F K) (z : Fin 2) |
| 76 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z) : |
| 77 | ∃ δ' ε', response W P Q U V F z δ' ε' = response W P Q U V F z δ ε ∧ |
| 78 | ∀ e, Module.finrank Binary (LinearMap.range (δ' e)) ≤ 3 * K + 28 ∧ |
| 79 | Module.finrank Binary (LinearMap.range (ε' e)) ≤ 3 * K + 28 |
| 80 | |
| 81 | axiom bounded_recipe_solution {H N : Type} [Fintype H] [Fintype N] {k n b degree r K : ℕ} {hr : 2 * r ≤ n} {E : Moment k n b degree} |
| 82 | (hk : 0 < k) (W : Lists k n b degree r hr) |
| 83 | (D : Testers (k := k) (b := b) (degree := degree) hr) {copies : ℕ} |
| 84 | (L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 85 | (oA oB : Unit (H := H) (N := N) (E := E)) |
| 86 | (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N) |
| 87 | (hK : P.rank ≤ K) (A B : 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) (hbounded : Bounded F K) |
| 94 | (hrecipe : ScalarRecipe W D L R oA oB T A B) |
| 95 | (hfrozen : Frozen F W P Q oA oB) (hkeys : MatchedKeys W oA oB) |
| 96 | (hgradients : ∀ i, Lax342547.ConcreteRecipes.RecipeGradients D L R (endpointAtoms W i) (oppositeP W oB i)) |
| 97 | (hdegree : 6 * (2 * K + 28) + 4 ≤ degree) (z : Fin 2) : |
| 98 | ∃ (β : Lax342547.PureObstructions.Parameters W P U V) |
| 99 | (δ : PlusParameters W P Q U z) (ε : MinusParameters W P Q V z), fullResponse W P Q U V F z β δ ε = |
| 100 | ∑ i, (Lax342547.RecipeResiduals.residual W D L R F i z).comp (LinearMap.proj i) ∧ |
| 101 | ∀ e, Module.finrank Binary (LinearMap.range (δ e)) ≤ 3 * K + 28 ∧ |
| 102 | Module.finrank Binary (LinearMap.range (ε e)) ≤ 3 * K + 28 |
| 103 | |
| 104 | end Lax342547.BoundedDerivatives |
| 105 |
Builds on
Used by
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments