Lax Lean Archive

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

Bounded baselines for both actual cross orientations

Lax342547.RawBaselines · concepts/Lax342547/RawBaselines.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

    For admissible tables and fresh paired lists, construct the two full nominal cross forms simultaneously. Each retains the actual pin/key entries, extends the whole table, and has the paper's 3K+28 bound in both reciprocal primal-to-channel orientations.

    Concept map
    47 concepts
    100%
    Exact-image bounds for independent affinecolumnsOrdered atom products in the actualgradient formPoint atoms and finite flavor distributionsRank control for the frozen baseline onprimal inputsFormal ordered product bits realizesymmetric correctionsConcrete 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 kernelExact 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 columnsThe 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 spacesBoolean point moments with restricted basecoordinatesThe 3K+28 baseline bound in the actualnominal coordinatesPrimal blocks of the nominal spaces andtheir bounded table partActual paired-witness key spaces satisfy thebaseline hypothesesBinary prescriptions at all endpoints of apaired scalar recipeFull paired witness lists and scalar recipeequationsRetractions with bounded rank on theprimal inputsExact images mixing independent injectiveframesJoint minus images after exposing severalplus framesPrimal projections and preservation ofeffective spacesBounded baselines for both actual crossorientationsActual frame observations realize thenominal channel contractionsRaw matrix frames and their tensorrealizationThe finite uniform raw-vertex lawCoupled scalar recipes give consistent atomgradientsJoint reference image caps across both signsand all drawsThe full reference cap for exact pin eventsNumerical cross tables, injection flags, andunary admissibilityA 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 taggeometryWell-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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax342547.PairedKeys
    2import Lax342547.NominalBaselines
    3
    4/-!
    5---
    6title: Bounded baselines for both actual cross orientations
    7type: lemma
    8---
    9For admissible tables and fresh paired lists, construct the two full
    10nominal cross forms simultaneously. Each retains the actual pin/key
    11entries, extends the whole table, and has the paper's 3K+28 bound in
    12both reciprocal primal-to-channel orientations.
    13-/
    14
    15namespace Lax342547.RawBaselines
    16
    17open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    18open Lax342547.CutProfiles
    19open Lax342547.PairedWitnesses Lax342547.PairedRecipes Lax342547.PairedKeys
    20open Lax342547.ExactPins Lax342547.TableSpaces Lax342547.SmallTables
    21open Lax342547.TableContractions Lax342547.RawContractions Lax342547.ReferencePins
    22open Lax342547.NominalPrimal Lax342547.FrozenBaselines Lax342547.KeySpans
    23
    24variable {k n b degree r : ℕ} {hr : 2 * r ≤ n}
    25 {H N : Type} [Fintype H] [Fintype N] {E : Moment k n b degree}
    26
    27def Frozen (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H)
    28 (W : Lists k n b degree r hr)
    29 (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N)
    30 (oA oB : Unit (H := H) (N := N) (E := E)) : Prop :=
    31 ∀ e,
    32 ExtendsFrozen (P.space (e, true)) (keys W e) (Q.space (e, false)) (keys (flip W) e)
    33 ((rawForms oA oB).forward e) (F.forward e) ∧
    34 ExtendsFrozen (Q.space (e, true)) (keys (flip W) e) (P.space (e, false)) (keys W e)
    35 ((rawForms oA oB).reverse e) (F.reverse e)
    36
    37def Bounded (F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H) (K : ℕ) : Prop :=
    38 ∀ e z,
    39 Module.finrank Binary (LinearMap.range ((F.forward e).compl₁₂ primal.subtype
    40 (channelEmbedding z))) ≤ 3 * K + 28 ∧
    41 Module.finrank Binary (LinearMap.range ((F.forward e).flip.compl₁₂ primal.subtype
    42 (channelEmbedding z))) ≤ 3 * K + 28 ∧
    43 Module.finrank Binary (LinearMap.range ((F.reverse e).compl₁₂ primal.subtype
    44 (channelEmbedding z))) ≤ 3 * K + 28 ∧
    45 Module.finrank Binary (LinearMap.range ((F.reverse e).flip.compl₁₂ primal.subtype
    46 (channelEmbedding z))) ≤ 3 * K + 28
    47
    48axiom raw_baselines (W : Lists k n b degree r hr)
    49 (P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N)
    50 (A B : Fin 2 → Finset (Fin b → Binary)) (hA : Excludes P A) (hB : Excludes Q B)
    51 (hfresh : FreshAgainst W A B) (K : ℕ) (hP : P.rank ≤ K) (hQ : Q.rank ≤ K)
    52 (oA oB : Unit (H := H) (N := N) (E := E)) (T : Table P Q)
    53 (hadmissible : Admissible T observation observation oA oB) :
    54 ∃ F : CrossForms (Component (Tag k)) (Coordinate k n b degree) H,
    55 Extends F T ∧ Frozen F W P Q oA oB ∧ Bounded F K
    56
    57end Lax342547.RawBaselines
    58
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…