OAI/Analysis/BoxTransport/Routing.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Effective realization of every balanced finite box instruction.

  1. theorem OAI.BoxTransport.Routing.Computation.representable_stageSwitch line 16
  2. theorem OAI.BoxTransport.Routing.Computation.representable_routeCenters line 21
  3. theorem OAI.BoxTransport.Routing.Computation.representable_linearBlend line 26
  4. theorem OAI.BoxTransport.Routing.Computation.representable_routeScales line 32
  5. theorem OAI.BoxTransport.Routing.Computation.routeScales_separated_from_zero line 51
  6. theorem OAI.BoxTransport.Routing.Computation.time_partial_curve line 73
  7. theorem OAI.BoxTransport.Routing.Computation.representable_curve_deriv line 82
  8. theorem OAI.BoxTransport.Routing.Computation.representable_diagonalLogVelocity line 88
  9. theorem OAI.BoxTransport.Routing.Computation.representable_movingAffinePotential line 94
  10. theorem OAI.BoxTransport.Routing.Computation.representable_movingBoxCutoff line 109
  11. theorem OAI.BoxTransport.Routing.Computation.representable_familyPotential line 120
  12. theorem OAI.BoxTransport.Routing.Computation.representable_spatialCurl line 133
  13. theorem OAI.BoxTransport.Routing.Computation.representable_routedField line 146
  14. theorem OAI.BoxTransport.Routing.Computation.effective_routedField line 161
  15. theorem OAI.BoxTransport.Routing.balanced_box_routing line 172

    Distinct definitions of this name: ComparatorChallenges/BalancedBoxRouting.lean:84 (same statement text; different proof or body). Qualify references as OAI.BoxTransport.Routing.balanced_box_routing@path.