Stop-Loss Weak Curvature

Abstract

The weak second derivative of a finite stop-loss profile is its weighted atomic divisor; tail integrals and depth derivatives describe transport.

Theorem 1.1 (Weak curvature of one kink).

$$\begin{array}{r}\forall \delta :\mathbb{R},\phi :\mathbb{R}\to \mathbb{R},\\ \mathrm{ContDiff}\left(\mathbb{R},2,\phi \right)\wedge \mathrm{HasCompactSupport}\left(\phi \right)\Rightarrow \\ {\int }_{x\in \mathbb{R}}\mathrm{activePoleHeight}\left(\delta ,x\right)\cdot \mathrm{deriv}\left(\mathrm{deriv}\left(\phi \right)\right)\left(x\right)dx=\phi \left(\delta \right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ObserverCriteria/StopLossWeakCurvature.active_pole_height_weak_curvature (✓ std3). ∎

Source. Repository-derived.

Commentary.

The primitive is the product of distance minus position with the first test derivative, plus the test itself. Its derivative cancels the first-derivative terms. Restricting the kink to its lower half-line and applying compact-support FTC leaves the test value at the pole.

Theorem 1.2 (Weak curvature of the finite defect product).

$$\begin{array}{r}\forall I:\mathrm{Type},[\mathrm{Fintype}\left(I\right)],\delta :I\to \mathbb{R},m:I\to \mathbb{N},\\ \forall \phi :\mathbb{R}\to \mathbb{R},\mathrm{ContDiff}\left(\mathbb{R},2,\phi \right)\wedge \mathrm{HasCompactSupport}\left(\phi \right)\Rightarrow \\ {\int }_{x\in \mathbb{R}}\mathrm{remainingDepth}\left(\delta ,m,x\right)\cdot \mathrm{deriv}\left(\mathrm{deriv}\left(\phi \right)\right)\left(x\right)dx=\sum _{j:I}(m\left(j\right):\mathbb{R})\cdot \phi \left(\delta \left(j\right)\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ObserverCriteria/StopLossWeakCurvature.remaining_depth_weak_curvature (✓ std3). ∎

Source. Repository-derived.

Commentary.

This finite-sum companion consumes the single-kink theorem. Compact support makes every weighted integrand integrable, so integral linearity gives the atomic evaluation sum for arbitrary C2 tests.

Theorem 1.3 (Tail transport and weak curvature).

$$\begin{array}{r}\forall I:\mathrm{Type},[\mathrm{Fintype}\left(I\right)],\delta :I\to \mathbb{R},m:I\to \mathbb{N},\\ \mathrm{let}R:\mathbb{R}\to \mathbb{R}:=\mathrm{remainingDepth}\left(\delta ,m\right),\\ N:\mathbb{R}\to \mathbb{R}:=(x:\mathbb{R}\mapsto (\mathrm{horizontalTailCount}\left(\delta ,m,x\right):\mathbb{R})),\\ A:\mathbb{R}\to \mathbb{R}\to \mathbb{R}:=\mathrm{doubleDepthDecay}\left(\delta ,m\right)\mathrm{in}\\ (\forall \omega :\mathbb{R},R\left(\omega \right)={\int }_{x\in \mathrm{Ioi}\left(\omega \right)}N\left(x\right)dx)\wedge \\ (\forall \omega y:\mathbb{R},0\le y\Rightarrow A\left(\omega ,y\right)=R\left(\omega \right)-R\left(\omega +y\right))\wedge \\ (\forall \omega y:\mathbb{R},0\le y\Rightarrow A\left(\omega ,y\right)={\int }_{\omega }^{\omega +y}N\left(x\right)dx)\wedge \\ (\forall \omega y:\mathbb{R},0<y\Rightarrow (\forall j:I,\omega +y\ne \delta \left(j\right))\Rightarrow \mathrm{deriv}\left((t:\mathbb{R}\mapsto A\left(\omega ,t\right))\right)\left(y\right)=N\left(\omega +y\right))\wedge \\ (\forall \omega y:\mathbb{R},0\le y\Rightarrow (\forall j:I,\omega \ne \delta \left(j\right))\Rightarrow (\forall j:I,\omega +y\ne \delta \left(j\right))\Rightarrow \mathrm{deriv}\left((t:\mathbb{R}\mapsto A\left(t,y\right))\right)\left(\omega \right)=N\left(\omega +y\right)-N\left(\omega \right))\wedge \\ (\forall \omega y:\mathbb{R},0<y\Rightarrow (\forall j:I,\omega \ne \delta \left(j\right))\Rightarrow (\forall j:I,\omega +y\ne \delta \left(j\right))\Rightarrow \mathrm{deriv}\left((t:\mathbb{R}\mapsto A\left(t,y\right))\right)\left(\omega \right)-\mathrm{deriv}\left((t:\mathbb{R}\mapsto A\left(\omega ,t\right))\right)\left(y\right)=-N\left(\omega \right))\wedge \\ (\forall \phi :\mathbb{R}\to \mathbb{R},\mathrm{ContDiff}\left(\mathbb{R},2,\phi \right)\wedge \mathrm{HasCompactSupport}\left(\phi \right)\Rightarrow {\int }_{x\in \mathbb{R}}R\left(x\right)\cdot \mathrm{deriv}\left(\mathrm{deriv}\left(\phi \right)\right)\left(x\right)dx=\sum _{j:I}(m\left(j\right):\mathbb{R})\cdot \phi \left(\delta \left(j\right)\right))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ObserverCriteria/StopLossWeakCurvature.stop_loss_transport_and_weak_curvature (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed local notation expands the canonical ObservationDepthStopLoss functions. Natural tail counts and multiplicities are cast to real numbers when integrated.

Source provenance: the observation-layer transport theorem in the observer-adelic-completion-constant-theory input. Its seven displayed identities are public here. Positive pole distances are not needed. This companion consumes the finite weak-curvature theorem. Recovery of arbitrary measures from distributions remains a separate prerequisite and is not a conclusion.

References

• Truth anchor: D5/S3/Zeros/ObserverCriteria/StopLossWeakCurvature.active_pole_height_weak_curvature
• Truth anchor: D5/S3/Zeros/ObserverCriteria/StopLossWeakCurvature.remaining_depth_weak_curvature
• Truth anchor: D5/S3/Zeros/ObserverCriteria/StopLossWeakCurvature.stop_loss_transport_and_weak_curvature
• Dependency: D5/S3/Zeros/ObservationDepthStopLoss