SourcePhysicalUnaryEndpoint.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A low-drop unary segment on the active mass path ends strictly before the terminal block and still has the positive mass required by the physical propagated-residual estimate.

theorem OAI.LipschitzHilbert.firstMassStop_unary_endpoint line 15
theorem OAI.LipschitzHilbert.AngularGrid.source_stopped_unary_endpoint line 30

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_selected_active_physical_unary_tail line 59

Source documentation

The active-path conditions supply the endpoint eligibility and positive mass in the actual propagated physical residual estimate. Its fixed reference subset omits the one terminal block.

theorem eventually_selected_active_physical_unary_tail
    (Cmass : ℝ) (hCmass : 0 ≤ Cmass) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (N : ℕ) (κ : Type) (Label : Fin N → Type) (Item : ∀ j, Label j → Type)
      [Fintype κ] [∀ j l, Fintype (Item j l)]
      (P : SourceLabeledLattice N κ Label Item)
      (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
      (t : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ)
      (v : ℝ×ℝ → ℝ) (test : ℝ×ℝ → EuclideanSpace ℂ κ)
      (T : ∀ j (l : P.labels j), Item j l → SlopeBox) (A : ℝ)
      (τ : Type*) (grid : AngularGrid) (tops : Finset τ)
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.AngularGrid