Lax Lean Archive

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

Prepared-unit injection on actual accepting pairs

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

    Adaptive nominal pins and the actual admissible small tables retain accepting mass under all sixteen component tests. Exponential errors are paid relative to inverse-polynomial pair mass before any conditioning.

    Concept map
    117 concepts; 2 descendants hidden
    100%
    Finite accepting-family lossesActual finite accepting-pair injectionActual projected span deficitChannel bounds with adaptive protectedcoefficient spacesSampling after exposed coordinatesAdaptive sampling on disjoint coordinatesetsUnion over adaptive component coversExact-image bounds for independent affinecolumnsFinite amplified-test averagingExact uniform bilinear character meanWalsh operator bounds with explicit bilinearrankRank of a lifted tensor sumIndependent binary channel charactersActual raw frame channel phase tailsJoint channel law and itsindependent-column densityActual channel moments and phase tailsCombined column and row mode exposureRows of diagonal tensor mapsMoment estimates for actual componenttensor phasesComponentwise mode spaces and diagonaltensorsConcrete coordinates, quadratic testers, andthe self-Gram formThe affine minus-column law at a fixed plusframeExact conditioning costs and recovery offinite probability massesEntropy progress for residual pair lawsIndependence of distinct sample positionsJoin-stable classes of mode coversCount tensors killed by exposureActual exposure cover projectionCut profiles and the constant kernelRank of a diagonal familyDyadic span deficit estimatesA small dyadic tail scaleActual dyadic deficit recurrenceEntropy along feasible mixture lines,including new supportFull feasible support and finite informationprojectionExact image pins in nominal coefficientspacesProjection removes the exposed termsCount tested index occurrencesFinite pin-injection exceptionFinite linear images and their uniform-lawdensity boundsFinite even moment expansionFinite independent sampling and vertexexception tailsAmbient symmetries and frame marginalsReciprocal raw-frame orientation and dualpin avoidanceThe symmetric binary gradient formGram-conditioned columns and theirrank-failure probabilityTwo-sided Gram normalization forindividually injective framesGreedy independence of subspacesGreedy mode space exposureSmall actual greedy exposure tailsThe binary hole relationPaying the reference-image conditioning anddimension costsGreedy independent failure samplesAmplified channel failures on independentpinned spacesNo-cover rank growth on arbitrary finiteindicesRelative injection loss for polynomialaccepting massEarly channel choice and injection exponentbudgetsInjection parameter quantifiersAccepting-pair test unions and relative lossUniform injective-matrix densityUniform injective frames and channeltranspose failureActual deficits indexed by a distinct listFinite list tail statisticsFactorization and counting of low-rankbinary matricesDimension deficits after an arbitrary modemapExposed mode dimension budgetExplicit no-cover moment parameter marginsBoolean point moments with restricted basecoordinatesFinite moment probability and rank splitA low rank sum supplies an actual adaptivecoverNo-cover phase momentsRank growth without an adaptive modecoverSquared restriction cost for independent uniteventsFinite exposure partitionsActual phase averages from small exceptionaltailsPrepared-unit injection on actual acceptingpairsUniform primal-span avoidanceExact images mixing independent injectiveframesJoint minus images after exposing severalplus framesProjected nonzero terms in the actualremaining sumPrimal projections and preservation ofeffective spacesDimensions of projected mode spacesExact probabilities for independent protectedchannel imagesWalsh bounds for independent image lawsand separated phasesRank of a tensor killed in two quotientspacesRank loss under two restrictionsRaw accepting-family injection withexponential lossActual frame observations realize thenominal channel contractionsRaw matrix frames and their tensorrealizationThe finite uniform raw-vertex lawActual raw primal-span avoidanceOriginal retained-cell laws from finite PMFsJoint reference image caps across both signsand all drawsThe full reference cap for exact pin eventsFinite relative entropy and support costsRank loss under restriction of a bilinear formImage caps inside original retained cellsFinite sequential testsOne exposure controls both modesCounting all bounded-dimensional protectedspacesNumerical cross tables, injection flags, andunary admissibilityMonotonicity of span deficitsMode space span deficitsNonzero tensor count from span deficitsRank of an actual linear map sumTable contractions on effective profiles andtheir full extensionsActual table injection and ambient pinfailuresTable coordinates and private channelcomplementsMajority intersections in the cyclic taggeometryCharacters of all independent tensor channelsWell-defined channel contractions onprojected tensor spacesCounting component tensors with boundedtotal rankUniform raw channel phase tails overbounded-rank targetsAdmissible pair lawsWhole-unit conditioned pin avoidanceUniversal protected pin witnessesOrthogonality and finite Walsh correlationbounds
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 actual_accepting_table_loss proven

    2 actual_relative_table_injection proven

    Lean source view on GitHub

    1import Lax342547.TableInjection
    2import Lax342547.RawAcceptingInjection
    3import Lax342547.FrameTranspose
    4import Lax342547.InjectionUnion
    5import Lax342547.InjectionThresholds
    6
    7/-!
    8---
    9title: Prepared-unit injection on actual accepting pairs
    10type: lemma
    11---
    12Adaptive nominal pins and the actual admissible small tables retain
    13accepting mass under all sixteen component tests. Exponential errors are
    14paid relative to inverse-polynomial pair mass before any conditioning.
    15-/
    16
    17namespace Lax342547.PreparedInjection
    18
    19open Lax342547.MomentSpace Lax342547.RawFrames Lax342547.ExactPins
    20open Lax342547.TableSpaces Lax342547.SmallTables Lax342547.TableInjection
    21open Lax342547.RealCellLaws Lax342547.PushforwardWalsh Lax342547.RetainedImages
    22open Lax342547.RelativeEntropy
    23open scoped BigOperators
    24
    25abbrev Test (Comp : Type) := Comp × (Fin 2 × Fin 2) × (Bool × Bool)
    26
    27def testFailure {Comp B H N U : Type} [Fintype B] [Fintype H] [Fintype N]
    28 {E : Matrix B B Binary} (P : U → Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N)
    29 (A : U → Fin 2 → Comp → Frame B H N E) (j : Test Comp) (a b : U) : Prop :=
    30 Failed (P a) (P b) (A a) (A b) j.1 j.2.1.1 j.2.1.2 j.2.2.1 j.2.2.2
    31
    32structure Budget (K m t Cs p h N : ℕ) (η : ℝ) : Prop where
    33 gap : 1/(2 : ℝ)^t ≤ η/2
    34 ambient : p+h+1 ≤ N
    35 primal : p ≤ N/8
    36 density : m+h+1 ≤ N/10
    37 channel : 2*K+t+20*(K+1)*(Cs+3) ≤ h
    38 probes : 20*(K+1) ≤ N
    39 constant : m+h*K ≤ N
    40 small : 1/(2 : ℝ)^(N/2) ≤ η/2
    41
    42variable {Comp B H N U I : Type} [Fintype Comp] [Fintype B] [Fintype H] [Fintype N]
    43 [Fintype U] [Fintype I] [DecidableEq B] [DecidableEq H] [DecidableEq N]
    44 {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    45
    46axiom actual_accepting_table_loss (ρ : U → ℝ)
    47 (P : U → Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N)
    48 (A : U → Fin 2 → Comp → Frame B H N E)
    49 (accept : U → U → Prop) (CL CR : I → U → Prop) (keyL keyR : U → I)
    50 (T : ∀ a b,Table (P a) (P b)) (K m t Cs : ℕ) (M η : ℝ)
    51 (hρ : Probability ρ) (hM : 0 ≤ M)
    52 (hbudget : Budget K m t Cs (Fintype.card B) (Fintype.card H) (Fintype.card N) η)
    53 (hcapM : M ≤ (2 : ℝ)^m) (hcapMB : 2*M ≤ (2 : ℝ)^(m+Fintype.card N))
    54 (hcount : (Fintype.card I : ℝ) ≤ (2 : ℝ)^(Cs*Fintype.card N))
    55 (hP : ∀ u,(P u).rank ≤ K)
    56 (hcap : ∀ i e f,push ρ (fun u => A u i e) f ≤
    57 M*weights (PMF.uniformOfFintype (Frame B H N E)) f)
    58 (hleft : ∀ a b,accept a b ↔ CL (keyL b) a)
    59 (hright : ∀ a b,accept b a ↔ CR (keyR b) a)
    60 (hT : ∀ a b,accept a b → Admissible (T a b)
    61 Lax342547.ReferencePins.observation Lax342547.ReferencePins.observation (A a) (A b)) :
    62 cellMass (fun ab : U × U => ρ ab.1*ρ ab.2)
    63 (fun ab => accept ab.1 ab.2 ∧ ¬ Injecting (T ab.1 ab.2)) ≤
    64 (16*Fintype.card Comp : ℕ)*(η*cellMass (fun ab : U × U => ρ ab.1*ρ ab.2)
    65 (fun ab => accept ab.1 ab.2)+
    66 (1/(2 : ℝ)^(Fintype.card N/100)+1/(2 : ℝ)^Fintype.card N))
    67
    68axiom actual_relative_table_injection (ρ : U → ℝ)
    69 (P : U → Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N)
    70 (A : U → Fin 2 → Comp → Frame B H N E)
    71 (accept : U → U → Prop) (CL CR : I → U → Prop) (keyL keyR : U → I)
    72 (T : ∀ a b,Table (P a) (P b)) (K m t Cs : ℕ) (M η ε : ℝ)
    73 (hρ : Probability ρ) (hM : 0 ≤ M)
    74 (hbudget : Budget K m t Cs (Fintype.card B) (Fintype.card H) (Fintype.card N) η)
    75 (hcapM : M ≤ (2 : ℝ)^m) (hcapMB : 2*M ≤ (2 : ℝ)^(m+Fintype.card N))
    76 (hcount : (Fintype.card I : ℝ) ≤ (2 : ℝ)^(Cs*Fintype.card N))
    77 (hP : ∀ u,(P u).rank ≤ K)
    78 (hcap : ∀ i e f,push ρ (fun u => A u i e) f ≤
    79 M*weights (PMF.uniformOfFintype (Frame B H N E)) f)
    80 (hleft : ∀ a b,accept a b ↔ CL (keyL b) a)
    81 (hright : ∀ a b,accept b a ↔ CR (keyR b) a)
    82 (hT : ∀ a b,accept a b → Admissible (T a b)
    83 Lax342547.ReferencePins.observation Lax342547.ReferencePins.observation (A a) (A b))
    84 (c : ℕ) (hJ : 0 < 16*Fintype.card Comp) (hε : 0 ≤ ε)
    85 (hη : η = ε/(2*(16*Fintype.card Comp : ℕ)))
    86 (haccept : 1/(Fintype.card N : ℝ)^c ≤ cellMass (fun ab : U × U => ρ ab.1*ρ ab.2)
    87 (fun ab => accept ab.1 ab.2))
    88 (htail : (16*Fintype.card Comp : ℕ)*(1/(2 : ℝ)^(Fintype.card N/100)+1/(2 : ℝ)^Fintype.card N) ≤
    89 (ε/2)/(Fintype.card N : ℝ)^c) :
    90 cellMass (fun ab : U × U => ρ ab.1*ρ ab.2)
    91 (fun ab => accept ab.1 ab.2 ∧ ¬ Injecting (T ab.1 ab.2)) ≤
    92 ε*cellMass (fun ab : U × U => ρ ab.1*ρ ab.2) (fun ab => accept ab.1 ab.2)
    93
    94end Lax342547.PreparedInjection
    95
    Show 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…