OAI/Probability/CoordinateSweeps/Grid.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CoordinateSweeps.FiniteLaw line 28

   Source comment

   A probability law on a finite sample space, with real-valued masses.

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:19 (same declaration text).

   structure FiniteLaw (Ω : Type*) where
   …

2. instance OAI.CoordinateSweeps.FiniteLaw.(instance at line 37) line 37
3. theorem OAI.CoordinateSweeps.FiniteLaw.ext line 39

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:30 (same declaration text).

4. theorem OAI.CoordinateSweeps.FiniteLaw.sum_mass line 47

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:38 (same declaration text).

5. def OAI.CoordinateSweeps.FiniteLaw.uniform line 51

   Source comment

   Uniform probability, not counting measure.

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:41 (same declaration text).

   def uniform (Ω : Type*) [Fintype Ω] [Nonempty Ω] : FiniteLaw Ω where
   …

   Mentions: OAI.CoordinateSweeps.FiniteLaw

6. def OAI.CoordinateSweeps.FiniteLaw.map line 60

   Source comment

   Push forward a law; the sample space need not map injectively.

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:49 (same declaration text).

   def map (μ : FiniteLaw Ω) (f : Ω → X) : FiniteLaw X where
   …

   Mentions: OAI.CoordinateSweeps.FiniteLaw

