OAI/Computability/UniqueGames/Reduction/AddressOutcomeSpecs.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.Spec line 14
2. abbrev OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.Values line 15
3. abbrev OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.Parameter line 16
4. def OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.bitVector line 20
5. def OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.rightMap line 22
6. def OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.row line 25
7. def OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.rows line 33
8. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.row_left_length line 37
9. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.row_right_length line 41
10. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.rows_length line 45
11. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.selected_rows line 49
12. def OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.interpreted line 57

    Source documentation

    A total proof-side interpretation. The fallback handles arbitrary malformed static specs; actual canonical rows always take the checked decoding branch.

    def interpreted (width : Nat) (bits : List Bool) : {words : List Nat // words.length = width} :=
    …

13. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.interpreted_encoded line 62
14. def OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.values line 66
15. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.row_left_output line 76
16. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.row_right_output line 82
17. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.values_row_left line 88
18. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.values_row_right line 96
19. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.correct_rows line 104
20. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.payload_row line 120
21. def OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.rhsBits line 129
22. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.bitVector_rhsBits line 132
23. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.rightMap_actual line 135
24. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.payload_row_actual line 141

    Source documentation

    Each static row emits exactly the concrete game's constraint encoding.

    theorem payload_row_actual (S : Source) (k : Nat) {s d : Nat}
        (T : NoiseTables.Table s d) (U : ActualGame.Question S k) (p : Parameter k T) :
        MachineOutcomeRows.payload
            (CanonicalAddress.base S.variables S.occurrences s d) (AddressGame.bodyCapacity S k s d)
            (values (CanonicalBodyTemplate.sourceFields U (ActualGame.names S)))
            (row T p (rhsBits S U)) =
          encodeWords (constraintWords (AddressGame.addressEdge S k (TableReduction.tableSkeleton T)
            (FixedOutcomes.assemble U p))) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.Question, OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.Parameter, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.payload, OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.base, OAI.UniqueGamesTheorem.Reduction.AddressGame.bodyCapacity, OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.values, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.sourceFields, OAI.UniqueGamesTheorem.Reduction.ActualGame.names, OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.row, OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.rhsBits, OAI.UniqueGamesTheorem.Reduction.AddressGame.addressEdge, OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.assemble

25. def OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.tupleBits line 153
26. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.tuplePayload_actual line 159
27. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.encodeWords_flatMap line 170
28. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.gameBits_factor line 178

    Source documentation

    Complete output-byte factorization used by the actual outer loop.

    theorem gameBits_factor (S : Source) (k : Nat) {s d : Nat} (T : NoiseTables.Table s d) :
        gameBits (AddressGame.tableOutput S k T) =
          encodeWords [(AddressGame.tableOutput S k T).vertices, 2^s,
            (AddressGame.tableOutput S k T).constraints.length] ++
          (FixedOutcomes.occurrenceTuples S.occurrences k).flatMap (tupleBits S k T) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressGame.tableOutput, OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.occurrenceTuples, OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.tupleBits