TrajectoryMoment.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CoordinateSweeps.Grid.Holes.auxCount line 23
theorem OAI.CoordinateSweeps.Grid.Holes.auxCount_sum line 26
theorem OAI.CoordinateSweeps.Grid.Holes.selected_sum line 33
theorem OAI.CoordinateSweeps.Grid.Holes.augment_selected_extraCount line 43
theorem OAI.CoordinateSweeps.Grid.Holes.size_pow_eq_aux_product line 54
def OAI.CoordinateSweeps.Grid.Holes.EndpointPossible line 63
Source comment
Very same endpoint feasibility event as the conditioned finite sample space.
```
def EndpointPossible (H : G.Holes h) (x y : Fin k → G.Slot) (A : Finset (Fin k)) : Prop :=
…
```
theorem OAI.CoordinateSweeps.Grid.Holes.descFactorial_add_split line 66

theorem OAI.CoordinateSweeps.Grid.Holes.scaled_extraProbability_uniform line 77

Source comment

Uniform scaled entries have exactly the falling-factorial moments that enter the shared-line gamma expansion, zero for impossible simultaneous paths.

theorem scaled_extraProbability_uniform (H : G.Holes h) (x y : Fin k → G.Slot)
    (hx : H.ValidInput x) (A : Finset (Fin k)) :
    (G.size : ℝ)^A.card * H.extraProbability x y A (fun _ => FiniteLaw.uniform _) =
      if H.EndpointPossible x y A then
        ∏ j, ∏ L : G.Line j, fallingMoment (2^G.bits j) (H.lineCount j L) (auxCount x y A j L)
      else 0 := by
…

Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.Grid.Holes.auxCount

def OAI.CoordinateSweeps.Grid.Holes.JointDisjoint line 142
Source comment
Geometric validity at EVERY boundary, not only at endpoints.
```
def JointDisjoint (H : G.Holes h) (x y : Fin k → G.Slot) (A : Finset (Fin k)) : Prop :=
…
```

def OAI.CoordinateSweeps.Grid.Holes.adjoin line 148

Source comment

Build the augmented hole family directly from disjoint geometry.

def adjoin (H : G.Holes h) (x y : Fin k → G.Slot) (A : Finset (Fin k))
    (hv : H.JointDisjoint x y A) : G.Holes (h+A.card) where
…

theorem OAI.CoordinateSweeps.Grid.Holes.adjoin_old line 166
theorem OAI.CoordinateSweeps.Grid.Holes.adjoin_new line 170
theorem OAI.CoordinateSweeps.Grid.Holes.feasible_of_disjoint_paths line 177
Source comment
Every geometrically specified hole family already has a positive uniform normalizer, whose proved factorial formula yields a real completion witness.
```
theorem feasible_of_disjoint_paths (H : G.Holes h) : H.Feasible := by
…
```
theorem OAI.CoordinateSweeps.Grid.Holes.adjoin_compatible_iff line 186

theorem OAI.CoordinateSweeps.Grid.Holes.endpointPossible_iff_jointDisjoint line 207

Source comment

Exact event feasibility equals disjointness of the unique full trajectories.

theorem endpointPossible_iff_jointDisjoint (H : G.Holes h) (x y : Fin k → G.Slot)
    (hx : H.ValidInput x) (A : Finset (Fin k)) :
    H.EndpointPossible x y A ↔ H.JointDisjoint x y A := by
…

def OAI.CoordinateSweeps.Grid.Holes.VertexIsolated line 225
Source comment
Precisely the vertex-isolation condition in the source's definition of good.
```
def VertexIsolated (H : G.Holes h) (x y : Fin k → G.Slot) (i : Fin k) : Prop :=
…
```
theorem OAI.CoordinateSweeps.Grid.Holes.jointDisjoint_mono line 229
theorem OAI.CoordinateSweeps.Grid.Holes.jointDisjoint_union_iff line 234

theorem OAI.CoordinateSweeps.Grid.Holes.endpointPossible_union_iff line 254

Source comment

Adding any subset of good paths CANNOT change validity, as needed before alternation is taken inside the shared-line expectation.

theorem endpointPossible_union_iff (H : G.Holes h) (x y : Fin k → G.Slot)
    (hx : H.ValidInput x) (A S : Finset (Fin k))
    (hS : ∀ i ∈ S, H.VertexIsolated x y i) :
    H.EndpointPossible x y (A∪S) ↔ H.EndpointPossible x y A := by
…