7. theorem OAI.CoordinateSweeps.FiniteLaw.uniform_apply line 69
8. theorem OAI.CoordinateSweeps.FiniteLaw.map_apply line 72
9. def OAI.CoordinateSweeps.FiniteLaw.mix line 76

   Source comment

   Mixture of two laws, with the real probability range explicit.

   def mix (μ ν : FiniteLaw Ω) (z : ℝ) (hz : 0 ≤ z) (hz' : z ≤ 1) : FiniteLaw Ω where
   …

   Mentions: OAI.CoordinateSweeps.FiniteLaw

10. def OAI.CoordinateSweeps.FiniteLaw.independent line 86

    Source comment

    Independent laws on finitely many (possibly different) finite spaces.

    def independent {ι : Type*} [Fintype ι] {A : ι → Type*} [∀ i, Fintype (A i)]
        (μ : ∀ i, FiniteLaw (A i)) : FiniteLaw (∀ i, A i) where
    …

    Mentions: OAI.CoordinateSweeps.FiniteLaw

11. def OAI.CoordinateSweeps.FiniteLaw.tv line 96

    Source comment

    The finite total-variation convention of the source: half the l1 distance.

    def tv (μ ν : FiniteLaw Ω) : ℝ := (1 / 2 : ℝ) * ∑ x, |μ x - ν x|

    Mentions: OAI.CoordinateSweeps.FiniteLaw

12. def OAI.CoordinateSweeps.FiniteLaw.event line 99

    Source comment

    Probability of an event.

    def event (μ : FiniteLaw Ω) (s : Finset Ω) : ℝ := ∑ x ∈ s, μ x
    …

    Mentions: OAI.CoordinateSweeps.FiniteLaw

13. def OAI.CoordinateSweeps.lineCost line 103
14. theorem OAI.CoordinateSweeps.monotone_prefix_average line 106
15. theorem OAI.CoordinateSweeps.sum_corrections line 124
16. theorem OAI.CoordinateSweeps.lineCost_eq line 137
17. theorem OAI.CoordinateSweeps.lineCost_nonneg line 143
18. theorem OAI.CoordinateSweeps.full_lineCost_le line 154
19. theorem OAI.CoordinateSweeps.lineCost_le line 162
20. abbrev OAI.CoordinateSweeps.Cube line 177

    Source comment

    Binary positions with their actual bit-coordinate labels.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:60 (same declaration text).

    abbrev Cube (d : ℕ) := Fin d → Bool

21. def OAI.CoordinateSweeps.pairSwitch line 180

    Source comment

    Switches on a family of disjoint two-point fibers.

    Distinct definitions of this name: ComparatorChallenges/CoordinateSweeps.lean:62 (same statement text; different proof or body). Qualify references as OAI.CoordinateSweeps.pairSwitch@path.

    def pairSwitch {L : Type*} (bits : L → Bool) : Equiv.Perm (Bool × L) where
    …

22. def OAI.CoordinateSweeps.binaryLayer line 193

    Source comment

    The parallel-edge switch layer in one specified bit direction.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:74 (same declaration text).

    def binaryLayer {d : ℕ} (j : Fin d) (bits : ({k : Fin d // k ≠ j} → Bool) → Bool) :
        Equiv.Perm (Cube d) :=
    …

    Mentions: OAI.CoordinateSweeps.Cube

23. def OAI.CoordinateSweeps.orderedProduct line 198

    Source comment

    Ordered composition: coordinate 0 is visited first.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:79 (same declaration text).

    def orderedProduct {G : Type*} [Monoid G] {d : ℕ} (g : Fin d → G) : G :=
    …

24. abbrev OAI.CoordinateSweeps.BinaryChoices line 202

    Source comment

    Exactly one independent fair bit for every stage-edge.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:82 (same declaration text).

    abbrev BinaryChoices (d : ℕ) := ∀ j : Fin d, ({k : Fin d // k ≠ j} → Bool) → Bool

25. instance OAI.CoordinateSweeps.(instance at line 204) line 204
26. def OAI.CoordinateSweeps.binarySweep line 207

    Source comment

    One binary coordinate sweep, with all individual switches specified.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:86 (same declaration text).

    def binarySweep (d : ℕ) (bits : BinaryChoices d) : Equiv.Perm (Cube d) :=
    …

    Mentions: OAI.CoordinateSweeps.BinaryChoices, OAI.CoordinateSweeps.Cube

27. def OAI.CoordinateSweeps.binaryLaw line 211

    Source comment

    The source's B_(2^d), as the pushforward of the independent fair switches.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:89 (same declaration text).

    def binaryLaw (d : ℕ) : FiniteLaw (Equiv.Perm (Cube d)) :=
    …

    Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube

28. def OAI.CoordinateSweeps.lineLaw line 215

    Source comment

    The line law L_m(z)=(1-z)U_m+zB_m, with m=2^d.

    def lineLaw (d : ℕ) (z : ℝ) (hz : 0 ≤ z) (hz' : z ≤ 1) :
        FiniteLaw (Equiv.Perm (Cube d)) :=
    …

    Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube

29. structure OAI.CoordinateSweeps.Grid line 221

    Source comment

    An ordered power-of-two grid. Its coordinate bounds are kept in the theorem, not hidden in a change to the definition of the process.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:92 (same declaration text).

    structure Grid where
    …

30. def OAI.CoordinateSweeps.Grid.size line 228

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:99 (same declaration text).

31. abbrev OAI.CoordinateSweeps.Grid.Slot line 230

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:101 (same declaration text).

32. abbrev OAI.CoordinateSweeps.Grid.Line line 232

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:103 (same declaration text).

33. abbrev OAI.CoordinateSweeps.Grid.Choices line 234

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:105 (same declaration text).

34. def OAI.CoordinateSweeps.Grid.fiberPerm line 237

    Source comment

    Simultaneous permutations on disjoint coordinate lines.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:107 (same declaration text).

    def fiberPerm {A B : Type*} (p : B → Equiv.Perm A) : Equiv.Perm (A × B) where
    …

35. def OAI.CoordinateSweeps.Grid.stage line 243

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:113 (same declaration text).

36. def OAI.CoordinateSweeps.Grid.boundary line 248

    Source comment

    The partial sweep at a stage boundary, including boundaries 0 and b.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:117 (same declaration text).

    def boundary (G : Grid) (ω : G.Choices) (t : ℕ) : Equiv.Perm G.Slot :=
    …

    Mentions: OAI.CoordinateSweeps.Grid

37. def OAI.CoordinateSweeps.Grid.sweep line 251

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:120 (same declaration text).

38. def OAI.CoordinateSweeps.Grid.stageLaw line 254

    Source comment

    Independent line choices for a single coordinate stage.

    def stageLaw (G : Grid) (j : Fin G.b) (z : ℝ) (hz : 0 ≤ z) (hz' : z ≤ 1) :
        FiniteLaw (G.Line j → Equiv.Perm (Cube (G.bits j))) :=
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube

39. def OAI.CoordinateSweeps.Grid.choiceLaw line 259

    Source comment

    All stage-lines randomize independently, exactly as in 03-paths:5-17.

    def choiceLaw (G : Grid) (z : ℝ) (hz : 0 ≤ z) (hz' : z ≤ 1) : FiniteLaw G.Choices :=
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.FiniteLaw

40. def OAI.CoordinateSweeps.Grid.Allowed line 263

    Source comment

    Allowed grid, with R=2^r. This is precisely m_j ∈ [R,R²] in bit coordinates.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:123 (same declaration text).

    def Allowed (G : Grid) (r : ℕ) : Prop := ∀ j, r ≤ G.bits j ∧ G.bits j ≤ 2 * r

    Mentions: OAI.CoordinateSweeps.Grid

41. structure OAI.CoordinateSweeps.Grid.Holes line 266

    Source comment

    Prescribed disjoint trajectories; disjointness is required at every boundary.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:126 (same declaration text).

    structure Holes (G : Grid) (h : ℕ) where
    …

    Mentions: OAI.CoordinateSweeps.Grid

42. def OAI.CoordinateSweeps.Grid.Holes.Compatible line 276

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:136 (same declaration text).

43. def OAI.CoordinateSweeps.Grid.Holes.Feasible line 279

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:139 (same declaration text).

44. def OAI.CoordinateSweeps.Grid.Holes.lineCount line 282

    Source comment

    Holes using a particular stage-line, counted before that stage.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:141 (same declaration text).

    def lineCount (H : G.Holes h) (j : Fin G.b) (L : G.Line j) : ℕ :=
    …

45. def OAI.CoordinateSweeps.Grid.Holes.cost line 287

    Source comment

    The exact falling-factorial potential C(H), with (m)_0=1.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:145 (same declaration text).

    def cost (H : G.Holes h) : ℝ :=
    …

46. theorem OAI.CoordinateSweeps.Grid.Holes.lineCount_le line 292
47. theorem OAI.CoordinateSweeps.Grid.Holes.sum_lineCount line 309
48. theorem OAI.CoordinateSweeps.Grid.Holes.cost_nonneg line 316
49. theorem OAI.CoordinateSweeps.Grid.Holes.cost_le line 323
50. def OAI.CoordinateSweeps.Grid.Holes.stabilizer line 337

    Source comment

    Permutations of the free input sites, presented as permutations fixing the prescribed inputs. This is the symmetric group on exactly s-h sites.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:151 (same declaration text).

    def stabilizer (H : G.Holes h) : Subgroup (Equiv.Perm G.Slot) where
    …

51. def OAI.CoordinateSweeps.Grid.Holes.reference line 348

    Source comment

    One feasible reference bijection is a permitted choice of identifications of the remaining input and output sites (02-preliminaries:5).

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:160 (same declaration text).

    def reference (H : G.Holes h) (hf : H.Feasible) : G.Choices := hf.choose

52. theorem OAI.CoordinateSweeps.Grid.Holes.reference_compatible line 350

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:162 (same declaration text).

53. def OAI.CoordinateSweeps.Grid.Holes.residual line 354

    Source comment

    The remaining permutation relative to those identifications.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:166 (same declaration text).

    def residual (H : G.Holes h) (hf : H.Feasible) (ω : {ω : G.Choices // H.Compatible ω}) :
        H.stabilizer :=
    …

54. def OAI.CoordinateSweeps.Grid.choiceWeight line 365

    Source comment

    Joint mass of all independent stage-line choices.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:177 (same declaration text).

    def choiceWeight (G : Grid) (z : ℝ) (ω : G.Choices) : ℝ :=
    …

    Mentions: OAI.CoordinateSweeps.Grid

55. theorem OAI.CoordinateSweeps.Grid.choiceWeight_eq line 370
56. theorem OAI.CoordinateSweeps.Grid.choiceWeight_pos line 373
57. theorem OAI.CoordinateSweeps.Grid.boundary_zero line 390
58. theorem OAI.CoordinateSweeps.Grid.boundary_succ line 393
59. theorem OAI.CoordinateSweeps.Grid.stage_apply_same line 399
60. theorem OAI.CoordinateSweeps.Grid.stage_apply_ne line 403
61. def OAI.CoordinateSweeps.Grid.Holes.StepCompatible line 410
62. theorem OAI.CoordinateSweeps.Grid.Holes.compatible_iff_step line 413
63. theorem OAI.CoordinateSweeps.Grid.Holes.step_iff_coordinate line 442

    Source comment

    Compatibility is a product of independent line assignment events.

    theorem step_iff_coordinate (H : G.Holes h) (ω : G.Choices) :
        H.StepCompatible ω ↔ ∀ i (j : Fin G.b),
          ω j (fun k => H.path i j.castSucc k) (H.path i j.castSucc j) = H.path i j.succ j := by
    …

64. def OAI.CoordinateSweeps.Grid.Holes.OnLine line 456
65. theorem OAI.CoordinateSweeps.Grid.Holes.line_input_injective line 459
66. theorem OAI.CoordinateSweeps.Grid.Holes.line_output_injective line 469
67. theorem OAI.CoordinateSweeps.Grid.Holes.feasible_of_disjoint line 484

    Source comment

    Disjoint source trajectories really are feasible; no probability event is postulated to be nonempty. The main target still retains its explicit feasibility hypothesis.

    theorem feasible_of_disjoint (H : G.Holes h) : H.Feasible := by
    …

68. theorem OAI.CoordinateSweeps.FiniteLaw.mass_le_one line 502
69. theorem OAI.CoordinateSweeps.FiniteLaw.mix_uniform_between line 508

    Source comment

    A uniform, finite-alphabet perturbation interval, depending on the line size only. This proves the source's half-to-two measure comparison.

    theorem mix_uniform_between [Nonempty Ω] (ν : FiniteLaw Ω) {z : ℝ}
        (hz : 0 ≤ z) (hzhalf : z ≤ 1/2) (hzcard : z ≤ (Fintype.card Ω : ℝ)⁻¹)
        (x : Ω) :
        (1/2 : ℝ) * uniform Ω x ≤ (uniform Ω).mix ν z hz (by linarith) x ∧
          (uniform Ω).mix ν z hz (by linarith) x ≤ 2 * uniform Ω x := by
    …

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

70. def OAI.CoordinateSweeps.FiniteLaw.assignments line 525
71. theorem OAI.CoordinateSweeps.FiniteLaw.assignments_nonneg line 529
72. theorem OAI.CoordinateSweeps.FiniteLaw.sum_assignments line 537
73. theorem OAI.CoordinateSweeps.FiniteLaw.uniform_assignments_same line 543
74. theorem OAI.CoordinateSweeps.FiniteLaw.uniform_assignments line 568
75. theorem OAI.CoordinateSweeps.FiniteLaw.uniform_assignments_pos line 585
76. theorem OAI.CoordinateSweeps.FiniteLaw.assignments_le line 591
77. theorem OAI.CoordinateSweeps.FiniteLaw.le_assignments line 602
78. theorem OAI.CoordinateSweeps.FiniteLaw.assignments_ratio_le_four line 615

    Source comment

    The exact factor four in the line-conditioning argument, with all line assignments represented by actual injections, not abstract events.

    theorem assignments_ratio_le_four {h v : ℕ} (μ : FiniteLaw (Equiv.Perm Ω))
        (hμlo : ∀ g, (1/2 : ℝ) * uniform (Equiv.Perm Ω) g ≤ μ g)
        (hμhi : ∀ g, μ g ≤ 2 * uniform (Equiv.Perm Ω) g)
        (x y : Fin h ↪ Ω) (x' y' : Fin (h+v) ↪ Ω) :
        μ.assignments x' y' / μ.assignments x y ≤
          4 * (((Fintype.card Ω - h).descFactorial v : ℝ)⁻¹) := by
    …

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

79. def OAI.CoordinateSweeps.Grid.Holes.LineCompatible line 648
80. theorem OAI.CoordinateSweeps.Grid.Holes.compatible_iff_lines line 652
81. def OAI.CoordinateSweeps.Grid.Holes.compatibleEquiv line 663
82. def OAI.CoordinateSweeps.Grid.Holes.probability line 673

    Source comment

    Probability of the prescribed trajectory event, with the root definition.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:186 (same declaration text).

    def probability (H : G.Holes h) (z : ℝ) : ℝ :=
    …

83. theorem OAI.CoordinateSweeps.Grid.Holes.probability_prod line 677

    Source comment

    Exact path probability factors into its independent constrained lines.

    theorem probability_prod (H : G.Holes h) {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ 1) :
        H.probability z = ∏ j, ∏ L, ∑ σ : {σ // H.LineCompatible j L σ},
          lineLaw (G.bits j) z hz hz' σ.val := by
    …

    Mentions: OAI.CoordinateSweeps.lineLaw

84. theorem OAI.CoordinateSweeps.Grid.Holes.card_onLine line 692
85. def OAI.CoordinateSweeps.Grid.Holes.lineCards line 699
86. def OAI.CoordinateSweeps.Grid.Holes.lineInput line 703
87. def OAI.CoordinateSweeps.Grid.Holes.lineOutput line 707
88. theorem OAI.CoordinateSweeps.Grid.Holes.lineCompatible_iff_assignments line 711
89. theorem OAI.CoordinateSweeps.Grid.Holes.sum_subtype_eq_sum_ite_of_iff line 723
90. theorem OAI.CoordinateSweeps.Grid.Holes.lineProbability_eq line 734
91. theorem OAI.CoordinateSweeps.Grid.Holes.probability_eq_assignments line 740
92. theorem OAI.CoordinateSweeps.Grid.Holes.probability_zero line 752

    Source comment

    Under uniform line randomization each prescribed injection pays exactly one falling-factorial denominator.

    theorem probability_zero (H : G.Holes h) :
        H.probability 0 = ∏ j, ∏ L,
          (((2 ^ G.bits j).descFactorial (H.lineCount j L) : ℝ)⁻¹) := by
    …