OAI/Computability/MaxCut/Games/PartnerProjection.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MaxCutGames.Soundness.PartnerProjection.Slot line 8
2. structure OAI.MaxCutGames.Soundness.PartnerProjection.Triple line 12
3. def OAI.MaxCutGames.Soundness.PartnerProjection.zeroTriple line 18
4. def OAI.MaxCutGames.Soundness.PartnerProjection.parity line 20
5. def OAI.MaxCutGames.Soundness.PartnerProjection.addTriple line 22
6. theorem OAI.MaxCutGames.Soundness.PartnerProjection.parity_add line 25
7. theorem OAI.MaxCutGames.Soundness.PartnerProjection.and_xor line 31
8. def OAI.MaxCutGames.Soundness.PartnerProjection.retained line 35
9. def OAI.MaxCutGames.Soundness.PartnerProjection.freeBit line 41
10. theorem OAI.MaxCutGames.Soundness.PartnerProjection.retained_add line 47
11. theorem OAI.MaxCutGames.Soundness.PartnerProjection.freeBit_add line 51
12. def OAI.MaxCutGames.Soundness.PartnerProjection.complete line 56

    Source documentation

    Reconstruct a parity-constrained triple from its retained bit and one free bit.

    def complete (s : Slot) (p r f : Bool) : Triple :=
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerProjection.Slot, OAI.MaxCutGames.Soundness.PartnerProjection.Triple

13. theorem OAI.MaxCutGames.Soundness.PartnerProjection.parity_complete line 62
14. theorem OAI.MaxCutGames.Soundness.PartnerProjection.retained_complete line 66
15. theorem OAI.MaxCutGames.Soundness.PartnerProjection.freeBit_complete line 70
16. theorem OAI.MaxCutGames.Soundness.PartnerProjection.complete_coordinates line 74
17. theorem OAI.MaxCutGames.Soundness.PartnerProjection.retained_zero line 79
18. theorem OAI.MaxCutGames.Soundness.PartnerProjection.freeBit_zero line 82
19. theorem OAI.MaxCutGames.Soundness.PartnerProjection.complete_zero line 85
20. theorem OAI.MaxCutGames.Soundness.PartnerProjection.complete_kernel_add line 88
21. structure OAI.MaxCutGames.Soundness.PartnerProjection.SourcePoint line 95
22. structure OAI.MaxCutGames.Soundness.PartnerProjection.PartnerPoint line 100
23. theorem OAI.MaxCutGames.Soundness.PartnerProjection.source_ext line 108
24. theorem OAI.MaxCutGames.Soundness.PartnerProjection.partner_ext line 116
25. def OAI.MaxCutGames.Soundness.PartnerProjection.project line 126
26. def OAI.MaxCutGames.Soundness.PartnerProjection.lift line 135

    Source documentation

    The constructive preimage used in Lemma 6.1: choose the free bit to be zero.

    def lift (y : PartnerPoint rhs active) : SourcePoint rhs where
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerProjection.PartnerPoint, OAI.MaxCutGames.Soundness.PartnerProjection.SourcePoint

27. theorem OAI.MaxCutGames.Soundness.PartnerProjection.project_lift line 146
28. theorem OAI.MaxCutGames.Soundness.PartnerProjection.project_surjective line 159
29. theorem OAI.MaxCutGames.Soundness.PartnerProjection.homogeneous_preserved line 164
30. def OAI.MaxCutGames.Soundness.PartnerProjection.zeroSource line 167
31. def OAI.MaxCutGames.Soundness.PartnerProjection.zeroPartner line 172
32. def OAI.MaxCutGames.Soundness.PartnerProjection.addSource line 180
33. def OAI.MaxCutGames.Soundness.PartnerProjection.addPartner line 187
34. theorem OAI.MaxCutGames.Soundness.PartnerProjection.project_add line 204

    Source documentation

    The projection preserves F₂ addition, as well as zero.

    theorem project_add (x y : SourcePoint rhs) :
        project rhs active slot (addSource rhs x y) =
          addPartner rhs active (project rhs active slot x) (project rhs active slot y) := by
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerProjection.SourcePoint, OAI.MaxCutGames.Soundness.PartnerProjection.project, OAI.MaxCutGames.Soundness.PartnerProjection.addSource, OAI.MaxCutGames.Soundness.PartnerProjection.addPartner

