IntegerResidueSplit.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact integer reconstruction implies the adaptive residue test

theorem OAI.Ostmann.intCast_frequency_zero line 12
theorem OAI.Ostmann.intCast_isUnit_of_coprime_frequency line 16
def OAI.Ostmann.integerResidueSplit line 23
Source documentation
A and B contain only the known nonbulk factors. The two variable products are units in the full modulus, and determine the parent product.
```
def integerResidueSplit {Q : ℕ} (f : NodeFrequencies) (hs : f.root ≠ 0)
    (hdvd : f.root.natAbs ∣ Q) (A B : ℤ) (L R : (ZMod Q)ˣ) : ArithmeticResidueSplit Q where
…
```
Mentions: OAI.Ostmann.NodeFrequencies, OAI.Ostmann.ArithmeticResidueSplit

theorem OAI.Ostmann.integerResidueSplit_support line 34

Source documentation

The integrality equation itself supplies the zero-numerator test. No equidistribution or independence is used in this bridge.

theorem integerResidueSplit_support {Q : ℕ} (f : NodeFrequencies)
    (hs : f.root ≠ 0) (hdvd : f.root.natAbs ∣ Q)
    (A B l r P : ℤ) (L R : (ZMod Q)ˣ)
    (hL : (L : ZMod Q) = l) (hR : (R : ZMod Q) = r)
    (hA : IsCoprime A f.root) (hB : IsCoprime B f.root)
    (heq : f.left * A * r - f.right * B * l = f.root * P) :
    (integerResidueSplit f hs hdvd A B L R).support L := by
…

Mentions: OAI.Ostmann.NodeFrequencies, OAI.Ostmann.integerResidueSplit

theorem OAI.Ostmann.singleArithmeticSplitTest_toData line 60

theorem OAI.Ostmann.integerResidueSplit_test line 67

Source documentation

A valid actual node gives a successful adaptive test after reduction. The statement remains valid for signed frequencies and reconstructed pivots.

theorem integerResidueSplit_test {Q : ℕ} (f : NodeFrequencies)
    (hs : f.root ≠ 0) (hdvd : f.root.natAbs ∣ Q)
    (A B l r P : ℤ) (L R : (ZMod Q)ˣ)
    (hL : (L : ZMod Q) = l) (hR : (R : ZMod Q) = r)
    (hA : IsCoprime A f.root) (hB : IsCoprime B f.root)
    (heq : f.left * A * r - f.right * B * l = f.root * P) :
    singleArithmeticSplitTest (integerResidueSplit f hs hdvd A B L R).toData L := by
…

Mentions: OAI.Ostmann.NodeFrequencies, OAI.Ostmann.singleArithmeticSplitTest, OAI.Ostmann.integerResidueSplit

theorem OAI.Ostmann.ArithmeticResidueSplit.support_of_reduced_integer_data line 79

Source documentation

At a later split only the surviving residues of the previously reconstructed coefficients are needed. Full-modulus equality is unnecessary.

theorem ArithmeticResidueSplit.support_of_reduced_integer_data {Q : ℕ}
    (d : ArithmeticResidueSplit Q) (x : (ZMod Q)ˣ)
    (A B l r P : ℤ) (L R : (ZMod d.frequencies.root.natAbs)ˣ)
    (hA : d.reduce d.leftFactor = A) (hB : d.reduce d.rightFactor = B)
    (hparent : ZMod.unitsMap d.frequency_dvd d.parentProduct = L * R)
    (hx : ZMod.unitsMap d.frequency_dvd x = L)
    (hL : (L : ZMod d.frequencies.root.natAbs) = l)
    (hR : (R : ZMod d.frequencies.root.natAbs) = r)
    (huA : IsCoprime A d.frequencies.root) (huB : IsCoprime B d.frequencies.root)
    (heq : d.frequencies.left * A * r - d.frequencies.right * B * l = d.frequencies.root * P) :
    d.support x := by
…

Mentions: OAI.Ostmann.ArithmeticResidueSplit