Lax Lean Archive

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

Exactification of actual vanishing point predictions

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

    Degree-two generic parameter error removes base discrepancies; excluded-selector recovery and an actual common tester-one point force the diagonal coefficient and the whole cut-space residual to vanish.

    Concept map
    32 concepts; 1 descendant hidden
    100%
    Actual point atoms determine cut-spacefunctionalsActual finite atom parameterization anddegreesPoint atoms and finite flavor distributionsThe exact space of binary base momentsBoolean polynomial nonvanishing andexactificationCommon star atoms eliminate the diagonalpredictor coefficientConcrete cut-space testers and the orderedmixer formConcrete coordinates, quadratic testers, andthe self-Gram formExact conditioning costs and recovery offinite probability massesEntropy progress for residual pair lawsCut profiles and the constant kernelExactification of actual vanishing pointpredictionsEntropy along feasible mixture lines,including new supportFull feasible support and finite informationprojectionFinite independent sampling and vertexexception tailsThe symmetric binary gradient formThe binary hole relationBoolean point moments with restricted basecoordinatesSquared restriction cost for independent uniteventsBoolean degree of actual point-tensorevaluationsPolynomial degree of actual tensorevaluationsWalsh bounds for independent image lawsand separated phasesLinear point-tensor evaluations are BooleanquadraticsRaw matrix frames and their tensorrealizationOriginal retained-cell laws from finite PMFsFinite relative entropy and support costsImage caps inside original retained cellsInterpolation of finitely many binary selectorlabelsAn actual common point with diagonaltester oneMajority intersections in the cyclic taggeometryAdmissible pair lawsOrthogonality 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 nonexceptional_prediction_exact proven

    2 vanishing_prediction_exact proven

    Lean source view on GitHub

    1import Lax342547.AtomParameters
    2import Lax342547.SharedTesterPoint
    3import Lax342547.BooleanWeight
    4
    5/-!
    6---
    7title: Exactification of actual vanishing point predictions
    8type: lemma
    9---
    10Degree-two generic parameter error removes base discrepancies; excluded-selector recovery and an actual common tester-one point force the diagonal coefficient and the whole cut-space residual to vanish.
    11-/
    12
    13namespace Lax342547.EmptyPredictions
    14
    15open Lax342547.MomentSpace Lax342547.Atoms Lax342547.TagGeometry Lax342547.ConcreteCut
    16open Lax342547.ConcreteGeometry Lax342547.SelectorInterpolation Lax342547.RetainedImages
    17open Lax342547.AtomParameters Lax342547.SharedTesterPoint
    18open scoped BigOperators
    19
    20axiom nonexceptional_prediction_exact {k n b degree r : ℕ} (hr : 2*r ≤ n)
    21 (l : Tag k) (s : Fin b → Binary) (φ : Module.Dual Binary (Profile k n b degree)) (γ : Binary)
    22 (herr : cellMass (fun _ : Fin (ParameterSize n l Flavor.generic) → Binary =>
    23 1/(2 : ℝ)^(ParameterSize n l Flavor.generic))
    24 (fun x => φ (parameterAtom (degree := degree) l s Flavor.generic x)+
    25 γ*eta (b := b) (degree := degree) hr (pointMoment selectorEval s (parameterBase l Flavor.generic x)) ≠ 0) < 1/4) :
    26 ∀ z (hz : ∀ i,i ∉ allowedBase k n l → z i = 0),
    27 φ (atom (degree := degree) l s z hz)+γ*eta (b := b) (degree := degree) hr (pointMoment selectorEval s z) = 0
    28
    29axiom vanishing_prediction_exact {k n b degree r : ℕ} (hr : 2*r ≤ n) (hr0 : 0 < r)
    30 (φ : Module.Dual Binary (Profile k n b degree)) (γ : Binary)
    31 (E : Finset (Fin b → Binary)) (hE : 2^(degree+degree)*E.card < 2^b)
    32 (herr : ∀ l s,s ∉ E → cellMass (fun _ : Fin (ParameterSize n l Flavor.generic) → Binary =>
    33 1/(2 : ℝ)^(ParameterSize n l Flavor.generic))
    34 (fun x => φ (parameterAtom (degree := degree) l s Flavor.generic x)+
    35 γ*eta (b := b) (degree := degree) hr (pointMoment selectorEval s (parameterBase l Flavor.generic x)) ≠ 0) < 1/4) :
    36 γ = 0 ∧ φ = 0
    37
    38end Lax342547.EmptyPredictions
    39
    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…