35. theorem OAI.MaxCutGames.Soundness.PartnerProjection.project_zero line 214
36. def OAI.MaxCutGames.Soundness.PartnerProjection.InKernel line 223
37. theorem OAI.MaxCutGames.Soundness.PartnerProjection.kernel_characterization line 226
38. structure OAI.MaxCutGames.Soundness.PartnerProjection.ActiveBits line 253

    Source documentation

    One coefficient bit at every active position; all other coefficients vanish.

    structure ActiveBits where
    …

39. theorem OAI.MaxCutGames.Soundness.PartnerProjection.activeBits_ext line 257
40. def OAI.MaxCutGames.Soundness.PartnerProjection.addActiveBits line 264
41. def OAI.MaxCutGames.Soundness.PartnerProjection.kernelPoint line 271
42. theorem OAI.MaxCutGames.Soundness.PartnerProjection.kernelPoint_add line 276
43. theorem OAI.MaxCutGames.Soundness.PartnerProjection.kernelPoint_mem line 284
44. def OAI.MaxCutGames.Soundness.PartnerProjection.kernelCoefficients line 293
45. theorem OAI.MaxCutGames.Soundness.PartnerProjection.kernelPoint_coefficients line 301
46. theorem OAI.MaxCutGames.Soundness.PartnerProjection.coefficients_kernelPoint line 317
47. theorem OAI.MaxCutGames.Soundness.PartnerProjection.kernelPoint_injective line 324
48. theorem OAI.MaxCutGames.Soundness.PartnerProjection.kernel_unique_coefficients line 336

    Source documentation

    Every kernel vector is uniquely determined by one bit per active position.

    theorem kernel_unique_coefficients (x : SourcePoint rhs) (hx : InKernel rhs active slot x) :
        ∃ a : ActiveBits active, kernelPoint rhs active slot a = x ∧
          ∀ b : ActiveBits active, kernelPoint rhs active slot b = x → b = a := by
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerProjection.SourcePoint, OAI.MaxCutGames.Soundness.PartnerProjection.InKernel, OAI.MaxCutGames.Soundness.PartnerProjection.ActiveBits, OAI.MaxCutGames.Soundness.PartnerProjection.kernelPoint

