BranchingHistoryIntegrality.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Ostmann.BranchingWordHistory.updatedFormula_integral_iff line 14
theorem OAI.Ostmann.BranchingWordHistory.pivotFormulas_integral_iff line 28
Source documentation
The full branching support has precisely one constructed integrality test for each internal node. Child branches are evaluated independently.
```
theorem pivotFormulas_integral_iff (history : BranchingWordHistory σ)
    (env : σ → HistoryFormula σ) (a x : σ → ℤ)
    (he : ∀ i, (env i).value (fun j => (a j : ℚ)) = x i) :
    (∀ F ∈ history.pivotFormulas env, F.IntegralAt a) ↔ history.Valid x := by
…
```
Mentions: OAI.Ostmann.BranchingWordHistory, OAI.Ostmann.HistoryFormula
theorem OAI.Ostmann.BranchingWordHistory.branching_integer_polynomial_tests line 48
Source documentation
In the initial prime environment the gate is an explicit divisibility of integer polynomial values by the constructed nonzero denominators.
```
theorem branching_integer_polynomial_tests (history : BranchingWordHistory σ) (x : σ → ℤ) :
    history.Valid x ↔ ∀ F ∈ history.pivotFormulas .prime,
      F.cleared.denominator ∣ MvPolynomial.eval₂Hom (RingHom.id ℤ) x F.cleared.numerator := by
…
```
Mentions: OAI.Ostmann.BranchingWordHistory