TransferHistoryUniqueness.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Ostmann.TransferHistorySystem line 12
Source documentation
A state records the current actual labels. Child states insert the reconstructed pivot and retain the corresponding branch.
```
structure TransferHistorySystem (State : Type*) where
…
```
structure OAI.Ostmann.ValidTransferNode line 22
Source documentation
The conditions used by the rigidity argument are all original support conditions or the strict product-range inequality.
```
structure ValidTransferNode {State : Type*} (sys : TransferHistorySystem State)
    (σ : State) (s v w : ℤ) (P : ℕ) : Prop where
…
```
Mentions: OAI.Ostmann.TransferHistorySystem
def OAI.Ostmann.ValidTransferHistory line 34
theorem OAI.Ostmann.validTransferHistory_unique line 44
Source documentation
Inserted ancestor pivots are part of the state. Fixing their value at a node therefore fixes both child states before the induction is applied.
```
theorem validTransferHistory_unique {State : Type*} (sys : TransferHistorySystem State)
    (n : ℕ) (σ : State) (x y : FrequencyTree ℤ n)
    (hx : ValidTransferHistory sys n σ x) (hy : ValidTransferHistory sys n σ y)
    (hroot : frequencyRoot n x = frequencyRoot n y) : x = y := by
…
```
Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.frequencyRoot
theorem OAI.Ostmann.validTransferHistory_root_injective line 69