49. def OAI.MaxCutGames.Soundness.PartnerProjection.extendActive line 346

    Source documentation

    Extend an arbitrary function on the active positions by zero.

    def extendActive (f : {j : Position // active j = true} → Bool) : ActiveBits active where
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerProjection.ActiveBits

50. theorem OAI.MaxCutGames.Soundness.PartnerProjection.kernel_realizes_active line 350
51. theorem OAI.MaxCutGames.Soundness.PartnerProjection.kernel_determined_by_active line 359
52. theorem OAI.MaxCutGames.Soundness.PartnerProjection.disjoint_kernels_intersection_zero line 377

    Source documentation

    The final assertion of Lemma 6.1, including arbitrary retained indices.

    theorem disjoint_kernels_intersection_zero
        (active' : Position → Bool) (slot' : Position → Slot)
        (hdisjoint : ∀ j, active j = true → active' j = false)
        (x : SourcePoint rhs)
        (hx : InKernel rhs active slot x)
        (hx' : InKernel rhs active' slot' x) : x = zeroSource rhs := by
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerProjection.Slot, OAI.MaxCutGames.Soundness.PartnerProjection.SourcePoint, OAI.MaxCutGames.Soundness.PartnerProjection.InKernel, OAI.MaxCutGames.Soundness.PartnerProjection.zeroSource

53. abbrev OAI.MaxCutGames.Soundness.KernelCardinality.Kernel line 406
54. def OAI.MaxCutGames.Soundness.KernelCardinality.kernelEquiv line 409

    Source documentation

    Exactly one freely chosen bit per active position parametrizes the kernel.

    def kernelEquiv : Kernel rhs active slot ≃ ({j : P // active j = true} → Bool) where
    …

    Mentions: OAI.MaxCutGames.Soundness.KernelCardinality.Kernel

55. instance OAI.MaxCutGames.Soundness.KernelCardinality.kernelFintype line 424
56. theorem OAI.MaxCutGames.Soundness.KernelCardinality.kernel_card line 429

    Source documentation

    The actual kernel has 2^t points when there are t active positions.

    theorem kernel_card [Fintype P] :
        Fintype.card (Kernel rhs active slot) = 2 ^ Fintype.card {j : P // active j = true} := by
    …

    Mentions: OAI.MaxCutGames.Soundness.KernelCardinality.Kernel

57. theorem OAI.MaxCutGames.Soundness.KernelCardinality.kernel_card_of_active_card line 438
58. theorem OAI.MaxCutGames.Gadget.LinearKernelCount.card_binary_space line 464

    Source documentation

    A finite-dimensional binary vector space has 2^dimension vectors.

    theorem card_binary_space : Nat.card V = 2 ^ Module.finrank (ZMod 2) V := by
    …

59. theorem OAI.MaxCutGames.Gadget.LinearKernelCount.kernel_card_mul_pow_rank line 469

    Source documentation

    Exact cross-multiplied uniform kernel probability: |ker f| * 2^rank f = |V|.

    theorem kernel_card_mul_pow_rank (f : V →ₗ[ZMod 2] P) :
        Nat.card f.ker * 2 ^ Module.finrank (ZMod 2) f.range = Nat.card V := by
    …

60. theorem OAI.MaxCutGames.Gadget.LinearKernelCount.card_source_pos line 477

    Source documentation

    The denominator of the uniform vector experiment is positive.

    theorem card_source_pos : 0 < Nat.card V := by
    …

61. theorem OAI.MaxCutGames.Gadget.LinearKernelCount.kernel_card_eq_pow_sub_rank line 482

    Source documentation

    The kernel size itself is the familiar power of the nullity.

    theorem kernel_card_eq_pow_sub_rank (f : V →ₗ[ZMod 2] P) :
        Nat.card f.ker =
          2 ^ (Module.finrank (ZMod 2) V - Module.finrank (ZMod 2) f.range) := by
    …

62. theorem OAI.MaxCutGames.Gadget.LinearKernelCount.zero_event_card_mul_pow_rank line 491

    Source documentation

    The kernel formula expressed directly as the cardinality of the zero event.

    theorem zero_event_card_mul_pow_rank (f : V →ₗ[ZMod 2] P) :
        Nat.card {x : V // f x = 0} * 2 ^ Module.finrank (ZMod 2) f.range = Nat.card V :=
    …

63. theorem OAI.MaxCutGames.Gadget.LinearKernelCount.zero_event_card_mul_pow_le line 496

    Source documentation

    A rank threshold gives the exact cleared-denominator bound used on a good leaf.

    theorem zero_event_card_mul_pow_le (f : V →ₗ[ZMod 2] P) (r : Nat)
        (hr : r ≤ Module.finrank (ZMod 2) f.range) :
        Nat.card {x : V // f x = 0} * 2 ^ r ≤ Nat.card V := by
    …

64. theorem OAI.MaxCutGames.Gadget.LinearKernelCount.zero_event_finset_count_mul_pow_rank line 506

    Source documentation

    The same exact probability identity for a direct count over a finite universe.

    theorem zero_event_finset_count_mul_pow_rank [Fintype V] [DecidableEq P]
        (f : V →ₗ[ZMod 2] P) :
        (Finset.univ.filter (fun x : V => f x = 0)).card *
          2 ^ Module.finrank (ZMod 2) f.range = Fintype.card V := by
    …

65. theorem OAI.MaxCutGames.Gadget.LinearKernelCount.zero_event_finset_count_mul_pow_le line 514

    Source documentation

    A rank-r lower bound yields a 2⁻ʳ bound on the actual finite zero-event count.

    theorem zero_event_finset_count_mul_pow_le [Fintype V] [DecidableEq P]
        (f : V →ₗ[ZMod 2] P) (r : Nat)
        (hr : r ≤ Module.finrank (ZMod 2) f.range) :
        (Finset.univ.filter (fun x : V => f x = 0)).card * 2 ^ r ≤ Fintype.card V := by
    …

66. abbrev OAI.MaxCutGames.Soundness.PartnerLinear.SourceCoordinates line 531
67. abbrev OAI.MaxCutGames.Soundness.PartnerLinear.Active line 532
68. abbrev OAI.MaxCutGames.Soundness.PartnerLinear.Inactive line 533
69. abbrev OAI.MaxCutGames.Soundness.PartnerLinear.PartnerCoordinates line 534
70. def OAI.MaxCutGames.Soundness.PartnerLinear.sourceCoordinates line 536
71. def OAI.MaxCutGames.Soundness.PartnerLinear.sourceFromCoordinates line 539
72. def OAI.MaxCutGames.Soundness.PartnerLinear.sourceEquiv line 545
73. def OAI.MaxCutGames.Soundness.PartnerLinear.partnerCoordinates line 563
74. def OAI.MaxCutGames.Soundness.PartnerLinear.partnerFromCoordinates line 568
75. def OAI.MaxCutGames.Soundness.PartnerLinear.partnerEquiv line 579
76. instance OAI.MaxCutGames.Soundness.PartnerLinear.sourceAddCommGroup line 608
77. instance OAI.MaxCutGames.Soundness.PartnerLinear.sourceModule line 611
78. instance OAI.MaxCutGames.Soundness.PartnerLinear.partnerAddCommGroup line 614
79. instance OAI.MaxCutGames.Soundness.PartnerLinear.partnerModule line 617
80. def OAI.MaxCutGames.Soundness.PartnerLinear.sourceLinearEquiv line 620
81. def OAI.MaxCutGames.Soundness.PartnerLinear.partnerLinearEquiv line 623
82. instance OAI.MaxCutGames.Soundness.PartnerLinear.sourceFintype line 626
83. instance OAI.MaxCutGames.Soundness.PartnerLinear.partnerFintype line 630
84. theorem OAI.MaxCutGames.Soundness.PartnerLinear.source_add line 634
85. theorem OAI.MaxCutGames.Soundness.PartnerLinear.source_zero line 643
86. theorem OAI.MaxCutGames.Soundness.PartnerLinear.partner_add line 649
87. theorem OAI.MaxCutGames.Soundness.PartnerLinear.partner_zero line 662
88. def OAI.MaxCutGames.Soundness.PartnerLinear.projection line 668
89. theorem OAI.MaxCutGames.Soundness.PartnerLinear.projection_apply line 677
90. theorem OAI.MaxCutGames.Soundness.PartnerLinear.projection_surjective line 680
91. theorem OAI.MaxCutGames.Soundness.PartnerLinear.mem_projection_ker line 683
92. instance OAI.MaxCutGames.Soundness.PartnerLinear.sourceFiniteDimensional line 689
93. instance OAI.MaxCutGames.Soundness.PartnerLinear.partnerFiniteDimensional line 693
94. def OAI.MaxCutGames.Soundness.PartnerLinear.kernelEquiv line 698

    Source documentation

    Identifies the actual linear kernel with the previously counted concrete kernel.

    noncomputable def kernelEquiv :
        (projection rhs active slot).ker ≃ KernelCardinality.Kernel rhs active slot where
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerLinear.projection, OAI.MaxCutGames.Soundness.KernelCardinality.Kernel

95. theorem OAI.MaxCutGames.Soundness.PartnerLinear.projection_ker_card line 705
96. theorem OAI.MaxCutGames.Soundness.PartnerLinear.projection_ker_finrank line 710
97. theorem OAI.MaxCutGames.Soundness.PartnerLinear.projection_ker_finrank_of_card line 717
98. theorem OAI.MaxCutGames.Soundness.PartnerLinear.source_finrank line 722
99. theorem OAI.MaxCutGames.Soundness.PartnerLinear.disjoint_projection_kernels line 728

    Source documentation

    Distinct coordinate blocks make disjoint active-set kernels have trivial intersection.

    theorem disjoint_projection_kernels
        (active' : P → Bool) (slot' : P → Slot)
        (hdisjoint : ∀ j, active j = true → active' j = false) :
        (projection rhs active slot).ker ⊓ (projection rhs active' slot').ker = ⊥ := by
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerLinear.projection

100. def OAI.MaxCutGames.Soundness.PartnerLinear.sourceTau line 741
101. def OAI.MaxCutGames.Soundness.PartnerLinear.partnerTau line 744
102. theorem OAI.MaxCutGames.Soundness.PartnerLinear.sourceTau_apply line 748
103. theorem OAI.MaxCutGames.Soundness.PartnerLinear.partnerTau_apply line 749
104. theorem OAI.MaxCutGames.Soundness.PartnerLinear.tau_comp_projection line 752