OAI/Computability/MaxCut/Encoding/AdviceLaw.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

The actual finite advice law. Uniform independent hidden/complement maps induce the exact uniform visible-map law, including for rank-deficient public maps. The whole-table comparison retains an arbitrary common occurrence/public-data law, so weighted occurrence sampling is not replaced by uniform IDs.

  1. def OAI.MaxCutGames.Decoder.AdviceLaw.visibleMap line 36

    Source documentation

    The precise visible table (T,A M), with the second component in its actual attainable range. The argument order is complement, hidden matrix.

    def visibleMap (A : K →ₗ[F2] R) {J : Finset (Fin k)}
    (T : RawPoint J →ₗ[F2] W) (M : RawPoint J →ₗ[F2] K) :
    RawPoint J →ₗ[F2] (W × A.range) :=
…
  2. theorem OAI.MaxCutGames.Decoder.AdviceLaw.visibleMap_apply line 42
  3. def OAI.MaxCutGames.Decoder.AdviceLaw.rawMapPairCoefficientsEquiv line 46
  4. theorem OAI.MaxCutGames.Decoder.AdviceLaw.visibleMap_raw line 53
  5. theorem OAI.MaxCutGames.Decoder.AdviceLaw.uniform_visible_maps line 60

    Source documentation

    Equality for every observable proves the whole joint visible-map law.

    theorem uniform_visible_maps (A : K →ₗ[F2] R) (J : Finset (Fin k))
    (H : (RawPoint J →ₗ[F2] (W × A.range)) → ℝ) :
    (𝔼 TM : (RawPoint J →ₗ[F2] W) × (RawPoint J →ₗ[F2] K),
      H (visibleMap A TM.1 TM.2)) =
      𝔼 Y : RawPoint J →ₗ[F2] (W × A.range), H Y := by
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.visibleMap

  6. theorem OAI.MaxCutGames.Decoder.AdviceLaw.uniform_visible_maps_expectation line 76
  7. def OAI.MaxCutGames.Decoder.AdviceLaw.actualSuccess line 90

    Source documentation

    Actual success starts with genuinely sampled hidden and complement maps. The iid incidence law includes every slot choice, including unused choices at full positions. Policies receive only their respective visible table.

    def actualSuccess (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N) (A : K →ₗ[F2] R)
    (policy : ActualAdviceStochasticBridge.Policies k g (W × A.range))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) : ℝ :=
