Kernel.lean`

80 declarations, 0 contain sorry, 0 declared as axioms

All definitions are finite and use the source's ordinary probability and trace normalizations.

def OAI.CoordinateSweeps.Grid.pathBetween line 25
Source comment
The unique auxiliary trajectory joining two slots.
```
def pathBetween (x y : G.Slot) (t : Fin (G.b+1)) : G.Slot :=
…
```
theorem OAI.CoordinateSweeps.Grid.pathBetween_zero line 28
theorem OAI.CoordinateSweeps.Grid.pathBetween_last line 32
theorem OAI.CoordinateSweeps.Grid.pathBetween_input line 37
theorem OAI.CoordinateSweeps.Grid.pathBetween_output line 41
theorem OAI.CoordinateSweeps.Grid.pathBetween_step line 45
def OAI.CoordinateSweeps.Grid.pathLine line 53
Source comment
The stage-decorated line used by the auxiliary trajectory.
```
def pathLine (x y : G.Slot) (j : Fin G.b) : G.Line j :=
…
```
def OAI.CoordinateSweeps.Grid.endpointEvent line 58
Source comment
Endpoint events are equivalent to the unique additional trajectory's line assignments. No feasibility or injectivity is postulated.
```
def endpointEvent {k : ℕ} (x y : Fin k → G.Slot) (A : Finset (Fin k))
    (ω : G.Choices) : Prop := ∀ i ∈ A, G.sweep ω (x i) = y i
```
def OAI.CoordinateSweeps.Grid.extraLineEvent line 62
Source comment
A direct finite constraint event on one line for the extra particles.
```
def extraLineEvent {k : ℕ} (x y : Fin k → G.Slot) (A : Finset (Fin k))
    (j : Fin G.b) (L : G.Line j) (σ : Equiv.Perm (Cube (G.bits j))) : Prop :=
…
```
Mentions: OAI.CoordinateSweeps.Cube
def OAI.CoordinateSweeps.Grid.Holes.localExtraProbability line 70
Source comment
Exact one-line probability after the hole assignments are prescribed.
```
def localExtraProbability (H : G.Holes h) (x y : Fin k → G.Slot)
    (A : Finset (Fin k)) (j : Fin G.b) (L : G.Line j)
    (μ : FiniteLaw (Equiv.Perm (Cube (G.bits j)))) : ℝ :=
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube
def OAI.CoordinateSweeps.Grid.Holes.extraProbability line 78
Source comment
Product form of the exact conditional endpoint probability. The bridge to the original conditioned sweep event is proved below, not assumed.
```
def extraProbability (H : G.Holes h) (x y : Fin k → G.Slot)
    (A : Finset (Fin k)) (μ : ∀ j : Fin G.b, FiniteLaw (Equiv.Perm (Cube (G.bits j)))) : ℝ :=
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube
def OAI.CoordinateSweeps.Grid.Holes.placementKernel line 84
Source comment
The path-weight alternating placement matrix Q, with counting measure and s, not s-h, in its normalization, exactly as 04-sparse:eq7.
```
def placementKernel (H : G.Holes h) (x y : Fin k → G.Slot)
    (μ : ∀ j : Fin G.b, FiniteLaw (Equiv.Perm (Cube (G.bits j)))) : ℝ :=
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube
def OAI.CoordinateSweeps.Grid.Holes.LineIsolated line 91
Source comment
A line-isolated additional trajectory, relative to all other additional paths AND the prescribed holes. Stage indices are never conflated.
```
def LineIsolated (H : G.Holes h) (x y : Fin k → G.Slot) (i : Fin k) : Prop :=
…
```
theorem OAI.CoordinateSweeps.Grid.Holes.lineCompatible_of_empty line 96
theorem OAI.CoordinateSweeps.Grid.Holes.localExtraProbability_no_paths line 102
theorem OAI.CoordinateSweeps.Grid.Holes.extraLineEvent_insert line 113
def OAI.CoordinateSweeps.Grid.Holes.OneCardUniform line 123
Source comment
The source's one-card marginal property, stated for a line law. This is proved for both U and the actual binary law below, not a main-proof assumption.
```
def OneCardUniform {d : ℕ} (μ : FiniteLaw (Equiv.Perm (Cube d))) : Prop :=
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube
theorem OAI.CoordinateSweeps.Grid.Holes.extraLineEvent_insert_off line 126
theorem OAI.CoordinateSweeps.Grid.Holes.localExtraProbability_insert_off line 134
theorem OAI.CoordinateSweeps.Grid.Holes.localExtraProbability_isolated_insert line 142
theorem OAI.CoordinateSweeps.Grid.Holes.stageExtraProbability_isolated_insert line 157
theorem OAI.CoordinateSweeps.Grid.Holes.extraProbability_isolated_insert line 178

lemma OAI.CoordinateSweeps.Grid.Holes.alternating_cancel line 192

Source comment

Elementary pairing identity for the alternating sum.

lemma alternating_cancel {ι : Type*} [DecidableEq ι] (s : Finset ι) (i : ι) (hi : i ∈ s)
    (P : Finset ι → ℝ)
    (hP : ∀ A ⊆ s.erase i, P (insert i A) = P A) :
    ∑ A ∈ s.powerset, (-1 : ℝ) ^ A.card * P A = 0 := by
…

theorem OAI.CoordinateSweeps.Grid.Holes.placementKernel_eq_zero_of_isolated line 212
Source comment
Isolated-path cancellation for the actual product conditional kernel. There is no independence assumption between auxiliary particle factors.
```
theorem placementKernel_eq_zero_of_isolated (H : G.Holes h) (x y : Fin k → G.Slot)
    (i : Fin k) (his : H.LineIsolated x y i)
    (μ : ∀ j : Fin G.b, FiniteLaw (Equiv.Perm (Cube (G.bits j))))
    (hμ : ∀ j, OneCardUniform (μ j)) : H.placementKernel x y μ = 0 := by
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube, OAI.CoordinateSweeps.Grid.Holes.OneCardUniform
theorem OAI.CoordinateSweeps.Grid.boundary_coordinate_before line 252
theorem OAI.CoordinateSweeps.Grid.boundary_coordinate_stable line 263
theorem OAI.CoordinateSweeps.Grid.boundary_eq_pathBetween line 275

