OAI/NumberTheory/Ostmann/Arithmetic/RecursiveNodeExpansion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.ReconstructedTransferNode line 11
2. def OAI.Ostmann.ReconstructedTransferNode.pivot line 19
3. def OAI.Ostmann.ReconstructedTransferNode.Valid line 23
4. def OAI.Ostmann.transferNodeList line 29
5. theorem OAI.Ostmann.transferNodeList_length line 38
6. theorem OAI.Ostmann.validTransferHistory_reconstructed_iff line 51

   Source documentation

   The pivot witness in the original definition is precisely the integer reconstruction, so no existential choice changes the child states.

   theorem validTransferHistory_reconstructed_iff {State : Type*}
       (sys : TransferHistorySystem State) (n : ℕ) (σ : State) (t : FrequencyTree ℤ (n + 1)) :
       ValidTransferHistory sys (n + 1) σ t ↔
         let P := historyPivot sys σ t.1 (frequencyRoot n t.2.1) (frequencyRoot n t.2.2)
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.historyPivot, OAI.Ostmann.frequencyRoot

7. theorem OAI.Ostmann.validTransferHistory_nodeList_iff line 67

   Source documentation

   All arithmetic support conditions in a complete history are the tests of its explicitly reconstructed preorder node list.

   theorem validTransferHistory_nodeList_iff {State : Type*}
       (sys : TransferHistorySystem State) (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) :
       ValidTransferHistory sys n σ t ↔ ∀ node ∈ transferNodeList sys n σ t, node.Valid sys := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.transferNodeList