Lax Lean Archive

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

Full paired witness lists and scalar recipe equations

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

    Four cross pairs carry matched lists of one to seven actual point atoms. Freshness holds across both lists at each endpoint. The scalar recipe records odd diagonal sums, role parity, both effective-space equations, and both coupled endpoint equations, using the actual contractions.

    Concept map
    32 concepts
    100%
    Exact-image bounds for independent affinecolumnsPoint atoms and finite flavor distributionsFormal ordered product bits realizesymmetric correctionsConcrete cut-space testers and the orderedmixer formConcrete coordinates, quadratic testers, andthe self-Gram formThe 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 basecoordinatesFull 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 lawJoint reference image caps across both signsand all drawsThe full reference cap for exact pin eventsNumerical cross tables, injection flags, andunary admissibilityTable 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 diagonal_sums proven

    2 list_budgets proven

    3 tensor_sharing proven

    Lean source view on GitHub

    1import Lax342547.WitnessAtoms
    2import Lax342547.RawContractions
    3import Mathlib.Data.Fintype.Sigma
    4
    5/-!
    6---
    7title: Full paired witness lists and scalar recipe equations
    8type: lemma
    9---
    10Four cross pairs carry matched lists of one to seven actual point atoms.
    11Freshness holds across both lists at each endpoint. The scalar recipe
    12records odd diagonal sums, role parity, both effective-space equations,
    13and both coupled endpoint equations, using the actual contractions.
    14-/
    15
    16namespace Lax342547.PairedWitnesses
    17
    18open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    19open Lax342547.ConcreteCut Lax342547.CutProfiles Lax342547.Atoms Lax342547.WitnessAtoms
    20open Lax342547.RawFrames Lax342547.ExactPins Lax342547.ProjectedPins
    21open Lax342547.SmallTables Lax342547.TableContractions
    22
    23def diagonalBit {k n b degree r : ℕ} (hr : 2 * r ≤ n) (x : PointAtom k n b degree) : Binary :=
    24 eta hr (pointMoment (selectorEval (degree := degree)) x.label x.base)
    25
    26structure Lists (k n b degree r : ℕ) (hr : 2 * r ≤ n) where
    27 length : Fin 2 → Fin 2 → ℕ
    28 positive : ∀ i z, 1 ≤ length i z
    29 short : ∀ i z, length i z ≤ 7
    30 left : ∀ i z, Fin (length i z) → PointAtom k n b degree
    31 right : ∀ i z, Fin (length i z) → PointAtom k n b degree
    32 same_tag : ∀ i z t, (left i z t).tag = (right i z t).tag
    33 same_diagonal : ∀ i z t, diagonalBit hr (left i z t) = diagonalBit hr (right i z t)
    34 left_fresh : ∀ i, Function.Injective (fun t : Σ z, Fin (length i z) => (left i t.1 t.2).label)
    35 right_fresh : ∀ z, Function.Injective (fun t : Σ i, Fin (length i z) => (right t.1 z t.2).label)
    36
    37def other (i : Fin 2) : Fin 2 := ⟨1 - i.val, by omega⟩
    38
    39variable {k n b degree r : ℕ} {hr : 2 * r ≤ n}
    40
    41noncomputable def leftRepresentation (W : Lists k n b degree r hr) (i z : Fin 2) :
    42 Representation k n b degree :=
    43 ∑ t, atomRepresentation (W.left i z t).tag (W.left i z t).label
    44 (W.left i z t).base (W.left i z t).supported
    45
    46noncomputable def rightRepresentation (W : Lists k n b degree r hr) (i z : Fin 2) :
    47 Representation k n b degree :=
    48 ∑ t, atomRepresentation (W.right i z t).tag (W.right i z t).label
    49 (W.right i z t).base (W.right i z t).supported
    50
    51noncomputable def leftWitness (W : Lists k n b degree r hr) (i z : Fin 2) : Profile k n b degree :=
    52 ∑ t, (W.left i z t).profile
    53
    54noncomputable def rightWitness (W : Lists k n b degree r hr) (i z : Fin 2) : Profile k n b degree :=
    55 ∑ t, (W.right i z t).profile
    56
    57def FreshAgainst (W : Lists k n b degree r hr) (A B : Fin 2 → Finset (Fin b → Binary)) : Prop :=
    58 (∀ i z t, (W.left i z t).label ∉ A i) ∧ (∀ i z t, (W.right i z t).label ∉ B z)
    59
    60variable {H N : Type} [Fintype H] [Fintype N]
    61 {E : Moment k n b degree}
    62
    63abbrev Unit := Fin 2 → Component (Tag k) → Frame (Coordinate k n b degree) H N E
    64
    65noncomputable def ownContraction (o : Unit (H := H) (N := N) (E := E)) (i : Fin 2) :
    66 Profile k n b degree →ₗ[Binary] Binary :=
    67 (profileContraction (o (other i))).comp ((profileMap (o i)).comp (Profile k n b degree).subtype)
    68
    69def MatchedKeys (W : Lists k n b degree r hr) (oA oB : Unit (H := H) (N := N) (E := E)) : Prop :=
    70 ∀ i z t (e : Component (Tag k)), (W.left i z t).tag ∈ e.val →
    71 (oA i e).P.mulVec (W.left i z t).vector = (oB z e).P.mulVec (W.right i z t).vector ∧
    72 (oA i e).Q.mulVec (W.left i z t).vector = (oB z e).Q.mulVec (W.right i z t).vector
    73
    74structure ScalarRecipe (W : Lists k n b degree r hr)
    75 (D : Testers (k := k) (b := b) (degree := degree) hr) {copies : ℕ}
    76 (L R : Fin copies → Component (Tag k) → Component (Tag k) → Moment k n b degree)
    77 (oA oB : Unit (H := H) (N := N) (E := E))
    78 {P Q : Pin (Component (Tag k) × Bool) (Fin 2 × (Coordinate k n b degree ⊕ H)) N}
    79 (T : Table P Q) (A B : Fin 2 → Finset (Fin b → Binary)) : Prop where
    80 fresh : FreshAgainst W A B
    81 odd : ∀ i z, (∑ t, diagonalBit hr (W.left i z t)) = 1
    82 roles : ∀ i z, D.role (leftWitness W i z) + D.role (rightWitness W i z) = 1
    83 effectiveLeft : ∀ i z (x : effective (Profile k n b degree) P i),
    84 gradient D L R (leftWitness W i z) x.val = D.role x.val +
    85 starContraction T (Profile k n b degree) i z x
    86 effectiveRight : ∀ i z (x : effective (Profile k n b degree) Q z),
    87 gradient D L R (rightWitness W i z) x.val = D.role x.val +
    88 starContraction (flipTable T) (Profile k n b degree) z i x
    89 coupledLeft : ∀ i z,
    90 (ownContraction oA i + D.role) (leftWitness W i z) =
    91 (ownContraction oA (other i) + D.role) (leftWitness W (other i) z)
    92 coupledRight : ∀ i z,
    93 (ownContraction oB z + D.role) (rightWitness W i z) =
    94 (ownContraction oB (other z) + D.role) (rightWitness W i (other z))
    95
    96axiom list_budgets (W : Lists k n b degree r hr) :
    97 (∀ i, Fintype.card (Σ z, Fin (W.length i z)) ≤ 14) ∧
    98 ∀ z, Fintype.card (Σ i, Fin (W.length i z)) ≤ 14
    99
    100axiom diagonal_sums (W : Lists k n b degree r hr) (i z : Fin 2) :
    101 chiStar hr (leftRepresentation W i z) = ∑ t, diagonalBit hr (W.left i z t) ∧
    102 chiStar hr (rightRepresentation W i z) = ∑ t, diagonalBit hr (W.left i z t)
    103
    104axiom tensor_sharing (W : Lists k n b degree r hr)
    105 (oA oB : Unit (H := H) (N := N) (E := E)) (hkeys : MatchedKeys W oA oB) (i z : Fin 2) :
    106 profileMap (oA i) (leftWitness W i z).val = profileMap (oB z) (rightWitness W i z).val
    107
    108end Lax342547.PairedWitnesses
    109
    Show 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…