theorem OAI.CoordinateSweeps.Grid.sweep_eq_iff_line_assignments line 284

Source comment

Actual endpoint events are exactly the auxiliary path constraints.

theorem sweep_eq_iff_line_assignments (ω : G.Choices) (x y : G.Slot) :
    G.sweep ω x = y ↔
      ∀ j, ω j (G.pathLine x y j) (x j) = y j := by
…

theorem OAI.CoordinateSweeps.Grid.endpointEvent_iff_lines line 324

theorem OAI.CoordinateSweeps.sum_prod_ite_all line 341

Source comment

Finite independence, keeping an arbitrary local constraint at every factor.

theorem sum_prod_ite_all {ι : Type*} [Fintype ι] [DecidableEq ι]
    {X : ι → Type*} [∀ i, Fintype (X i)]
    (w : ∀ i, X i → ℝ) (P : ∀ i, X i → Prop) :
    (∑ x : ∀ i, X i, if ∀ i, P i (x i) then ∏ i, w i (x i) else 0) =
      ∏ i, ∑ y, if P i y then w i y else 0 := by
…

def OAI.CoordinateSweeps.Grid.productLineMass line 360
theorem OAI.CoordinateSweeps.Grid.sum_productLineMass_event line 364
def OAI.CoordinateSweeps.Grid.Holes.conditionalEndpointProbability line 387
Source comment
Conditional probability of an endpoint specification, from the original independent line sample space; the full trajectories of the holes are retained.
```
def conditionalEndpointProbability (H : G.Holes h) (x y : Fin k → G.Slot)
    (A : Finset (Fin k))
    (μ : ∀ j : Fin G.b, FiniteLaw (Equiv.Perm (Cube (G.bits j)))) : ℝ :=
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube
theorem OAI.CoordinateSweeps.Grid.Holes.extraProbability_eq_conditionalEndpoint line 395
Source comment
The kernel's product formula really is the conditioned sweep probability; no independence of different layers of the auxiliary paths is used.
```
theorem extraProbability_eq_conditionalEndpoint (H : G.Holes h) (x y : Fin k → G.Slot)
    (A : Finset (Fin k))
    (μ : ∀ j : Fin G.b, FiniteLaw (Equiv.Perm (Cube (G.bits j)))) :
    H.extraProbability x y A μ = H.conditionalEndpointProbability x y A μ := by
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube
theorem OAI.CoordinateSweeps.Grid.Holes.lineMass_hole_normalizer line 429
Source comment
At the source law, the denominator in the direct event formula is exactly the source normalizer (with all prescribed paths, not just endpoints).
```
theorem lineMass_hole_normalizer (H : G.Holes h) {z : ℝ}
    (hz : 0 ≤ z) (hz' : z ≤ 1) :
    (∑ ω, if H.Compatible ω then
      G.productLineMass (fun j => lineLaw (G.bits j) z hz hz') ω else 0) =
      H.probability z := by
…
```
Mentions: OAI.CoordinateSweeps.lineLaw
def OAI.CoordinateSweeps.binaryBoundary line 443
theorem OAI.CoordinateSweeps.binaryBoundary_zero line 446
theorem OAI.CoordinateSweeps.binaryBoundary_last line 449
theorem OAI.CoordinateSweeps.binaryBoundary_succ line 454
theorem OAI.CoordinateSweeps.binaryLayer_apply_same line 460
theorem OAI.CoordinateSweeps.binaryLayer_apply_ne line 465
def OAI.CoordinateSweeps.binaryPath line 470
def OAI.CoordinateSweeps.binaryPathLine line 473
theorem OAI.CoordinateSweeps.binaryPath_zero line 476
theorem OAI.CoordinateSweeps.binaryPath_last line 479
theorem OAI.CoordinateSweeps.binaryBoundary_before line 482
theorem OAI.CoordinateSweeps.binaryBoundary_stable line 493
theorem OAI.CoordinateSweeps.binaryBoundary_eq_path line 505
theorem OAI.CoordinateSweeps.binarySweep_eq_iff_coins line 514
theorem OAI.CoordinateSweeps.FiniteLaw.uniform_pi line 563
Source comment
Independent uniform choices coincide with the uniform law on a finite product, including dependent factors.
```
theorem uniform_pi {ι : Type*} [Fintype ι] [DecidableEq ι]
    {X : ι → Type*} [∀ i, Fintype (X i)] [∀ i, Nonempty (X i)] :
    uniform (∀ i, X i) = independent (fun i => uniform (X i)) := by
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.FiniteLaw.independent

theorem OAI.CoordinateSweeps.FiniteLaw.uniform_eval line 571

Source comment

One specified coordinate of a uniform random function is uniform.

theorem uniform_eval {A B : Type*} [Fintype A] [DecidableEq A] [Fintype B]
    [Nonempty B] (a : A) (b : B) :
    (∑ f : A → B, if f a = b then uniform (A → B) f else 0) =
      (Fintype.card B : ℝ)⁻¹ := by
…

Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.FiniteLaw.uniform

theorem OAI.CoordinateSweeps.FiniteLaw.map_event line 588

Source comment

Exact pushforward probability identity.

theorem map_event {A B : Type*} [Fintype A] [Fintype B]
    (μ : FiniteLaw A) (f : A → B) (P : B → Prop) :
    (∑ b, if P b then μ.map f b else 0) = ∑ a, if P (f a) then μ a else 0 := by
…

Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.a

theorem OAI.CoordinateSweeps.binaryLaw_one_card line 611
Source comment
The actual fair-switch binary sweep sends every given slot uniformly. In particular this is not imported as a hypothesis on the line law.
```
theorem binaryLaw_one_card (d : ℕ) (x y : Cube d) :
    (∑ σ, if σ x = y then binaryLaw d σ else 0) = (2^d : ℝ)⁻¹ := by
