OAI/Computability/MaxCut/Games/OccurrenceTupleOrder.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate-order bridge from the checked tuple odometer to the outer reduction's occurrence enumeration. The odometer changes coordinate zero fastest; ActualEnumeration.functions changes it slowest. Reading saved digit j.rev as query coordinate j matches the complete ordered list. No primitive machine or assumed whole-loop runtime is introduced here.

  1. def OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.readCoordinates line 23

    Source documentation

    Read the physical saved digit positions in reverse coordinate order.

    def readCoordinates {m k : Nat} (digits : Fin k → Fin m) : Fin k → Fin m :=
…
  2. theorem OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.readCoordinates_apply line 26
  3. theorem OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.readCoordinates_involutive line 29
  4. def OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.coordinateEquiv line 34
  5. theorem OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.readCoordinates_snoc line 40
  6. theorem OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.tupleOrder_readCoordinates line 46

    Source documentation

    Exact equality of occurrence lists after reading saved digits in reverse coordinate order. This includes dimension zero and radix zero.

    theorem tupleOrder_readCoordinates (m k : Nat) :
    (MachineTupleOdometer.tupleOrder m k).map readCoordinates =
      ActualEnumeration.functions (List.finRange m) k := by
…

    Mentions: OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.readCoordinates, OAI.MaxCutGames.Reduction.ActualEnumeration.functions

  7. theorem OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.functions_readCoordinates line 71
  8. theorem OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.functions_flatMap line 80

    Source documentation

    An arbitrary exact emitted list, including serialized edge bytes, inherits the order identity. There is no permutation or counting-only replacement.

    theorem functions_flatMap (m k : Nat) (emit : (Fin k → Fin m) → List α) :
    (ActualEnumeration.functions (List.finRange m) k).flatMap emit =
      (MachineTupleOdometer.tupleOrder m k).flatMap
        (fun digits => emit (readCoordinates digits)) := by
…

    Mentions: OAI.MaxCutGames.Reduction.ActualEnumeration.functions, OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.readCoordinates

  9. theorem OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.actualSchedule_order line 95

    Source documentation

    Apply the coordinate readout to an existing actual odometer schedule. Its visit-order theorem already follows from the real nested-cycle constructors.

    theorem actualSchedule_order
    (tree : MachineTupleOdometer.NestedCycle m current remaining bodyLabel
      checkLabel resetLabel program k exitLabel start finish) :
    tree.order.map readCoordinates = ActualEnumeration.functions (List.finRange m) k := by
…

    Mentions: OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.readCoordinates, OAI.MaxCutGames.Reduction.ActualEnumeration.functions

  10. theorem OAI.MaxCutGames.Reduction.OccurrenceTupleOrder.actualSchedule_flatMap line 101
  11. def OAI.MaxCutGames.Integration.AddressTupleBudget.radixBound line 119
  12. def OAI.MaxCutGames.Integration.AddressTupleBudget.magnitude line 121
  13. def OAI.MaxCutGames.Integration.AddressTupleBudget.magnitudePolynomial line 125
  14. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.magnitudePolynomial_eval line 130
  15. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.source_counts_le line 136
  16. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.radix_le line 141
  17. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.radix_le_magnitude line 148
  18. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.capacity_le_magnitude line 155
  19. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.field_length_le_magnitude line 163
  20. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.canonicalValues_le line 167
  21. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.loaded_fields_le_magnitude line 184
  22. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.queryWords_lt_radix line 201

    Source documentation

    These are the actual canonical words, not arbitrary interpreted templates.

    theorem queryWords_lt_radix (F : SourceEncoding.Input)
    (tuple : Fin k → Fin F.equations.length) (X : ActualGame.Map k s d)
    (w : Nat) (hw : w ∈ AddressByteSemantics.queryWords
      (AddressTupleLoaded.canonicalValues F tuple) X
      (AddressOutcomeSpecs.bitVector (rhs F tuple))) :
    w < CanonicalAddress.base F.«variables» F.equations.length s d := by
…

    Mentions: OAI.MaxCutGames.Integration.AddressTupleLoaded.canonicalValues

  23. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.queryWords_encoded_length_le_magnitude line 212
  24. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.queryWords_digits_le_magnitude line 227
  25. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.selected_values_bound line 242
  26. def OAI.MaxCutGames.Integration.AddressTupleBudget.rowPolynomial line 267

    Source documentation

    Both canonical templates have exactly the same fixed token count.

    noncomputable def rowPolynomial (k : Nat) {s d : Nat} (T : NoiseTables.Table s d) :
    Polynomial Nat :=
