RationalQuartetValue.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Bottom quartets in the actual rational-tree recursion

theorem OAI.Ostmann.rationalTreeFrequency_cast line 11
theorem OAI.Ostmann.rationalTreeAmplitude_cast line 17
structure OAI.Ostmann.RationalQuartetData line 27
Source documentation
The fixed data above a bottom quartet; its four leaf products remain free.
```
structure RationalQuartetData (U : Type*) [CommGroup U] where
…
```
def OAI.Ostmann.RationalQuartetData.tree line 47
def OAI.Ostmann.rationalQuartetValue line 55

theorem OAI.Ostmann.rationalTreeAmplitude_quartet line 70

Source documentation

This local value is the depth-two instance of the same tree amplitude used in the global cycle projection, rather than a new surrogate diagram.

theorem rationalTreeAmplitude_quartet {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
    (XL XR m₁ m₂ m₃ m₄ : (ZMod p)ˣ) :
    rationalTreeAmplitude g D Q.tree XL XR ((false, true), (false, true))
      ((m₁, m₂), (m₃, m₄)) = rationalQuartetValue g D Q XL XR m₁ m₂ m₃ m₄ := by
…

Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.rationalQuartetValue