OAI/Computability/UniqueGames/Reduction/AddressTupleBudget.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.radixBound line 15
2. def OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.magnitude line 17
3. def OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.magnitudePolynomial line 21
4. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.magnitudePolynomial_eval line 26
5. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.source_counts_le line 32
6. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.radix_le line 37
7. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.radix_le_magnitude line 44
8. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.capacity_le_magnitude line 51
9. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.field_length_le_magnitude line 59
10. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.canonicalValues_le line 63
11. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.loaded_fields_le_magnitude line 80
12. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.queryWords_lt_radix line 97

    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.UniqueGamesTheorem.Integration.AddressTupleLoaded.canonicalValues

13. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.queryWords_encoded_length_le_magnitude line 108
14. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.queryWords_digits_le_magnitude line 123
15. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.selected_values_bound line 138
16. def OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.rowPolynomial line 163

    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.UniqueGamesTheorem.Integration.NoiseTables.Table

17. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.eval_sum_constant line 168
18. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.selected_polynomial_eval line 177
19. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.rows_budget_le line 188
20. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.physicalField_le line 210
21. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.lengthSum_le_of_mem line 223
22. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.cleanup_budget_le line 237

    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.UniqueGamesTheorem.Integration.AddressTupleCleanup.budget

23. def OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.timePolynomial line 260

    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.UniqueGamesTheorem.Integration.NoiseTables.Table

24. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.timePolynomial_eval line 266
25. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.budget_le_timePolynomial line 273

    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.UniqueGamesTheorem.Integration.NoiseTables.Table, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.budget, OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.canonicalValues, OAI.UniqueGamesTheorem.Integration.AddressTupleBudget.timePolynomial