…

    Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table

  27. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.eval_sum_constant_inline_AddressTupleBudget line 272
  28. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.selected_polynomial_eval line 281
  29. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.rows_budget_le line 292
  30. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.physicalField_le line 314
  31. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.lengthSum_le_of_mem_inline_AddressTupleBudget line 327
  32. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.cleanup_budget_le line 341

    Source documentation

    Cleanup sees only the four loaded fields per position; output is not scanned.

    theorem cleanup_budget_le (rows : Rows k) (B C : Nat)
    (values : MachineOutcomeRows.Spec (4*k) (1+9*k) → MachineOutcomeRows.Values (1+9*k))
    (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (base : Arena k s d noiseCount → List Bool) (ready : Ready F tuple base) :
    AddressTupleCleanup.budget k s d noiseCount (emitted rows B C values F tuple base) ≤
      4*k*((SourceEncoding.inputBits F).length+2) := by
…

    Mentions: OAI.MaxCutGames.Integration.AddressTupleCleanup.budget

  33. def OAI.MaxCutGames.Integration.AddressTupleBudget.timePolynomial line 364

    Source documentation

    Fixed program dimensions determine this explicit polynomial in input bits.

    noncomputable def timePolynomial (k : Nat) {s d : Nat} (T : NoiseTables.Table s d) :
    Polynomial Nat :=
…

    Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table

  34. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.timePolynomial_eval line 370
  35. theorem OAI.MaxCutGames.Integration.AddressTupleBudget.budget_le_timePolynomial line 377

    Source documentation

    Uniform bound for the actual tuple body, with all canonical values instantiated.

    theorem budget_le_timePolynomial (F : SourceEncoding.Input)
    (tuple : Fin k → Fin F.equations.length) (T : NoiseTables.Table s d)
    (base : Arena k s d noiseCount → List Bool) (ready : Ready F tuple base)
    (clean : MachineAddressEdge.Clean (Slots k s d noiseCount) base) :
    AddressTupleBody.budget (AddressOutcomeSpecs.rows k T)
      (CanonicalAddress.base F.«variables» F.equations.length s d)
      (AddressGame.bodyCapacity (source F) k s d)
      (AddressOutcomeSpecs.values (AddressTupleLoaded.canonicalValues F tuple)) F tuple base ≤
        (timePolynomial k T).eval (SourceEncoding.inputBits F).length := by
…

    Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table, OAI.MaxCutGames.Integration.AddressTupleBody.budget, OAI.MaxCutGames.Integration.AddressTupleLoaded.canonicalValues, OAI.MaxCutGames.Integration.AddressTupleBudget.timePolynomial

  36. def OAI.MaxCutGames.Integration.AddressTuplePolynomial.run_actual line 403
  37. theorem OAI.MaxCutGames.Integration.AddressTuplePolynomial.trace_actual line 432

    Source documentation

    The explicit iterated transition trace and its uniform bound, for callers that compose traces directly instead of runtime-witness structures.

    theorem trace_actual (T : NoiseTables.Table s d)
    (labels : AddressTupleBody.Label k s d noiseCount (AddressOutcomeSpecs.rows k T) → Λ)
    (exit : Option Λ)
    (P : Λ → TM2.Stmt (fun _ : AddressTupleBody.Arena k s d noiseCount => Bool) Λ (BodyState k))
    (atLabels : ∀ l, P (labels l) = instruction (AddressOutcomeSpecs.rows k T) labels exit l)
    (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (base : AddressTupleBody.Arena k s d noiseCount → List Bool) (ready : Ready F tuple base)
    (clean : MachineAddressEdge.Clean (Slots k s d noiseCount) base)
    (oldRhs : Fin k → Bool)
    (hB : base (headerTape k s d noiseCount .baseValue) =
      encodeWord (CanonicalAddress.base F.«variables» F.equations.length s d))
    (hC : base (headerTape k s d noiseCount .capacity) =
…

    Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table, OAI.MaxCutGames.Integration.AddressTupleBody.Label, OAI.MaxCutGames.Integration.AddressTupleBody.Arena

  38. theorem OAI.MaxCutGames.Reduction.OutputSize.explicitBodies_length_le line 476
  39. def OAI.MaxCutGames.Reduction.OutputSize.vertexCoefficient line 485
  40. def OAI.MaxCutGames.Reduction.OutputSize.edgeCoefficient line 488
  41. theorem OAI.MaxCutGames.Reduction.OutputSize.collect_vertex_coefficient_inline_OutputSize line 492
  42. theorem OAI.MaxCutGames.Reduction.OutputSize.collect_edge_coefficient_inline_OutputSize line 497
  43. theorem OAI.MaxCutGames.Reduction.OutputSize.output_vertices_le line 502
  44. theorem OAI.MaxCutGames.Reduction.OutputSize.output_constraints_eq line 516
  45. def OAI.MaxCutGames.Reduction.OutputSize.sizeBound line 523
  46. theorem OAI.MaxCutGames.Reduction.OutputSize.sizeBound_mono line 529
  47. theorem OAI.MaxCutGames.Reduction.OutputSize.output_bits_length_le line 541
  48. def OAI.MaxCutGames.Reduction.OutputSize.outputPolynomial line 556

    Source documentation

    An explicit polynomial for the actual serialized game.

    noncomputable def outputPolynomial (k : Nat) (T : NoiseTables.Table s d) : Polynomial Nat :=
…
  49. theorem OAI.MaxCutGames.Reduction.OutputSize.outputPolynomial_eval line 562
  50. theorem OAI.MaxCutGames.Reduction.OutputSize.output_bits_polynomial_in_occurrences line 567
  51. theorem OAI.MaxCutGames.Reduction.OutputSize.output_bits_polynomial_in_input line 575
  52. theorem OAI.MaxCutGames.Reduction.OutputSize.fixed_parameters_output_size line 585

    Source documentation

    Fixed reduction parameters give one polynomial for every encoded input.

    theorem fixed_parameters_output_size (k : Nat) (T : NoiseTables.Table s d) :
    ∃ p : Polynomial Nat, ∀ input : SourceEncoding.Input,
      (Complexity.gameBits
        (UniformReduction.output input.equations input.nonempty k T)).length ≤
          p.eval (SourceEncoding.inputBits input).length :=
…

    Mentions: OAI.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.UniformReduction.output, OAI.MaxCutGames.Reduction.SourceEncoding.inputBits

  53. def OAI.MaxCutGames.Reduction.AddressOutputSize.vertexBound line 602
  54. def OAI.MaxCutGames.Reduction.AddressOutputSize.edgeBound line 606
  55. def OAI.MaxCutGames.Reduction.AddressOutputSize.bitsBound line 609
  56. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.bitsBound_mono line 613
  57. def OAI.MaxCutGames.Reduction.AddressOutputSize.sizeBound line 621
  58. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.table_constraints_eq line 624
  59. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.scaled_sum_le_inline_AddressOutputSize line 632
  60. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.output_constraints_eq line 639
  61. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.output_vertices_le_input line 648
  62. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.output_constraints_le_input line 667
  63. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.output_bits_length_le line 676
  64. def OAI.MaxCutGames.Reduction.AddressOutputSize.outputPolynomial line 686

    Source documentation

    One fixed polynomial includes every declared address and every edge table.

    noncomputable def outputPolynomial (k : Nat) (T : NoiseTables.Table s d) : Polynomial Nat :=
…
  65. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.outputPolynomial_eval line 694
  66. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.output_bits_polynomial_in_input line 700
  67. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.fixed_parameters_output_size line 708
  68. def OAI.MaxCutGames.Reduction.AddressOutputSize.directVertexBound line 715
  69. def OAI.MaxCutGames.Reduction.AddressOutputSize.directEdgeCoefficient line 718
  70. def OAI.MaxCutGames.Reduction.AddressOutputSize.directSizeBound line 721
  71. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.direct_vertices_le_input line 725
  72. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.direct_constraints_eq line 741
  73. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.direct_constraints_le_input line 749
  74. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.direct_bits_length_le line 757
  75. def OAI.MaxCutGames.Reduction.AddressOutputSize.directOutputPolynomial line 766
  76. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.directOutputPolynomial_eval line 773
  77. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.direct_bits_polynomial_in_input line 779
  78. theorem OAI.MaxCutGames.Reduction.AddressOutputSize.fixed_parameters_direct_output_size line 787