…
  8. theorem OAI.MaxCutGames.Decoder.AdviceLaw.actualSuccess_eq_cleanSuccess line 102
  9. def OAI.MaxCutGames.Decoder.AdviceLaw.drawDistribution line 121
  10. def OAI.MaxCutGames.Decoder.AdviceLaw.paddedDistribution line 135
  11. theorem OAI.MaxCutGames.Decoder.AdviceLaw.paddedDistribution_totalVariation_eq_slope line 142

    Source documentation

    Padding adds an independent uniform affine intercept. The full map's variation is therefore exactly the sparse slope variation used in constants.

    theorem paddedDistribution_totalVariation_eq_slope (rhs : Fin k → Bool) (β : ℝ)
    (hβ : 0 ≤ β) (hβ' : β ≤ 1) :
    (paddedDistribution (V := V) rhs β hβ hβ').totalVariation
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.paddedDistribution

  12. theorem OAI.MaxCutGames.Decoder.AdviceLaw.paddedDistribution_totalVariation line 151
  13. def OAI.MaxCutGames.Decoder.AdviceLaw.withKernel line 165

    Source documentation

    Keep the common outer datum while sampling its conditional table law.

    def withKernel (μ : FiniteDistribution Ω) (p : Ω → FiniteDistribution Y) :
    FiniteDistribution (Ω × Y) where
…
  14. theorem OAI.MaxCutGames.Decoder.AdviceLaw.withKernel_totalVariation line 174
  15. theorem OAI.MaxCutGames.Decoder.AdviceLaw.withKernel_totalVariation_le line 190
  16. theorem OAI.MaxCutGames.Decoder.AdviceLaw.wholeAdvice_totalVariation line 206

    Source documentation

    Whole (occurrences, public advice, Mπ,Tπ) comparison. The product codomain represents the two genuine sampled maps; occurrence weights are arbitrary and remain in both laws. The public law can in particular be uniform on all row maps. Projection choices are averaged out before this comparison.

    theorem wholeAdvice_totalVariation {k : ℕ} {Id A V : Type}
    [Fintype Id] [Fintype A] [AddCommGroup V] [Module F2 V] [Fintype V]
    [Fintype (ActualHomogeneous.E k →ₗ[F2] V)]
    (occurrences : FiniteDistribution (Fin k → Id)) (publicLaw : FiniteDistribution A)
    (rhs : Id → Bool) (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) :
    (withKernel (occurrences.product publicLaw)
      (fun ua => paddedDistribution (V := V) (fun j => rhs (ua.1 j)) β hβ hβ')).totalVariation
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.withKernel, OAI.MaxCutGames.Decoder.AdviceLaw.paddedDistribution

  17. theorem OAI.MaxCutGames.Decoder.AdviceLaw.wholeAdvice_totalVariation_eq_slope line 221

    Source documentation

    Common occurrence/public randomness preserves the exact slope variation.

    theorem wholeAdvice_totalVariation_eq_slope {k : ℕ} {Id A V : Type}
    [Fintype Id] [Fintype A] [AddCommGroup V] [Module F2 V] [Fintype V]
    [Fintype (ActualHomogeneous.E k →ₗ[F2] V)]
    (occurrences : FiniteDistribution (Fin k → Id)) (publicLaw : FiniteDistribution A)
    (rhs : Id → Bool) (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) :
    (withKernel (occurrences.product publicLaw)
      (fun ua => paddedDistribution (V := V) (fun j => rhs (ua.1 j)) β hβ hβ')).totalVariation
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.withKernel, OAI.MaxCutGames.Decoder.AdviceLaw.paddedDistribution

  18. theorem OAI.MaxCutGames.Decoder.AdviceLaw.wholeAdvice_totalVariation_le_slope line 237
  19. instance OAI.MaxCutGames.Decoder.AdviceLaw.observedRowsFintype line 257
  20. theorem OAI.MaxCutGames.Decoder.AdviceLaw.observed_hidden_independent line 263

    Source documentation

    After fixing the mask, public map and complement table, the uniform hidden matrix has independent uniform attainable rows and private kernel coordinates. The observation fixes only A M, not M or a chosen witness.

    theorem observed_hidden_independent (J : Finset (Fin k)) (A : K →ₗ[F2] R)
    (f : AdviceFibers.ObservedRow (E := RawPoint J) A → ℝ)
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow

  21. abbrev OAI.MaxCutGames.Decoder.AdviceLaw.ProjectionSeed line 280

    Source documentation

    The actual two-stage sampler retains both its projection choices and its uniform map on that projected target. Thus target advice is not forgotten.

    abbrev ProjectionSeed (k : ℕ) (V : Type) [AddCommGroup V] [Module F2 V] :=
…
  22. def OAI.MaxCutGames.Decoder.AdviceLaw.projectionSeedDistribution line 284
  23. def OAI.MaxCutGames.Decoder.AdviceLaw.projectSeedMap line 295
  24. theorem OAI.MaxCutGames.Decoder.AdviceLaw.projectionSeed_expectation line 301
  25. theorem OAI.MaxCutGames.Decoder.AdviceLaw.projectionSeed_pushforward line 325
  26. def OAI.MaxCutGames.Decoder.AdviceLaw.seedToActualDraw line 345

    Source documentation

    Convert the actual two-stage seed into the full hidden experiment. The second summand of the seed remains available for the target-side observation.

    def seedToActualDraw (occ : Fin k → Id) (A : K →ₗ[F2] R)
    (s : ProjectionSeed k (K × W)) : AdviceExperiment.Draw k Id K W R where
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.ProjectionSeed, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw

  27. theorem OAI.MaxCutGames.Decoder.AdviceLaw.seed_projection line 354
  28. theorem OAI.MaxCutGames.Decoder.AdviceLaw.seed_padded_pair line 360
  29. theorem OAI.MaxCutGames.Decoder.AdviceLaw.seed_left_observation line 367
  30. theorem OAI.MaxCutGames.Decoder.AdviceLaw.seed_right_observation line 376
  31. def OAI.MaxCutGames.Decoder.AdviceLaw.choiceDistribution line 389
  32. def OAI.MaxCutGames.Decoder.AdviceLaw.maskSlotChoice line 396

    Source documentation

    Full positions discard their auxiliary slot; singleton positions retain it.

    def maskSlotChoice (p : Bool × Fin 3) : PaddedLaw.ProjectionChoice :=
…

    Mentions: OAI.MaxCutGames.Decoder.PaddedLaw.ProjectionChoice

  33. theorem OAI.MaxCutGames.Decoder.AdviceLaw.maskSlotChoice_pushforward line 399
  34. def OAI.MaxCutGames.Decoder.AdviceLaw.choicesOfMaskSlots line 409
  35. theorem OAI.MaxCutGames.Decoder.AdviceLaw.choices_expectation line 416

    Source documentation

    The Option sampler is exactly the Bernoulli-mask sampler with independent uniform slots at every position, including the full positions. This identity allows arbitrary functions of the retained choices.

    theorem choices_expectation {k : ℕ} (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1)
    (H : (Fin k → PaddedLaw.ProjectionChoice) → ℝ) :
    ((choiceDistribution β hβ hβ').iid k).expectation H =
      ((Clean.bernoulli β hβ hβ').iid k).expectation (fun mask =>
        (FiniteDistribution.uniform (Fin k → Fin 3)).expectation (fun slots =>
          H (choicesOfMaskSlots mask slots))) := by
…

    Mentions: OAI.MaxCutGames.Decoder.PaddedLaw.ProjectionChoice, OAI.MaxCutGames.Decoder.AdviceLaw.choiceDistribution, OAI.MaxCutGames.Clean.bernoulli, OAI.MaxCutGames.Decoder.AdviceLaw.choicesOfMaskSlots

  36. theorem OAI.MaxCutGames.Decoder.AdviceLaw.choices_mask line 427
  37. theorem OAI.MaxCutGames.Decoder.AdviceLaw.choices_active_slot line 435
  38. theorem OAI.MaxCutGames.Decoder.AdviceLaw.projectionSeed_mask_slots_expectation line 442

    Source documentation

    The same identity with the entire original target map retained. This is the full two-stage seed law, not merely the law of its padded marginal.

    theorem projectionSeed_mask_slots_expectation {k : ℕ} {V : Type}
    [AddCommGroup V] [Module F2 V] [Fintype V]
    (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) (H : ProjectionSeed k V → ℝ) :
    (projectionSeedDistribution β hβ hβ').expectation H =
      ((Clean.bernoulli β hβ hβ').iid k).expectation (fun mask =>
        (FiniteDistribution.uniform (Fin k → Fin 3)).expectation (fun slots =>
          (FiniteDistribution.uniform
            (RawPoint (PaddedLaw.choiceMask (choicesOfMaskSlots mask slots)) →ₗ[F2] V)).expectation
              (fun Y => H ⟨choicesOfMaskSlots mask slots, Y⟩))) := by
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.ProjectionSeed, OAI.MaxCutGames.Decoder.AdviceLaw.projectionSeedDistribution, OAI.MaxCutGames.Clean.bernoulli, OAI.MaxCutGames.Decoder.PaddedLaw.choiceMask, OAI.MaxCutGames.Decoder.AdviceLaw.choicesOfMaskSlots

  39. theorem OAI.MaxCutGames.Decoder.AdviceLaw.product_pushforward_withKernel line 473
  40. def OAI.MaxCutGames.Decoder.AdviceLaw.fullSeedLaw line 499

    Source documentation

    A finite hidden sample whose actual Draw is seedToActualDraw.

    def fullSeedLaw {k : ℕ} {Id A V : Type} [Fintype Id] [Fintype A]
    [AddCommGroup V] [Module F2 V] [Fintype V]
    (occurrences : FiniteDistribution (Fin k → Id)) (publicLaw : FiniteDistribution A)
    (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) :=
…
  41. def OAI.MaxCutGames.Decoder.AdviceLaw.fullSeedPad line 505
  42. theorem OAI.MaxCutGames.Decoder.AdviceLaw.fullSeed_pad_law line 510
  43. theorem OAI.MaxCutGames.Decoder.AdviceLaw.fullSeed_totalVariation line 526
  44. theorem OAI.MaxCutGames.Decoder.AdviceLaw.fullSeed_totalVariation_eq_slope line 539
  45. theorem OAI.MaxCutGames.Decoder.AdviceLaw.fullSeed_totalVariation_le_slope line 554
  46. abbrev OAI.MaxCutGames.Decoder.AdviceLaw.FullSeed line 572
  47. abbrev OAI.MaxCutGames.Decoder.AdviceLaw.CompleteData line 579

    Source documentation

    Complete visible conditioning data: occurrences, public map, projection choices, the entire complement map, and precisely the attainable rows.

    abbrev CompleteData (k : ℕ) (Id K W R : Type)
    [AddCommGroup K] [Module F2 K] [AddCommGroup W] [Module F2 W]
    [AddCommGroup R] [Module F2 R] :=
…
  48. abbrev OAI.MaxCutGames.Decoder.AdviceLaw.PrivateMap line 587
  49. def OAI.MaxCutGames.Decoder.AdviceLaw.targetObservationEquiv line 590
  50. def OAI.MaxCutGames.Decoder.AdviceLaw.fullSeedCoordinatesEquiv line 601

    Source documentation

    A global bijection retains all actual visible data, with exactly one uniform kernel-valued matrix left after conditioning.

    def fullSeedCoordinatesEquiv :
    FullSeed k Id K W R ≃ Σ d : CompleteData k Id K W R, PrivateMap d :=
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.FullSeed, OAI.MaxCutGames.Decoder.AdviceLaw.CompleteData, OAI.MaxCutGames.Decoder.AdviceLaw.PrivateMap

  51. def OAI.MaxCutGames.Decoder.AdviceLaw.completeObserve line 612
  52. def OAI.MaxCutGames.Decoder.AdviceLaw.completeAssemble line 615
  53. theorem OAI.MaxCutGames.Decoder.AdviceLaw.completeObserve_eq line 619
  54. theorem OAI.MaxCutGames.Decoder.AdviceLaw.completeAssemble_eq line 624
  55. theorem OAI.MaxCutGames.Decoder.AdviceLaw.completeObserve_assemble line 629
  56. def OAI.MaxCutGames.Decoder.AdviceLaw.completeFiberEquiv line 635

    Source documentation

    Exact equivalence for a fiber of the complete observation, not just the marginal row observation. This is the input for finite conditioning.

    def completeFiberEquiv (d : CompleteData k Id K W R) :
    PrivateMap d ≃ {s : FullSeed k Id K W R // completeObserve s = d} :=
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.CompleteData, OAI.MaxCutGames.Decoder.AdviceLaw.PrivateMap, OAI.MaxCutGames.Decoder.AdviceLaw.FullSeed, OAI.MaxCutGames.Decoder.AdviceLaw.completeObserve

  57. theorem OAI.MaxCutGames.Decoder.AdviceLaw.completeFiberEquiv_val line 640
  58. def OAI.MaxCutGames.Decoder.AdviceLaw.completeDraw line 644

    Source documentation

    The actual Draw obtained from the complete-data fiber coordinates.

    def completeDraw (d : CompleteData k Id K W R) (N : PrivateMap d) :
    AdviceExperiment.Draw k Id K W R where
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.CompleteData, OAI.MaxCutGames.Decoder.AdviceLaw.PrivateMap, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw

  59. theorem OAI.MaxCutGames.Decoder.AdviceLaw.completeDraw_seed line 653
  60. theorem OAI.MaxCutGames.Decoder.AdviceLaw.completeDraw_rows line 657
  61. theorem OAI.MaxCutGames.Decoder.AdviceLaw.completeDraw_left line 662
  62. theorem OAI.MaxCutGames.Decoder.AdviceLaw.completeDraw_right line 672
  63. def OAI.MaxCutGames.Decoder.AdviceLaw.completeWeight line 683
  64. theorem OAI.MaxCutGames.Decoder.AdviceLaw.fullSeed_weight_observed line 693

    Source documentation

    The actual law has exactly constant point weights on every fiber of all observed data, even for arbitrary occurrence and public-map laws.

    theorem fullSeed_weight_observed (occurrences : FiniteDistribution (Fin k → Id))
    (publicLaw : FiniteDistribution (K →ₗ[F2] R)) (β : ℝ)
    (hβ : 0 ≤ β) (hβ' : β ≤ 1) (s : FullSeed k Id K W R) :
    (fullSeedLaw (V := K × W) occurrences publicLaw β hβ hβ').weight s =
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.FullSeed, OAI.MaxCutGames.Decoder.AdviceLaw.fullSeedLaw

  65. theorem OAI.MaxCutGames.Decoder.AdviceLaw.fullSeed_weight_fiber line 700