OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactMediator.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Explicit labels for the eighteen fresh sites of each three-stage mediator gadget. These identify the actual iterated graph with the nineteen-link contact geometry, rather than only matching their counts.

  1. abbrev OAI.ContinuumCoulomb.ContactMediator.LocalPath line 13
  2. abbrev OAI.ContinuumCoulomb.ContactMediator.LocalInternal line 14
  3. abbrev OAI.ContinuumCoulomb.ContactMediator.LocalSite line 15
  4. def OAI.ContinuumCoulomb.ContactMediator.spokeIndex line 17
  5. def OAI.ContinuumCoulomb.ContactMediator.pathIndex line 20
  6. def OAI.ContinuumCoulomb.ContactMediator.decodePath line 24
  7. def OAI.ContinuumCoulomb.ContactMediator.pathEquiv line 34
  8. theorem OAI.ContinuumCoulomb.ContactMediator.decodePath_pathIndex line 51
  9. theorem OAI.ContinuumCoulomb.ContactMediator.finProd_divNat line 55
  10. theorem OAI.ContinuumCoulomb.ContactMediator.finProd_modNat line 59
  11. def OAI.ContinuumCoulomb.ContactMediator.encodeSite line 63
  12. def OAI.ContinuumCoulomb.ContactMediator.decodeSite line 72
  13. theorem OAI.ContinuumCoulomb.ContactMediator.decode_encode line 95
  14. theorem OAI.ContinuumCoulomb.ContactMediator.encode_decode line 108
  15. def OAI.ContinuumCoulomb.ContactMediator.siteEquiv line 132
  16. def OAI.ContinuumCoulomb.ContactMediator.localToContact line 139
  17. def OAI.ContinuumCoulomb.ContactMediator.localOld line 154
  18. def OAI.ContinuumCoulomb.ContactMediator.localFirst line 155
  19. def OAI.ContinuumCoulomb.ContactMediator.localSecond line 156
  20. def OAI.ContinuumCoulomb.ContactMediator.localThird line 157
  21. def OAI.ContinuumCoulomb.ContactMediator.contactToLocal line 160
  22. theorem OAI.ContinuumCoulomb.ContactMediator.contact_local_inverse line 173
  23. theorem OAI.ContinuumCoulomb.ContactMediator.local_contact_inverse line 184
  24. def OAI.ContinuumCoulomb.ContactMediator.localContactEquiv line 190
  25. def OAI.ContinuumCoulomb.ContactMediator.localVertex line 196
  26. theorem OAI.ContinuumCoulomb.ContactMediator.localVertex_injective line 201
  27. abbrev OAI.ContinuumCoulomb.ContactMediator.LocalEdge line 217
  28. def OAI.ContinuumCoulomb.ContactMediator.encodeEdge line 219
  29. def OAI.ContinuumCoulomb.ContactMediator.decodeEdge line 228
  30. def OAI.ContinuumCoulomb.ContactMediator.edgeEquiv line 243
  31. def OAI.ContinuumCoulomb.ContactMediator.firstAttachment line 272
  32. def OAI.ContinuumCoulomb.ContactMediator.secondEndpoint line 275
  33. def OAI.ContinuumCoulomb.ContactMediator.localLeft line 282
  34. def OAI.ContinuumCoulomb.ContactMediator.localRight line 287
  35. theorem OAI.ContinuumCoulomb.ContactMediator.localEdge_contactLinked line 292
  36. theorem OAI.ContinuumCoulomb.ContactMediator.spoke_nonneg line 319
  37. theorem OAI.ContinuumCoulomb.ContactMediator.member_spoke line 323
  38. theorem OAI.ContinuumCoulomb.ContactMediator.member_nat line 327
  39. theorem OAI.ContinuumCoulomb.ContactMediator.member_secondPath line 330
  40. theorem OAI.ContinuumCoulomb.ContactMediator.finalGraph_left line 342

    Source documentation

    Every left endpoint of the actual three-stage graph has the explicit local gadget label. This identity retains the original edge index.

    theorem finalGraph_left {n r : ℕ} (F : Bonds n r) (W G : ℕ)
    (e : Fin r) (a : LocalEdge) :
    (finalGraph F W G).left (encodeEdge r e a) =
      localVertex (F.left e) (F.right e) e (localLeft (member (F.weight e)) a) := by
…

    Mentions: OAI.ContinuumCoulomb.ContactMediator.LocalEdge, OAI.ContinuumCoulomb.ContactMediator.encodeEdge, OAI.ContinuumCoulomb.ContactMediator.localVertex, OAI.ContinuumCoulomb.ContactMediator.localLeft

  41. theorem OAI.ContinuumCoulomb.ContactMediator.finalGraph_right line 367

    Source documentation

    The matching right-endpoint identity uses the proved nonnegativity of the actual rounded spokes, so later subdivisions always use member one.

    theorem finalGraph_right {n r : ℕ} (F : Bonds n r) (W G : ℕ)
    (e : Fin r) (a : LocalEdge) :
    (finalGraph F W G).right (encodeEdge r e a) =
      localVertex (F.left e) (F.right e) e (localRight a) := by
…

    Mentions: OAI.ContinuumCoulomb.ContactMediator.LocalEdge, OAI.ContinuumCoulomb.ContactMediator.encodeEdge, OAI.ContinuumCoulomb.ContactMediator.localVertex, OAI.ContinuumCoulomb.ContactMediator.localRight

  42. def OAI.ContinuumCoulomb.ContactMediator.edgeNegative line 381
  43. theorem OAI.ContinuumCoulomb.ContactMediator.member_edgeNegative line 383
  44. theorem OAI.ContinuumCoulomb.ContactMediator.finalGraph_contact_links line 389

    Source documentation

    The entire actual final edge enumeration, not just a graph with the same cardinality, is carried to the nineteen physical contact links.

    theorem finalGraph_contact_links {n r : ℕ} (F : Bonds n r) (_W _G : ℕ)
    (e : Fin r) (a : LocalEdge) :
    contactGadgetLinked (edgeNegative F e)
      (localToContact (localLeft (member (F.weight e)) a))
      (localToContact (localRight a)) := by
…

    Mentions: OAI.ContinuumCoulomb.ContactMediator.LocalEdge, OAI.ContinuumCoulomb.contactGadgetLinked, OAI.ContinuumCoulomb.ContactMediator.edgeNegative, OAI.ContinuumCoulomb.ContactMediator.localToContact, OAI.ContinuumCoulomb.ContactMediator.localLeft, OAI.ContinuumCoulomb.ContactMediator.localRight