Lax Lean Archive

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

Binary prescriptions at all endpoints of a paired scalar recipe

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

    Swapping the units preserves the full scalar recipe. At each endpoint, its two role equations and the opposite unit's coupled equation give formal ordered mixer bits realizing the required selected-atom gradients. These are prescriptions; their occurrence is a separate probability problem.

    Concept map
    37 concepts
    100%
    Exact-image bounds for independent affinecolumnsOrdered atom products in the actualgradient formPoint atoms and finite flavor distributionsFormal 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 marginalsThe 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 failureBoolean point moments with restricted basecoordinatesBinary prescriptions at all endpoints of apaired scalar recipeFull paired witness lists and scalar recipeequationsExact images mixing independent injectiveframesJoint minus images after exposing severalplus framesPrimal projections and preservation ofeffective spacesActual 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 admissibilityConsistent 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

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

    1 endpoint_fresh proven

    2 flip_recipe proven

    3 paired_prescriptions proven

    Lean source view on GitHub

    1import Lax342547.PairedWitnesses
    2import Lax342547.ConcreteRecipes
    3
    4/-!
    5---
    6title: Binary prescriptions at all endpoints of a paired scalar recipe
    7type: lemma
    8---
    9Swapping the units preserves the full scalar recipe. At each endpoint,
    10its two role equations and the opposite unit's coupled equation give
    11formal ordered mixer bits realizing the required selected-atom gradients.
    12These are prescriptions; their occurrence is a separate probability problem.
    13-/
    14
    15namespace Lax342547.PairedRecipes
    16
    17open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    18open Lax342547.ConcreteCut Lax342547.CutProfiles Lax342547.WitnessAtoms
    19open Lax342547.PairedWitnesses Lax342547.ConcreteRecipes
    20open Lax342547.ExactPins Lax342547.SmallTables Lax342547.TableContractions
    21
    22variable {k n b degree r : ℕ} {hr : 2 * r ≤ n}
    23
    24def flip (W : Lists k n b degree r hr) : Lists k n b degree r hr where
    25 length i z := W.length z i
    26 positive i z := W.positive z i
    27 short i z := W.short z i
    28 left i z := W.right z i
    29 right i z := W.left z i
    30 same_tag i z t := (W.same_tag z i t).symm
    31 same_diagonal i z t := (W.same_diagonal z i t).symm
    32 left_fresh := W.right_fresh
    33 right_fresh := W.left_fresh
    34
    35abbrev Position (W : Lists k n b degree r hr) (i : Fin 2) :=
    36 Fin (W.length i 0) ⊕ Fin (W.length i 1)
    37
    38def endpointAtoms (W : Lists k n b degree r hr) (i : Fin 2) :
    39 Position W i → PointAtom k n b degree := Sum.elim (W.left i 0) (W.left i 1)
    40
    41variable {H N : Type} [Fintype H] [Fintype N] {E : Moment k n b degree}
    42
    43noncomputable def oppositeP (W : Lists k n b degree r hr)
    44 (oB : Unit (H := H) (N := N) (E := E)) (i : Fin 2) : Position W i → Binary :=
    45 Sum.elim (fun t => ownContraction oB 0 (W.right i 0 t).profile)
    46 (fun t => ownContraction oB 1 (W.right i 1 t).profile)
    47
    48def Prescriptions (W : Lists k n b degree r hr)
    49 (D : Testers (k := k) (b := b) (degree := degree) hr)
    50 (oB : Unit (H := H) (N := N) (E := E)) (copies : ℕ) : Prop :=
    51 ∀ i, ∃ lbits rbits : Position W i → Position W i → ProductIndex k copies → Binary,
    52 (∀ x y t, ¬ allowedIndex ((endpointAtoms W i x).numerical hr)
    53 ((endpointAtoms W i y).numerical hr) t → lbits x y t = 0 ∧ rbits x y t = 0) ∧
    54 ∀ L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree,
    55 (∀ x y, x ≠ y → ∀ t, allowedIndex ((endpointAtoms W i x).numerical hr)
    56 ((endpointAtoms W i y).numerical hr) t →
    57 (L t.1 t.2.1 t.2.2).toBilin' (endpointAtoms W i x).vector
    58 (endpointAtoms W i y).vector = lbits x y t ∧
    59 (R t.1 t.2.1 t.2.2).toBilin' (endpointAtoms W i x).vector
    60 (endpointAtoms W i y).vector = rbits x y t) →
    61 RecipeGradients D L R (endpointAtoms W i) (oppositeP W oB i)
    62
    63axiom endpoint_fresh (W : Lists k n b degree r hr) (i : Fin 2) :
    64 Function.Injective (fun x : Position W i => (endpointAtoms W i x).label)
    65
    66axiom flip_recipe (W : Lists k n b degree r hr)
    67 (D : Testers (k := k) (b := b) (degree := degree) hr) {copies : ℕ}
    68 (L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree)
    69 (oA oB : Unit (H := H) (N := N) (E := E))
    70 {P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N}
    71 (T : Table P Q) (A B : Fin 2 → Finset (Fin b → Binary))
    72 (h : ScalarRecipe W D L R oA oB T A B) :
    73 ScalarRecipe (flip W) D L R oB oA (flipTable T) B A
    74
    75axiom paired_prescriptions (W : Lists k n b degree r hr)
    76 (D : Testers (k := k) (b := b) (degree := degree) hr) {copies : ℕ}
    77 (hk : 0 < k) (hcopies : 0 < copies)
    78 (L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree)
    79 (oA oB : Unit (H := H) (N := N) (E := E))
    80 {P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N}
    81 (T : Table P Q) (A B : Fin 2 → Finset (Fin b → Binary))
    82 (h : ScalarRecipe W D L R oA oB T A B) :
    83 Prescriptions W D oB copies ∧ Prescriptions (flip W) D oA copies
    84
    85end Lax342547.PairedRecipes
    86
    Show ProofShow ProofShow 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…