Lax Lean Archive

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

Coupled scalar recipes give consistent atom gradients

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

    Theorem

    At one endpoint, a and the opposite matched a-values satisfy the two role equations. The opposite p-values satisfy the coupled equation. These numerical data determine compatible row sums on the two lists, and hence formal ordered product prescriptions for the desired gradients.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 recipe_bits proven

    2 recipe_matrix proven

    Lean source view on GitHub

    1import Lax342547.SymmetricPrescriptions
    2import Lax342547.BinaryPrescriptions
    3
    4/-!
    5---
    6title: Coupled scalar recipes give consistent atom gradients
    7type: theorem
    8---
    9At one endpoint, a and the opposite matched a-values satisfy the two
    10role equations. The opposite p-values satisfy the coupled equation.
    11These numerical data determine compatible row sums on the two lists,
    12and hence formal ordered product prescriptions for the desired gradients.
    13-/
    14
    15namespace Lax342547.RecipeRows
    16
    17open Lax342547.MomentSpace Lax342547.BinaryPrescriptions
    18
    19axiom recipe_matrix {I J : Type} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J]
    20 (a opposite p : I ⊕ J → Binary)
    21 (hrole₁ : (∑ i : I, a (Sum.inl i)) + (∑ i : I, opposite (Sum.inl i)) = 1)
    22 (hrole₂ : (∑ j : J, a (Sum.inr j)) + (∑ j : J, opposite (Sum.inr j)) = 1)
    23 (hcoupled : (∑ i : I, (p (Sum.inl i) + opposite (Sum.inl i))) =
    24 ∑ j : J, (p (Sum.inr j) + opposite (Sum.inr j))) :
    25 ∃ M : Matrix (I ⊕ J) (I ⊕ J) Binary, (∀ x y, M x y = M y x) ∧
    26 (∀ x, M x x = a x) ∧
    27 (∀ i : I, a (Sum.inl i) + ∑ t : I, M (Sum.inl t) (Sum.inl i) = 0) ∧
    28 (∀ j : J, a (Sum.inr j) + ∑ t : I, M (Sum.inl t) (Sum.inr j) = p (Sum.inr j)) ∧
    29 (∀ j : J, a (Sum.inr j) + ∑ t : J, M (Sum.inr t) (Sum.inr j) = 0) ∧
    30 (∀ i : I, a (Sum.inl i) + ∑ t : J, M (Sum.inr t) (Sum.inl i) = p (Sum.inl i))
    31
    32axiom recipe_bits {I J Term : Type} [Fintype I] [Fintype J] [Fintype Term]
    33 [Nonempty I] [Nonempty J]
    34 (a opposite p : I ⊕ J → Binary)
    35 (hrole₁ : (∑ i : I, a (Sum.inl i)) + (∑ i : I, opposite (Sum.inl i)) = 1)
    36 (hrole₂ : (∑ j : J, a (Sum.inr j)) + (∑ j : J, opposite (Sum.inr j)) = 1)
    37 (hcoupled : (∑ i : I, (p (Sum.inl i) + opposite (Sum.inl i))) =
    38 ∑ j : J, (p (Sum.inr j) + opposite (Sum.inr j)))
    39 (allowed : (I ⊕ J) → (I ⊕ J) → Term → Prop) (hallowed : ∀ x y, ∃ t, allowed x y t)
    40 (T₀ : Matrix (I ⊕ J) (I ⊕ J) Binary) (hsym : ∀ x y, T₀ x y = T₀ y x)
    41 (hdiag : ∀ x, T₀ x x = a x) :
    42 ∃ L R : (I ⊕ J) → (I ⊕ J) → Term → Binary,
    43 (∀ x y t, ¬ allowed x y t → L x y t = 0 ∧ R x y t = 0) ∧
    44 let T := fun x y => T₀ x y + productSum L R x y + productSum L R y x
    45 (∀ i : I, a (Sum.inl i) + ∑ t : I, T (Sum.inl t) (Sum.inl i) = 0) ∧
    46 (∀ j : J, a (Sum.inr j) + ∑ t : I, T (Sum.inl t) (Sum.inr j) = p (Sum.inr j)) ∧
    47 (∀ j : J, a (Sum.inr j) + ∑ t : J, T (Sum.inr t) (Sum.inr j) = 0) ∧
    48 (∀ i : I, a (Sum.inl i) + ∑ t : J, T (Sum.inr t) (Sum.inl i) = p (Sum.inl i))
    49
    50end Lax342547.RecipeRows
    51
    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…