OAI/Computability/MaxCut/PCP/PreprocessingRegularBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Bounds on the actual output prefixes used by the regularization loops. The bounds include the stored headers and all earlier original/owner blocks. They concern actual serialized words; machine executions are proved separately.

  1. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.offset_succ line 15
  2. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.blocksPrefix_length_le line 23
  3. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.header line 29
  4. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.ownerBits line 32
  5. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix line 37
  6. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix line 42
  7. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix line 48
  8. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix_length_le line 56
  9. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix_length_le line 64
  10. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix_length_le line 75
  11. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.regular_originalPrefix_le line 89
  12. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.regular_ownerPrefix_le line 96
  13. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.regular_dummyPrefix_le line 103
  14. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.visits_le_input line 112

    Source documentation

    The number of original and dummy vertex visits is exactly the constructed vertex count; adding owner visits still gives a linear bound in input bits.

    theorem visits_le_input :
    t.darts + t.vertices + (∑ v, padding t v) + 1 ≤
      (ExpanderFamily.growth + 1) * PreprocessingMachineBounds.inputLength t + 1 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth, OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.inputLength

  15. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularBounds.sum_body_costs_le line 124

    Source documentation

    An elementary budget aggregation for the actual three finite loops. The per-call bounds must be supplied from the separately checked subprogram runs.

    theorem sum_body_costs_le (old : Fin t.darts → Nat) (owners : Fin t.vertices → Nat)
    (dummy : ∀ v : Fin t.vertices, Fin (padding t v) → Nat) (setup cap : Nat)
    (hs : setup ≤ cap) (ho : ∀ e, old e ≤ cap) (hv : ∀ v, owners v ≤ cap)
    (hd : ∀ v j, dummy v j ≤ cap) :
    setup + (∑ e, old e) + (∑ v, owners v) + (∑ v, ∑ j, dummy v j) ≤
      ((ExpanderFamily.growth + 1) * PreprocessingMachineBounds.inputLength t + 1) * cap := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth, OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.inputLength