OAI/Computability/WLIdentification/MachineReduction.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.Machine.actionConfig line 10
  2. theorem OAI.WLIdentification.Machine.step_action line 16
  3. theorem OAI.WLIdentification.Machine.displacement_bound line 22
  4. theorem OAI.WLIdentification.Machine.run_succ line 25
  5. theorem OAI.WLIdentification.Machine.head_bound line 28
  6. structure OAI.WLIdentification.Machine.RingAgrees line 39
  7. theorem OAI.WLIdentification.Machine.initial_ringAgrees line 44
  8. theorem OAI.WLIdentification.Machine.RingAgrees.step line 61
  9. theorem OAI.WLIdentification.Machine.run_ringAgrees line 91
  10. theorem OAI.WLIdentification.Machine.ringRun_halted line 101
  11. theorem OAI.WLIdentification.Machine.compiledCircuit_run line 110
  12. theorem OAI.WLIdentification.AffineBlocks.graph_nonempty line 129
  13. def OAI.WLIdentification.ProductCircuit.outputGraph line 141

    Source documentation

    The fixed-width output construction, with private-wire length absorbed.

    noncomputable def outputGraph (hr : 32 ≤ r) : Graph :=
…

    Mentions: OAI.WLIdentification.Graph

  14. theorem OAI.WLIdentification.ProductCircuit.outputGraph_correct line 144
  15. theorem OAI.WLIdentification.ProductCircuit.outputGraph_nonempty line 147
  16. def OAI.WLIdentification.Machine.paddedExponent line 161
  17. def OAI.WLIdentification.Machine.addressWidth line 163
  18. def OAI.WLIdentification.Machine.reductionDimension line 165
  19. theorem OAI.WLIdentification.Machine.reductionDimension_ge line 167
  20. theorem OAI.WLIdentification.Machine.compiledCircuit_decides line 171
  21. def OAI.WLIdentification.Machine.reductionGraph line 189
  22. theorem OAI.WLIdentification.Machine.reductionGraph_correct line 194
  23. theorem OAI.WLIdentification.Machine.reductionGraph_nonempty line 200
  24. def OAI.WLIdentification.binaryWord line 208

    Source documentation

    Canonical most-significant-first binary representation.

    def binaryWord (n : ℕ) : Word := n.bits.reverse

    Mentions: OAI.WLIdentification.Word

  25. theorem OAI.WLIdentification.binaryValue_append_bit line 210
  26. theorem OAI.WLIdentification.binaryValue_binaryWord line 214
  27. theorem OAI.WLIdentification.binaryWord_leading line 223
  28. theorem OAI.WLIdentification.unary_frame_injective line 239

    Source documentation

    The order header is genuinely uniquely parsable, including order zero.

    theorem unary_frame_injective {n m : ℕ} {s t : Word}
    (h : List.replicate n true ++ false :: s = List.replicate m true ++ false :: t) :
    n = m ∧ s = t := by
…

    Mentions: OAI.WLIdentification.Word

  29. theorem OAI.WLIdentification.split_matrix_length line 256
  30. theorem OAI.WLIdentification.matrixWord_length line 260
  31. theorem OAI.WLIdentification.split_matrix_injective line 263
  32. theorem OAI.WLIdentification.Graph.ext line 276
  33. theorem OAI.WLIdentification.inputWord_injective line 286
  34. theorem OAI.WLIdentification.inputWord_mem_iff line 305

    Source documentation

    Correctness of serialization includes exclusion of every malformed alternative parse.

    theorem inputWord_mem_iff (G : Graph) (hn : 0 < G.order) (k : ℕ) (hk : 0 < k) :
    inputWord G (binaryWord k) ∈ dimensionLanguage ↔ WLdim G ≤ k := by
…

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.inputWord, OAI.WLIdentification.binaryWord, OAI.WLIdentification.dimensionLanguage, OAI.WLIdentification.WLdim

  35. def OAI.WLIdentification.Machine.reductionWord line 318

    Source documentation

    The literal binary output of the compressed-computation graph reduction. The separate cost obligation is a genuine ComputesWithin statement.

    noncomputable def reductionWord (M : Machine) (C e : ℕ) (w : Word) : Word :=
…

    Mentions: OAI.WLIdentification.Machine, OAI.WLIdentification.Word

  36. theorem OAI.WLIdentification.Machine.reductionWord_correct line 321