OAI/NumberTheory/Ostmann/Construction/BranchingHistoryReplay.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Ostmann.BranchingWordHistory line 9
  2. def OAI.Ostmann.BranchingWordHistory.Valid line 17
  3. def OAI.Ostmann.BranchingWordHistory.flipSigned line 22
  4. def OAI.Ostmann.BranchingWordHistory.mapSigned line 24
  5. def OAI.Ostmann.BranchingWordHistory.integerLeaves line 26
  6. def OAI.Ostmann.BranchingWordHistory.updatedFormulas line 32
  7. def OAI.Ostmann.BranchingWordHistory.formulaLeaves line 36
  8. def OAI.Ostmann.BranchingWordHistory.pivotFormulas line 43
  9. theorem OAI.Ostmann.BranchingWordHistory.wordFormula_value line 51
  10. theorem OAI.Ostmann.BranchingWordHistory.updatedFormulas_value line 66
  11. theorem OAI.Ostmann.BranchingWordHistory.mapSigned_flip line 80
  12. theorem OAI.Ostmann.BranchingWordHistory.formulaLeaves_value line 87

    Source documentation

    Every signed leaf formula evaluates to its actual product after all ancestor integer substitutions, including the independently replayed right branch.

    theorem formulaLeaves_value (history : BranchingWordHistory σ) (env : σ → HistoryFormula σ)
    (a : σ → ℚ) (x : σ → ℤ) (he : ∀ i, (env i).value a = x i) (hx : history.Valid x) :
    (history.formulaLeaves env).map (mapSigned (fun F => F.value a)) =
      (history.integerLeaves x).map (mapSigned (fun z : ℤ => (z : ℚ))) := by
…

    Mentions: OAI.Ostmann.BranchingWordHistory, OAI.Ostmann.HistoryFormula, OAI.Ostmann.BranchingWordHistory.mapSigned

  13. def OAI.Ostmann.BranchingWordHistory.leafCount line 101

    Source documentation

    Counts use the original branching structure, independent of assignments.

    def leafCount : BranchingWordHistory σ → ℕ
  | .leaf _ => 1
  | .node _ left right => left.leafCount + right.leafCount

    Mentions: OAI.Ostmann.BranchingWordHistory

  14. def OAI.Ostmann.BranchingWordHistory.nodeCount line 105
  15. theorem OAI.Ostmann.BranchingWordHistory.formulaLeaves_length line 109
  16. theorem OAI.Ostmann.BranchingWordHistory.pivotFormulas_length line 115