InvalidOccupation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.LocalMoments.operatorSign line 12

lemma OAI.Problem335.LocalMoments.localPolynomial_zero_of_negative line 15

Source documentation

An invalid shifted coordinate forces the relevant local table factor to vanish.

lemma localPolynomial_zero_of_negative {σ : Type*} [DecidableEq σ]
    (derivative : Bool) (M : σ → ℕ) (p q r x : σ)
    (hneg : (M x : ℤ) + operatorSign derivative *
      ((if x = p then 1 else 0) - (if x = q then 1 else 0)) < 0) :
    localPolynomial derivative M p q r = 0 := by
…

Mentions: OAI.Problem335.LocalMoments.operatorSign, OAI.Problem335.LocalMoments.localPolynomial

lemma OAI.Problem335.LocalMoments.localPolynomial_product_zero_of_negative line 51

Source documentation

An invalid source in any layer annihilates the complete four-path table product.

lemma localPolynomial_product_zero_of_negative {ι σ : Type*}
    [DecidableEq σ] (layers : Finset ι) (derivative : ι → Bool)
    (M : ι × σ → ℕ) (p q r : ι → σ) (t : ι) (a : σ)
    (ht : t ∈ layers)
    (hneg : ShiftedOccupation.signedSource M (operatorSign ∘ derivative) p q (t, a) < 0) :
    (∏ j ∈ layers, localPolynomial (derivative j) (fun b => M (j, b)) (p j) (q j) (r j)) = 0 := by
…

Mentions: OAI.Problem335.ShiftedOccupation.signedSource, OAI.Problem335.LocalMoments.operatorSign, OAI.Problem335.LocalMoments.localPolynomial

lemma OAI.Problem335.LocalMoments.localPolynomial_product_zero_of_no_source line 63

Source documentation

The global table vanishes whenever no natural shifted source exists.

lemma localPolynomial_product_zero_of_no_source {ι σ : Type*}
    [Fintype ι] [DecidableEq σ] (derivative : ι → Bool)
    (M : ι × σ → ℕ) (p q r : ι → σ)
    (hbad : ¬ ∃ N : ι × σ → ℕ, ∀ x, (N x : ℤ) =
      ShiftedOccupation.signedSource M (operatorSign ∘ derivative) p q x) :
    (∏ j : ι, localPolynomial (derivative j) (fun b => M (j, b)) (p j) (q j) (r j)) = 0 := by
…

Mentions: OAI.Problem335.ShiftedOccupation.signedSource, OAI.Problem335.LocalMoments.operatorSign, OAI.Problem335.LocalMoments.localPolynomial