OAI/Dynamics/TriangleBilliards/FlightUniqueness.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.FlightChain.initial_line line 12
2. lemma OAI.TriangularBilliards.FlightChain.previous_line line 17
3. def OAI.TriangularBilliards.FlightChain.Agree line 27

   Source documentation

   Agreement of the four data fields at a collision; the proof fields are proposition-valued and need no extra equality assumptions.

   def Agree {Q : Triangle} {z : Phase} (c d : FlightChain Q z) (n : ℤ) : Prop :=
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.FlightChain

4. lemma OAI.TriangularBilliards.FlightChain.agree_zero line 31
5. lemma OAI.TriangularBilliards.FlightChain.agree_succ line 56
6. lemma OAI.TriangularBilliards.FlightChain.agree_pred line 83
7. theorem OAI.TriangularBilliards.FlightChain.unique line 130

   Source documentation

   Determinism of actual complete nonsingular specular trajectories. Both forward and backward schemes use the same geometric reflection and never postulate uniqueness as an assumption.

   theorem unique {Q : Triangle} {z : Phase} (c d : FlightChain Q z) : c = d := by
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.FlightChain

8. def OAI.TriangularBilliards.FlightChain.rebase line 151

   Source documentation

   Rebase a complete chain at a time strictly between its collisions. The integer relabeling is forced by the designated initial flight.

   def rebase {Q : Triangle} {z : Phase} (c : FlightChain Q z)
       (t : ℝ) (n : ℤ) (hn : c.time n < t ∧ t < c.time (n + 1)) :
       FlightChain Q (c.at t) where
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.FlightChain

9. lemma OAI.TriangularBilliards.FlightChain.rebase_at line 195
10. lemma OAI.TriangularBilliards.billiardFlow_eq_chain line 211
11. lemma OAI.TriangularBilliards.billiardFlow_add_of_noncollision line 222

    Source documentation

    The exact cocycle identity on every rebased nonsingular trajectory. Only rebasing at a collision is excluded, since Phase itself uses interior initial states; the main theorem still needs the fixed-time exceptional sets to be proved null.

    lemma billiardFlow_add_of_noncollision {Q : Triangle} {z : Phase}
        (c : FlightChain Q z) (s t : ℝ) (ht : t ∉ range c.time) :
        billiardFlow Q (s + t) z = billiardFlow Q s (billiardFlow Q t z) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.FlightChain, OAI.TriangularBilliards.billiardFlow