OAI/Combinatorics/HoneycombCorridor/BridgeFiniteness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.finite_bridges_window line 11
  2. theorem OAI.PolynomialVacuumBridge.Corridor.bridge_finite_sum_word_bound line 25
  3. theorem OAI.PolynomialVacuumBridge.Corridor.bridge_weight_finite_sum_bound line 38
  4. theorem OAI.PolynomialVacuumBridge.Corridor.sourceExit_reaches_zero line 48
  5. theorem OAI.PolynomialVacuumBridge.Corridor.lateralLengthMass_zero line 56
  6. theorem OAI.PolynomialVacuumBridge.Corridor.bridge_length_finite_sum_bound line 65
  7. theorem OAI.PolynomialVacuumBridge.Corridor.bridge_weight_summable line 77
  8. theorem OAI.PolynomialVacuumBridge.Corridor.bridge_length_summable line 83
  9. theorem OAI.PolynomialVacuumBridge.Corridor.finite_bridge_sums line 91

    Distinct definitions of this name: ComparatorChallenges/HoneycombBridgeFiniteness.lean:60 (same statement text; different proof or body). Qualify references as OAI.PolynomialVacuumBridge.Corridor.finite_bridge_sums@path.