…
```
Mentions: OAI.CoordinateSweeps.Cube, OAI.CoordinateSweeps.binaryLaw
theorem OAI.CoordinateSweeps.uniformLaw_one_card line 645
Source comment
The uniform permutation law has the same exact one-card marginal.
```
theorem uniformLaw_one_card (d : ℕ) (x y : Cube d) :
    (∑ σ : Equiv.Perm (Cube d), if σ x = y then FiniteLaw.uniform _ σ else 0) =
      (2^d : ℝ)⁻¹ := by
…
```
Mentions: OAI.CoordinateSweeps.Cube, OAI.CoordinateSweeps.FiniteLaw.uniform
theorem OAI.CoordinateSweeps.lineLaw_one_card line 668
Source comment
No auxiliary marginal hypothesis remains: this is the manuscript's real line law, including either endpoint value of the mixture parameter.
```
theorem lineLaw_one_card (d : ℕ) (z : ℝ) (hz : 0 ≤ z) (hz' : z ≤ 1) :
    Grid.Holes.OneCardUniform (lineLaw d z hz hz') := by
…
```
Mentions: OAI.CoordinateSweeps.Grid.Holes.OneCardUniform, OAI.CoordinateSweeps.lineLaw

theorem OAI.CoordinateSweeps.Grid.Holes.placementKernel_lineLaw_eq_zero_of_isolated line 687

Source comment

Isolated-path cancellation, now for the literal conditioned sweep law.

theorem Grid.Holes.placementKernel_lineLaw_eq_zero_of_isolated
    {G : Grid} {h k : ℕ} (H : G.Holes h) (x y : Fin k → G.Slot)
    (i : Fin k) (his : H.LineIsolated x y i)
    (z : ℝ) (hz : 0 ≤ z) (hz' : z ≤ 1) :
    H.placementKernel x y (fun j => lineLaw (G.bits j) z hz hz') = 0 := by
…

Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.lineLaw

def OAI.CoordinateSweeps.Grid.spliceEquiv line 704

theorem OAI.CoordinateSweeps.Grid.sum_pathBetween line 713

Source comment

Exact counting identity for one layer of an independent endpoint pair.

theorem sum_pathBetween (t : Fin (G.b+1)) (f : G.Slot → ℝ) :
    (∑ p : G.Slot × G.Slot, f (G.pathBetween p.1 p.2 t)) =
      (G.size : ℝ) * ∑ x : G.Slot, f x := by
…

theorem OAI.CoordinateSweeps.Grid.sum_slot_line line 725

Source comment

A uniform slot chooses each stage-line with probability m_j/s.

theorem sum_slot_line (j : Fin G.b) (L : G.Line j) (c : ℝ) :
    (∑ x : G.Slot, if (fun k : {k : Fin G.b // k ≠ j} => x k) = L then c else 0) =
      (2^G.bits j : ℝ) * c := by
…

Mentions: OAI.CoordinateSweeps.c

def OAI.CoordinateSweeps.Grid.endpointWeight line 740
Source comment
Uniform product weight on the full pair of endpoints, with replacement.
```
def endpointWeight (p : G.Slot × G.Slot) : ℝ := FiniteLaw.uniform _ p
```
Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform
theorem OAI.CoordinateSweeps.Grid.endpointWeight_nonneg line 742
theorem OAI.CoordinateSweeps.Grid.endpointWeight_total line 745

theorem OAI.CoordinateSweeps.Grid.probability_path_vertex line 748

Source comment

A single fixed vertex-sharing event has exact probability 1/s.

theorem probability_path_vertex (t : Fin (G.b+1)) (v : G.Slot) :
    (∑ p : G.Slot × G.Slot, if G.pathBetween p.1 p.2 t = v then G.endpointWeight p else 0) =
      (G.size : ℝ)⁻¹ := by
…

theorem OAI.CoordinateSweeps.Grid.probability_path_line line 766

Source comment

A single stage-line-sharing event has exact probability m_j/s.

theorem probability_path_line (j : Fin G.b) (L : G.Line j) :
    (∑ p : G.Slot × G.Slot, if G.pathLine p.1 p.2 j = L then G.endpointWeight p else 0) =
      (2^G.bits j : ℝ) / G.size := by
…

theorem OAI.CoordinateSweeps.Coverage.sum_ite_exists_le line 790

Source comment

The union bound on a single finite random datum.

theorem sum_ite_exists_le {X J : Type*} [Fintype X] [Fintype J]
    (w : X → ℝ) (hw : ∀ x, 0 ≤ w x) (P : J → X → Prop) :
    (∑ x, if ∃ j, P j x then w x else 0) ≤ ∑ j, ∑ x, if P j x then w x else 0 := by
…

def OAI.CoordinateSweeps.Grid.lineShares line 812
Source comment
Sharing means using the same decorated line at the same stage.
```
def lineShares (p q : G.Slot × G.Slot) : Prop :=
…
```
def OAI.CoordinateSweeps.Grid.vertexShares line 816
Source comment
Vertex sharing means the same slot at one fixed stage boundary.
```
def vertexShares (p q : G.Slot × G.Slot) : Prop :=
…
```
theorem OAI.CoordinateSweeps.Grid.lineShares_symm line 819
theorem OAI.CoordinateSweeps.Grid.vertexShares_symm line 823
def OAI.CoordinateSweeps.Grid.lineSharingRate line 827
def OAI.CoordinateSweeps.Grid.vertexSharingRate line 829
theorem OAI.CoordinateSweeps.Grid.lineSharingRate_nonneg line 831
theorem OAI.CoordinateSweeps.Grid.vertexSharingRate_nonneg line 836
theorem OAI.CoordinateSweeps.Grid.probability_lineShares_le line 840
theorem OAI.CoordinateSweeps.Grid.probability_vertexShares_le line 854
def OAI.CoordinateSweeps.Grid.Holes.endpointData line 873
Source comment
Keep the actual prescribed hole paths, recording their endpoints.
```
def endpointData (H : G.Holes h) (i : Fin h) : G.Slot × G.Slot :=
…
```
theorem OAI.CoordinateSweeps.Grid.Holes.path_eq_pathBetween line 878
Source comment
The source's feasibility ensures these endpoints reconstruct the entire prescribed trajectory, not merely an unrelated bridge between its endpoints.
```
theorem path_eq_pathBetween (H : G.Holes h) (hH : H.Feasible)
    (i : Fin h) (t : Fin (G.b+1)) :
    H.path i t = G.pathBetween (H.endpointData i).1 (H.endpointData i).2 t := by
…
```
theorem OAI.CoordinateSweeps.Grid.Holes.lineIsolated_of_not_covered line 890
Source comment
A card not covered by any line-sharing has exactly the isolation property needed for the alternating probability kernel.
```
theorem lineIsolated_of_not_covered (H : G.Holes h) (hH : H.Feasible)
    (x : Fin k → G.Slot × G.Slot) (i : Fin k)
    (hi : i ∉ Coverage.sharingCoverage G.lineShares H.endpointData x) :
    H.LineIsolated (fun a => (x a).1) (fun a => (x a).2) i := by
…
```
Mentions: OAI.CoordinateSweeps.Coverage.sharingCoverage, OAI.CoordinateSweeps.a

theorem OAI.CoordinateSweeps.Grid.Holes.placementKernel_ne_zero_coverage line 912

Source comment

Nonzero Q entries require coverage of every auxiliary particle, for the literal real line mixture and full feasible path conditioning.

theorem placementKernel_ne_zero_coverage (H : G.Holes h) (hH : H.Feasible)
    (x : Fin k → G.Slot × G.Slot) (z : ℝ) (hz : 0 ≤ z) (hz' : z ≤ 1)
    (hQ : H.placementKernel (fun a => (x a).1) (fun a => (x a).2)
      (fun j => lineLaw (G.bits j) z hz hz') ≠ 0) :
    (Coverage.sharingCoverage G.lineShares H.endpointData x).card = k := by
…

Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.lineLaw, OAI.CoordinateSweeps.Coverage.sharingCoverage

theorem OAI.CoordinateSweeps.Grid.Holes.probability_nonzero_placementKernel_le line 927

Source comment

The exact full-array probability bound needed to estimate the counting Hilbert--Schmidt norm in the many-coordinate sparse case.

theorem probability_nonzero_placementKernel_le (H : G.Holes h) (hH : H.Feasible)
    (z : ℝ) (hz : 0 ≤ z) (hz' : z ≤ 1)
    (hsmall : ((k+h : ℕ) : ℝ) * G.lineSharingRate ≤ 1) :
    Coverage.probability G.endpointWeight (fun x : Fin k → G.Slot × G.Slot =>
      H.placementKernel (fun a => (x a).1) (fun a => (x a).2)
        (fun j => lineLaw (G.bits j) z hz hz') ≠ 0) ≤
      (2 : ℝ)^k * (((k+h : ℕ) : ℝ) * G.lineSharingRate)^((k : ℝ)/2) := by
…

Mentions: OAI.CoordinateSweeps.Coverage.probability, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.lineLaw