Main.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalGramIdentity line 13
Source documentation
The collected mixed polynomial is the genuine nonnegative Gram expression.
```
theorem originalGramIdentity (B : Fin 7 → Basis) (hB : IsMUBFamily B) :
    Integer.Sparse.eval originalPolynomial (originalVector B) =
      GramNonnegative.sourceGram B := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Certificate.Integer.Sparse.eval, OAI.MUB6.Certificate.MixedTargetSemantics.originalPolynomial, OAI.MUB6.Certificate.MixedTargetSemantics.originalVector, OAI.MUB6.Certificate.GramNonnegative.sourceGram
theorem OAI.MUB6.Certificate.MixedTargetSemantics.rawGramIdentity line 25
Source documentation
The exact integer target has the manuscript's Gram interpretation, including both its factor of five and its common integer denominator.
```
theorem rawGramIdentity (B : Fin 7 → Basis) (hB : IsMUBFamily B)
    (hF : AllTransitionsFourierZero B) :
    Integer.Combination.eval MixedData.targetRows (numericVector B) MixedData.rawCombination =
      (MixedData.denominator : ℝ) * GramNonnegative.sourceGram B := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.AllTransitionsFourierZero, OAI.MUB6.Certificate.Integer.Combination.eval, OAI.MUB6.Certificate.MixedData.targetRows, OAI.MUB6.Certificate.MixedData.rawCombination, OAI.MUB6.Certificate.MixedData.denominator, OAI.MUB6.Certificate.GramNonnegative.sourceGram