Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Compression preserving allowed point moments and the actual cut domain

Lax342547.BaseCompression · concepts/Lax342547/BaseCompression.lean · lax-342547

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    A projection can fix a prescribed vector space and preserve observations, with rank bounded by the fixed-space dimension plus the observation rank. Blockwise base maps fix the constant coordinate and selector factor, send allowed points to allowed points, and preserve the actual cut-profile space. Their ranks and the transformation of target matrices are checked. The choice fixing every pin and residual target is treated separately.

    Concept map
    77 concepts
    100%
    Exact-image bounds for independent affinecolumnsOrdered atom products in the actualgradient formPoint atoms and finite flavor distributionsSparse unselected primal vectors in barredspaces lie in the pinsBarred response spaces and the actualobstruction rank budgetCompression preserving allowed pointmoments and the actual cut domainThe exact space of binary base momentsRank control for the frozen baseline onprimal inputsFormal ordered product bits realizesymmetric correctionsBounded allowed derivatives preserving theactual linearized responseAllowed channel changes and the actual tableinjection testsConcrete cut-space testers and the orderedmixer formConcrete coordinates, quadratic testers, andthe self-Gram formNumerical recipes prescribe the concretegradients on witness atomsThe affine minus-column law at a fixed plusframeCut profiles and the constant kernelThe full linearized response on pairs ofactual cut profilesFull response obstructions are effectiveprofiles plus selected atomsExact image pins in nominal coefficientspacesFinite linear images and their uniform-lawdensity boundsAmbient symmetries and frame marginalsFresh key directions are independent modulotable spacesBaseline bilinear extensions retaining allfrozen rows and columnsBaseline contractions on the selected atomsThe symmetric binary gradient formGram-conditioned columns and theirrank-failure probabilityTwo-sided Gram normalization forindividually injective framesThe binary hole relationPaying the reference-image conditioning anddimension costsUniform injective frames and channeltranspose failureFresh point-ray spans are disjoint from thenominal table spacesLow-rank Boolean moments have boundedlabel supportTriangle relations separate into individuallabel blocksBoolean point moments with restricted basecoordinatesThe 3K+28 baseline bound in the actualnominal coordinatesPrimal blocks of the nominal spaces andtheir bounded table partEndpoint projections of paired pure-responseannihilatorsActual paired-witness key spaces satisfy thebaseline hypothesesBinary prescriptions at all endpoints of apaired scalar recipeFull paired witness lists and scalar recipeequationsSparse pin exclusions with arbitrary basecoefficientsSparse residual contractions belong to theactual primal pinsRetractions with bounded rank on theprimal inputsExact images mixing independent injectiveframesJoint minus images after exposing severalplus framesPrimal projections and preservation ofeffective spacesPure obstructions on the actual pair of cutprofilesExtracting fresh label coefficients throughpin quotientsRank of a tensor killed in two quotientspacesBounded baselines for both actual crossorientationsActual frame observations realize thenominal channel contractionsRaw matrix frames and their tensorrealizationThe finite uniform raw-vertex lawGradient residuals vanish on effective profilesand selected atomsCoupled scalar recipes give consistent atomgradientsJoint reference image caps across both signsand all drawsThe full reference cap for exact pin eventsRemoving selected atoms leaves onlyunselected component labelsMatrix representations and the boundedresidual rank ingredientsUnrestricted linearized solutions for actualscalar recipesRank loss under restriction of a bilinear formSelected tensor blocks of actual pureobstructionsA selected affine ray determines its momentblockSubtracting selected atoms preserves pureannihilationSelected label coefficients agree across thecut profileInterpolation of finitely many binary selectorlabelsNumerical cross tables, injection flags, andunary admissibilityUnselected sparse vectors cannot concealfresh key coefficientsA uniform label budget for all sparse pinvectorsConsistent symmetric binary prescriptions ontwo witness listsTable contractions on effective profiles andtheir full extensionsTable coordinates and private channelcomplementsMajority intersections in the cyclic taggeometryPure bilinear responses detect quotienttensorsQuotient extractors isolate individual tensorlabel blocksWell-defined channel contractions onprojected tensor spacesWitness atoms and their numerical testerrecords
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 14 statements. Each proof establishes one of them relative to its assumptions.

    1 blockMap_allowed proven

    2 blockMap_profile proven

    3 blockMap_rank proven

    4 blockMap_tagSpace proven

    5 componentMap_cut proven

    6 concrete_compression_rank proven

    7 fixing_observed_projection proven

    8 liftBase_point proven

    9 liftBase_rank proven

    10 matrixPair_tensorMap proven

    11 matrixPair_trace proven

    12 tensorMap_moments proven

    13 tensorMap_point proven

    14 tensorMap_target proven

    Lean source view on GitHub

    1import Lax342547.ResponseMatrices
    2import Mathlib.LinearAlgebra.Matrix.Bilinear
    3import Mathlib.LinearAlgebra.Matrix.Trace
    4
    5/-!
    6---
    7title: Compression preserving allowed point moments and the actual cut domain
    8type: lemma
    9---
    10A projection can fix a prescribed vector space and preserve observations,
    11with rank bounded by the fixed-space dimension plus the observation rank.
    12Blockwise base maps fix the constant coordinate and selector factor, send
    13allowed points to allowed points, and preserve the actual cut-profile
    14space. Their ranks and the transformation of target matrices are checked.
    15The choice fixing every pin and residual target is treated separately.
    16-/
    17
    18namespace Lax342547.BaseCompression
    19
    20open Lax342547.MomentSpace
    21open Lax342547.TagGeometry Lax342547.ConcreteGeometry Lax342547.ConcreteCut Lax342547.CutProfiles
    22
    23axiom fixing_observed_projection {V X : Type} [AddCommGroup V] [Module Binary V]
    24 [AddCommGroup X] [Module Binary X] [FiniteDimensional Binary V]
    25 (U : Submodule Binary V) (L : V →ₗ[Binary] X) :
    26 ∃ p : V →ₗ[Binary] V, (∀ v ∈ U, p v = v) ∧ L.comp p = L ∧
    27 Module.finrank Binary (LinearMap.range p) ≤
    28 Module.finrank Binary U + Module.finrank Binary (LinearMap.range L)
    29
    30def liftBase {Coord Base : Type}
    31 (f : (Base → Binary) →ₗ[Binary] (Base → Binary)) :
    32 (Coord × Option Base → Binary) →ₗ[Binary] (Coord × Option Base → Binary) where
    33 toFun v c := match c.2 with
    34 | none => v (c.1, none)
    35 | some b => f (fun b => v (c.1, some b)) b
    36 map_add' v w := by
    37 ext ⟨a, c⟩
    38 cases c with
    39 | none => rfl
    40 | some b => exact congrFun (f.map_add _ _) b
    41 map_smul' c v := by
    42 ext ⟨a, q⟩
    43 cases q with
    44 | none => rfl
    45 | some b => exact congrFun (f.map_smul c _) b
    46
    47axiom liftBase_point {Label Coord Base : Type}
    48 (f : (Base → Binary) →ₗ[Binary] (Base → Binary))
    49 (p : Label → Coord → Binary) (s : Label) (z : Base → Binary) :
    50 liftBase (Coord := Coord) f (point p s z) = point p s (f z)
    51
    52noncomputable def tensorMap {B : Type} [Fintype B] (f : (B → Binary) →ₗ[Binary] (B → Binary)) :
    53 Matrix B B Binary →ₗ[Binary] Matrix B B Binary := by
    54 classical
    55 exact (mulRightLinearMap B Binary (LinearMap.toMatrix' f).transpose).comp
    56 (mulLeftLinearMap B Binary (LinearMap.toMatrix' f))
    57
    58axiom tensorMap_point {Label Coord Base : Type} [Fintype Coord] [Fintype Base]
    59 (f : (Base → Binary) →ₗ[Binary] (Base → Binary))
    60 (p : Label → Coord → Binary) (s : Label) (z : Base → Binary) :
    61 tensorMap (liftBase f) (pointMoment p s z) = pointMoment p s (f z)
    62
    63axiom tensorMap_moments {Label Coord Base : Type} [Fintype Coord] [Fintype Base]
    64 (f : (Base → Binary) →ₗ[Binary] (Base → Binary)) (p : Label → Coord → Binary)
    65 (A : Set Base)
    66 (hA : ∀ z, (∀ b, b ∉ A → z b = 0) → ∀ b, b ∉ A → f z b = 0) :
    67 (momentSpace p A).map (tensorMap (liftBase f)) ≤ momentSpace p A
    68
    69abbrev Block (k : ℕ) := (Tag k × Tag k) ⊕ Fin 3
    70
    71def blockMap {k n : ℕ} (A : Block k → (Fin n → Binary) →ₗ[Binary] (Fin n → Binary)) :
    72 (Base k n → Binary) →ₗ[Binary] (Base k n → Binary) where
    73 toFun z q := match q with
    74 | Sum.inl ((d, t), i) => A (Sum.inl (d, t)) (fun j => z (Sum.inl ((d, t), j))) i
    75 | Sum.inr (q, i) => A (Sum.inr q) (fun j => z (Sum.inr (q, j))) i
    76 map_add' z w := by
    77 ext q
    78 rcases q with ⟨⟨d, t⟩, i⟩ | ⟨q, i⟩ <;> exact congrFun (LinearMap.map_add _ _ _) i
    79 map_smul' c z := by
    80 ext q
    81 rcases q with ⟨⟨d, t⟩, i⟩ | ⟨q, i⟩ <;> exact congrFun (LinearMap.map_smul _ c _) i
    82
    83axiom blockMap_allowed {k n : ℕ}
    84 (A : Block k → (Fin n → Binary) →ₗ[Binary] (Fin n → Binary)) (l : Tag k)
    85 (z : Base k n → Binary) (hz : ∀ q, q ∉ allowedBase k n l → z q = 0) :
    86 ∀ q, q ∉ allowedBase k n l → blockMap A z q = 0
    87
    88axiom blockMap_tagSpace {k n b degree : ℕ}
    89 (A : Block k → (Fin n → Binary) →ₗ[Binary] (Fin n → Binary)) (l : Tag k) :
    90 (tagSpace k n b degree l).map (tensorMap (liftBase (blockMap A))) ≤ tagSpace k n b degree l
    91
    92def componentMap {Tag V : Type} [AddCommGroup V] [Module Binary V]
    93 (f : V →ₗ[Binary] V) : (Component Tag → V) →ₗ[Binary] (Component Tag → V) where
    94 toFun x e := f (x e)
    95 map_add' x y := by ext e; exact f.map_add _ _
    96 map_smul' c x := by ext e; exact f.map_smul c _
    97
    98axiom componentMap_cut {Tag V : Type} [AddCommGroup V] [Module Binary V]
    99 (f : V →ₗ[Binary] V) (w : Tag → V) :
    100 componentMap (Tag := Tag) f (cutMap w) = cutMap (fun t => f (w t))
    101
    102axiom blockMap_profile {k n b degree : ℕ}
    103 (A : Block k → (Fin n → Binary) →ₗ[Binary] (Fin n → Binary)) :
    104 (Profile k n b degree).map (componentMap (tensorMap (liftBase (blockMap A)))) ≤
    105 Profile k n b degree
    106
    107axiom liftBase_rank {Coord Base : Type} [Fintype Coord] [Fintype Base]
    108 (f : (Base → Binary) →ₗ[Binary] (Base → Binary)) :
    109 Module.finrank Binary (LinearMap.range (liftBase (Coord := Coord) f)) ≤
    110 Fintype.card Coord * (1 + Module.finrank Binary (LinearMap.range f))
    111
    112axiom matrixPair_trace {B : Type} [Fintype B] (M W : Matrix B B Binary) :
    113 Lax342547.ConcreteGeometry.matrixPair M W = Matrix.trace (M.transpose * W)
    114
    115axiom matrixPair_tensorMap {B : Type} [Fintype B]
    116 (f : (B → Binary) →ₗ[Binary] (B → Binary)) (M W : Matrix B B Binary) : by
    117 classical
    118 exact Lax342547.ConcreteGeometry.matrixPair M (tensorMap f W) =
    119 Lax342547.ConcreteGeometry.matrixPair
    120 ((LinearMap.toMatrix' f).transpose * M * LinearMap.toMatrix' f) W
    121
    122axiom tensorMap_target {B : Type} [Fintype B]
    123 (f : (B → Binary) →ₗ[Binary] (B → Binary)) (M : Matrix B B Binary)
    124 (hM : by classical exact (LinearMap.toMatrix' f).transpose * M * LinearMap.toMatrix' f = M) :
    125 (Lax342547.ConcreteGeometry.matrixPair M).comp (tensorMap f) =
    126 Lax342547.ConcreteGeometry.matrixPair M
    127
    128axiom blockMap_rank {k n : ℕ}
    129 (A : Block k → (Fin n → Binary) →ₗ[Binary] (Fin n → Binary)) :
    130 Module.finrank Binary (LinearMap.range (blockMap A)) ≤
    131 ∑ q, Module.finrank Binary (LinearMap.range (A q))
    132
    133axiom concrete_compression_rank {k n b degree D : ℕ}
    134 (A : Block k → (Fin n → Binary) →ₗ[Binary] (Fin n → Binary))
    135 (hA : ∀ q, Module.finrank Binary (LinearMap.range (A q)) ≤ D) :
    136 Module.finrank Binary (LinearMap.range
    137 (liftBase (Coord := SelectorCoordinates b degree) (blockMap A))) ≤
    138 Fintype.card (SelectorCoordinates b degree) * (1 + ((2 * k + 1)^2 + 3) * D)
    139
    140end Lax342547.BaseCompression
    141
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…