OAI/Computability/WLIdentification/CircuitReduction.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WLIdentification.ProductCircuit.primaryTruth line 10
2. abbrev OAI.WLIdentification.ProductCircuit.primarySet line 15
3. abbrev OAI.WLIdentification.ProductCircuit.sourceTruth line 18
4. abbrev OAI.WLIdentification.ProductCircuit.targetTruth line 26
5. def OAI.WLIdentification.ProductCircuit.rejectConstant line 34
6. theorem OAI.WLIdentification.ProductCircuit.source_truth_image line 38
7. theorem OAI.WLIdentification.ProductCircuit.target_truth_image line 60
8. theorem OAI.WLIdentification.ProductCircuit.source_implies_target line 72
9. def OAI.WLIdentification.ProductCircuit.rejectDestination line 83
10. theorem OAI.WLIdentification.ProductCircuit.rejectDestination_nonempty line 87
11. theorem OAI.WLIdentification.ProductCircuit.rejectDestination_true line 91
12. def OAI.WLIdentification.ProductCircuit.rejectBuffer line 101
13. theorem OAI.WLIdentification.ProductCircuit.rejectBuffer_nonempty line 105
14. theorem OAI.WLIdentification.ProductCircuit.rejectBuffer_projection line 113
15. theorem OAI.WLIdentification.ProductCircuit.rejectBuffer_sum line 122
16. def OAI.WLIdentification.ProductCircuit.rejectingImages line 136

    Source documentation

    Rejection produces actual nonempty scalar-image sets, including correlated buffers. This does not assert an unavailable simultaneous global assignment.

    noncomputable def rejectingImages (h : ¬ C.Accepted) : C.schemas.SpecialImages C.rejectConstant where
    …

17. theorem OAI.WLIdentification.Marker.sum_delta line 171
18. theorem OAI.WLIdentification.ComparisonSchemas.linkShift_special line 189
19. theorem OAI.WLIdentification.ComparisonSchemas.wireShift_special line 195
20. theorem OAI.WLIdentification.ProductCircuit.special_not_isomorphic line 208
21. theorem OAI.WLIdentification.ProductCircuit.not_identifies_of_rejected line 243

    Source documentation

    Rejection prevents identification for the full least-closure product circuit, not only for a promised selection of comparison mates.

    theorem not_identifies_of_rejected (hr : 32 ≤ r) (n : ℕ) (hn : r + 1 < n)
        (h : ¬ C.Accepted) : ¬ Identifies r (((C.schemas.layout n).affine (by omega)).graph 0) := by
    …

    Mentions: OAI.WLIdentification.Identifies

22. theorem OAI.WLIdentification.ProductCircuit.identifies_iff_accepted line 249
23. theorem OAI.WLIdentification.tupleColor_zero_eq line 260

    Source documentation

    Retained color history always determines the original atomic type.

    theorem tupleColor_zero_eq {G H : Graph} {k s : ℕ}
        {v : Fin k → Fin G.order} {w : Fin k → Fin H.order}
        (h : tupleColor G k s v = tupleColor H k s w) :
        tupleColor G k 0 v = tupleColor H k 0 w := by
    …

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.tupleColor

24. theorem OAI.WLIdentification.tupleColor_atomic line 268
25. def OAI.WLIdentification.restrictTupleColor line 278

    Source documentation

    Restricting a joint color retains an entire replacement vector at once.

    def restrictTupleColor {j k : ℕ} (q : Fin j → Fin k) :
        (s : ℕ) → TupleColor k s → TupleColor j s
      | 0, c => (fun i l => c.1 (q i) (q l), fun i l => c.2 (q i) (q l))
      | s + 1, c => (restrictTupleColor q s c.1,
          c.2.map (fun v i => restrictTupleColor q s (v (q i))))

    Mentions: OAI.WLIdentification.TupleColor

26. theorem OAI.WLIdentification.restrictTupleColor_apply line 284
27. def OAI.WLIdentification.padIndex line 301
28. theorem OAI.WLIdentification.padIndex_castLE line 304
29. def OAI.WLIdentification.paddedEquiv line 308
30. theorem OAI.WLIdentification.tupleHistogram_dimension_mono line 318
31. theorem OAI.WLIdentification.neighborColor_of_tupleColor line 338

    Source documentation

    Ordinary neighbor refinement is recoverable from any joint dimension >=2.

    theorem neighborColor_of_tupleColor {G H : Graph} {k : ℕ} (hk : 2 ≤ k) (s : ℕ)
        {v : Fin k → Fin G.order} {w : Fin k → Fin H.order}
        (h : tupleColor G k s v = tupleColor H k s w) (i : Fin k) :
        neighborColor G s (v i) = neighborColor H s (w i) := by
    …

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.tupleColor, OAI.WLIdentification.neighborColor

32. theorem OAI.WLIdentification.neighborHistogram_of_tupleHistogram line 368
33. theorem OAI.WLIdentification.equivalent_dimension_mono line 380
34. theorem OAI.WLIdentification.identifies_dimension_mono line 392
35. theorem OAI.WLIdentification.identifies_order line 398

    Source documentation

    A finite graph has a positive identifying dimension without any restriction on the order of its candidate mate.

    theorem identifies_order (G : Graph) : Identifies (max 2 G.order) G := by
    …

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Identifies

36. theorem OAI.WLIdentification.positive_identifying_nonempty line 410
37. theorem OAI.WLIdentification.WLdim_spec line 414
38. theorem OAI.WLIdentification.WLdim_le_iff line 417
39. theorem OAI.WLIdentification.ProductCircuit.dimension_iff_accepted line 426