OAI/Computability/WLIdentification/Hardness.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.WLIdentification.FinitePresentation.MachineRealizer.compiledRealTypeFintype line 12

    Source documentation

    Factor the finite enumerations through the compiled type names so instance search does not repeatedly expand the entire cellular compiler.

    noncomputable instance compiledRealTypeFintype (M : Machine) (d : ℕ) (w : Word) :
    Fintype (M.compiledCircuit d w).RealType := by infer_instance

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

  2. instance OAI.WLIdentification.FinitePresentation.MachineRealizer.compiledComparisonFintype line 15
  3. theorem OAI.WLIdentification.FinitePresentation.MachineRealizer.width_poly line 18
  4. theorem OAI.WLIdentification.FinitePresentation.MachineRealizer.inputSpan_lt_width line 23
  5. theorem OAI.WLIdentification.FinitePresentation.MachineRealizer.dimension_poly line 29
  6. def OAI.WLIdentification.FinitePresentation.MachineRealizer.compiled line 32
  7. theorem OAI.WLIdentification.FinitePresentation.MachineRealizer.wire_poly line 35
  8. def OAI.WLIdentification.FinitePresentation.MachineRealizer.ring line 38
  9. def OAI.WLIdentification.FinitePresentation.MachineRealizer.affine line 41
  10. def OAI.WLIdentification.FinitePresentation.MachineRealizer.uncolored line 44
  11. theorem OAI.WLIdentification.FinitePresentation.MachineRealizer.graph_isomorphic line 46
  12. theorem OAI.WLIdentification.FinitePresentation.MachineRealizer.graph_nonempty line 50
  13. def OAI.WLIdentification.FinitePresentation.MachineRealizer.output line 58
  14. theorem OAI.WLIdentification.FinitePresentation.MachineRealizer.output_poly line 61
  15. theorem OAI.WLIdentification.FinitePresentation.MachineRealizer.output_correct line 64
  16. theorem OAI.WLIdentification.dimensionLanguage_hard line 75

    Source documentation

    The reduction is an actual polynomial-time tape transducer. Relabeling is by effective rank/select on polynomial finite coding families, not by an arbitrary Fintype enumeration. Its semantic conclusion retains all graph mates.

    theorem dimensionLanguage_hard : ∀ L : BinaryLanguage, InEXPTIME L → PolytimeManyOne L dimensionLanguage := by
…

    Mentions: OAI.WLIdentification.BinaryLanguage, OAI.WLIdentification.InEXPTIME, OAI.WLIdentification.PolytimeManyOne, OAI.WLIdentification.dimensionLanguage