abbrev OAI.CoordinateSweeps.Grid.StageLine line 265
Source comment
A line is named by both its stage and its remaining coordinates.
```
abbrev StageLine (G : Grid) := Σ j : Fin G.b, G.Line j
```
Mentions: OAI.CoordinateSweeps.Grid
def OAI.CoordinateSweeps.Grid.stagePath line 267
theorem OAI.CoordinateSweeps.Grid.Holes.incidenceCount_stagePath line 274
theorem OAI.CoordinateSweeps.Grid.Holes.incidenceCount_stagePath_any line 288
theorem OAI.CoordinateSweeps.Grid.Holes.incidenceCount_total line 294
def OAI.CoordinateSweeps.Grid.Holes.Light line 300
def OAI.CoordinateSweeps.Grid.Holes.Good line 304
def OAI.CoordinateSweeps.Grid.Holes.goodSet line 307
theorem OAI.CoordinateSweeps.Grid.Holes.mem_goodSet line 310
def OAI.CoordinateSweeps.Grid.Holes.lightMoment line 313
theorem OAI.CoordinateSweeps.Grid.Holes.lightMoment_zero line 316
theorem OAI.CoordinateSweeps.Grid.Holes.incidenceCount_good_nonlight line 319
theorem OAI.CoordinateSweeps.Grid.Holes.incidenceCount_mono line 331
theorem OAI.CoordinateSweeps.Grid.Holes.incidenceCount_union line 336

theorem OAI.CoordinateSweeps.Grid.Holes.goodExpansion_lightMoment_le line 344

Source comment

The actual shared-line moment bound: inactive (non-light) line variables are set to 1, not made independent per particle.

theorem goodExpansion_lightMoment_le (H : G.Holes h) (x y : Fin k → G.Slot)
    {η : ℝ} (hη : 0 ≤ η) (hηsmall : η ≤ 1/8) (J : Finset (Fin k))
    (hJ : Disjoint J (H.goodSet x y η)) :
    |shiftedMoment (H.lightMoment x y η) (incidenceCount J (G.stagePath x y))
      (goodExpansion (H.goodSet x y η) (G.stagePath x y))| ≤
      (16 * Real.exp 2)^(G.b*J.card) * (1+16 * Real.exp 2)^(G.b*(H.goodSet x y η).card) *
        η^(((H.goodSet x y η).card : ℝ)/2) := by
…

theorem OAI.CoordinateSweeps.MomentExpansion.fallingMoment_one_le line 394
theorem OAI.CoordinateSweeps.Grid.Holes.endpointPossible_lineCount_le line 409
def OAI.CoordinateSweeps.Grid.Holes.nonlightFactor line 423
Source comment
Product outside the light-line expectation; zero validity is handled separately, never by interpreting a divergent inverse-gamma moment.
```
def nonlightFactor (H : G.Holes h) (x y : Fin k → G.Slot) (η : ℝ) (J : Finset (Fin k)) : ℝ :=
…
```
theorem OAI.CoordinateSweeps.Grid.Holes.nonlightFactor_nonneg line 427
theorem OAI.CoordinateSweeps.Grid.Holes.nonlightFactor_le line 435

theorem OAI.CoordinateSweeps.Grid.Holes.scaled_extraProbability_good_union line 462

Source comment

Exact factorization for adding any collection of good paths.

theorem scaled_extraProbability_good_union (H : G.Holes h) (x y : Fin k → G.Slot)
    (hx : H.ValidInput x) (η : ℝ) (J S : Finset (Fin k))
    (hJ : Disjoint J (H.goodSet x y η)) (hS : S ⊆ H.goodSet x y η) :
    (G.size : ℝ)^(J∪S).card * H.extraProbability x y (J∪S) (fun _ => FiniteLaw.uniform _) =
      (if H.EndpointPossible x y J then H.nonlightFactor x y η J else 0) *
        ∏ l : G.StageLine, H.lightMoment x y η l
          (incidenceCount J (G.stagePath x y) l+incidenceCount S (G.stagePath x y) l) := by
…

Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform

theorem OAI.CoordinateSweeps.sum_powerset_union line 495
theorem OAI.CoordinateSweeps.sum_powerset_sdiff line 553
theorem OAI.CoordinateSweeps.alternating_good_split line 571
theorem OAI.CoordinateSweeps.Grid.Holes.alternating_good_extensions line 605

theorem OAI.CoordinateSweeps.Grid.Holes.scaled_placementKernel_good_bound line 623

Source comment

Source04:eq10, now proved for literal uniform stage-line laws and actual conditioned path probabilities. Constants are explicit and absolute; all non-light factors and validity indicators remain outside the moment.

theorem scaled_placementKernel_good_bound (H : G.Holes h) (x y : Fin k → G.Slot)
    (hx : H.ValidInput x) {η : ℝ} (hη : 0 ≤ η) (hηsmall : η ≤ 1/8) :
    |(G.size : ℝ)^k * H.placementKernel x y (fun _ => FiniteLaw.uniform _)| ≤
      (2 : ℝ)^k * Real.exp ((G.b : ℝ)*(h+k)+Real.log 4*k*G.b) *
        (16*Real.exp 2)^(G.b*k) * (1+16*Real.exp 2)^(G.b*k) *
          η^(((H.goodSet x y η).card : ℝ)/2) := by
…

Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform