Model.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The phase space is represented in the ambient plane × circle, with measure supported on the interior of the triangle. Values on side-collision states at a fixed time are immaterial to the modulo-null-set conclusion. The trajectories themselves include the collisions and impose specular reflection.

structure OAI.TriangularBilliards.Triangle line 20
Source documentation
Three affinely independent vertices in the Euclidean plane.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:20 (same declaration text).
```
structure Triangle where
…
```
def OAI.TriangularBilliards.Triangle.table line 27
Source documentation
The open table; the complex plane carries its ordinary real Euclidean metric.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:27 (same declaration text).
```
def table (Q : Triangle) : Set ℂ := interior (convexHull ℝ (range Q.vertex))
```
Mentions: OAI.TriangularBilliards.Triangle
def OAI.TriangularBilliards.Triangle.side line 30
Source documentation
The open side from vertex i to the next vertex, indexed cyclically.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:30 (same declaration text).
```
def side (Q : Triangle) (i : Fin 3) : Set ℂ :=
…
```
Mentions: OAI.TriangularBilliards.Triangle
def OAI.TriangularBilliards.Triangle.tangent line 34
Source documentation
A tangent vector to side i, with no choice of inward or outward normal.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:34 (same declaration text).
```
def tangent (Q : Triangle) (i : Fin 3) : ℂ := Q.vertex (i + 1) - Q.vertex i
```
Mentions: OAI.TriangularBilliards.Triangle
def OAI.TriangularBilliards.Triangle.angle line 37
Source documentation
Interior angle at vertex i.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:37 (same declaration text).
```
def angle (Q : Triangle) (i : Fin 3) : ℝ :=
…
```
Mentions: OAI.TriangularBilliards.Triangle
def OAI.TriangularBilliards.Triangle.HasIrrationalAngle line 41
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:41 (same declaration text).
def OAI.TriangularBilliards.reflect line 49
Source documentation
Reflection in the real line spanned by the nonzero tangent e. In coordinates with e real this is complex conjugation, preserving the tangential component and reversing the normal component.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:49 (same declaration text).
```
def reflect (e v : ℂ) : ℂ := (e / star e) * star v
```
instance OAI.TriangularBilliards.circleMeasurableSpace line 51
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:51 (same declaration text).
instance OAI.TriangularBilliards.circleBorelSpace line 53
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:53 (same declaration text).
abbrev OAI.TriangularBilliards.Phase line 55
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:55 (same declaration text).
structure OAI.TriangularBilliards.FlightChain line 61
Source documentation
A complete nonsingular billiard trajectory, indexed by its collisions. Flight zero contains the initial time strictly. Both ends of the collision time sequence are unbounded; collisions occur only in open sides, never vertices. These are geometric conditions, not ergodicity/analytic assumptions.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:61 (same declaration text).
```
structure FlightChain (Q : Triangle) (z : Phase) where
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase
def OAI.TriangularBilliards.FlightChain.at line 82
Source documentation
The geometric state on a chain, using outgoing velocity at a collision.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:82 (same declaration text).
```
def FlightChain.at {Q : Triangle} {z : Phase} (c : FlightChain Q z) (t : ℝ) : Phase := by
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.FlightChain
def OAI.TriangularBilliards.billiardFlow line 92
Source documentation
The actual specular flow on complete regular chains. Singular initial states are assigned their initial state; the theorem must prove these form a null set. No nonemptiness of the regular set is postulated.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:92 (same declaration text).
```
def billiardFlow (Q : Triangle) (t : ℝ) (z : Phase) : Phase := by
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase
def OAI.TriangularBilliards.angularMeasure line 97
Source documentation
Uniform angular probability, parameterized by [0,2π).
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:97 (same declaration text).
```
def angularMeasure : Measure Circle :=
…
```
def OAI.TriangularBilliards.phaseMeasure line 102
Source documentation
Exactly normalized area in the open table times uniform angular measure.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:102 (same declaration text).
```
def phaseMeasure (Q : Triangle) : Measure Phase :=
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase
def OAI.TriangularBilliards.MainConclusion line 108
Source documentation
The main conclusion, together with the geometric/nonvacuity guarantees needed by the concrete definition of the actual two-sided billiard.
Also declared: ComparatorChallenges/IrrationalTriangleBilliard.lean:108 (same declaration text).
```
def MainConclusion (Q : Triangle) : Prop :=
…
```
Mentions: OAI.TriangularBilliards.Triangle