Loss density stability on the original clock

Abstract

Strong derivative error and a separate terminal phase certificate control the full original output.

Let c<1/2, 0<a0. Both (k,chi) and (l,psi) are original controls at the same base (c,c,1-2c) and horizon T>=0, with k(0)=l(0)=a. Both heights stay in [eta,c-eta]. For every t in [0,T], assume |k(t)-l(t)|<=delta. All integrals are Lebesgue integrals on (0,T], with their norm taken before integration. The original regularity alternatives imply absolute continuity and integrability of the derivatives; no common partition or derivative supremum bound is assumed.

Write e=derivativeError(T,k,l)=integral |k prime-l prime|, M=variation(T,l)=integral |l prime|, and D=variation(T,k)=integral |k prime|. Absolute continuity identifies these variations with total variation. Define budget(eta,delta,e,M)=B=e/eta+M delta/eta^2. The five original probabilities have slopes sigma=(1,-1,0,-1,1), in mode order 0,1,2,3,13. Every mode remains in the loss output, including constant-probability mode 2 and mode 13 at index four.

Theorem 1.1 (Pointwise hazard error).

$\forall c \in R e a l, e t a \in R e a l, t \in R e a l, k \in Function (R e a l, R e a l), l \in Function (R e a l, R e a l), (positive (e t a) \land pointwisePairMargin (t, e t a, c, k, l)) \Rightarrow absHazardDifference (c, k, l, t) \leq absDerivativeDifference (k, l, t) / e t a + absDerivative (l, t) absHeightDifference (k, l, t) / square (e t a)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.hazard_pointwise_error (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any two differentiable-value functions k,l and any real t at which both heights lie in [eta,c-eta], |hazard_k(t)-hazard_l(t)|<=|k prime(t)-l prime(t)|/eta+|l prime(t)| |k(t)-l(t)|/eta^2. The assertion is pointwise for totalized derivatives. The velocity dependence is continuous piecewise linear, and changing a reciprocal height costs at most the height error divided by eta squared.

Theorem 1.2 (Accumulated hazard error).

$\forall c \in R e a l, T \in R e a l, e t a \in R e a l, d e lt a \in R e a l, k \in Function (R e a l, R e a l), c hi \in Function (R e a l, R e a l), l \in Function (R e a l, R e a l), p s i \in Function (R e a l, R e a l), (positive (e t a) \land ((OriginalControl (base (c), T, k, c hi) \land OriginalControl (base (c), T, l, p s i)) \land (uniformPairMargin (T, e t a, c, k, l) \land uniformHeightErrorLe (T, k, l, d e lt a)))) \Rightarrow integralAbsHazardDifference (c, T, k, l) \leq budget (e t a, d e lt a, derivativeError (T, k, l), variation (T, l))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.hazard_integral_error (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under the common margin and height-error hypotheses, integral_0^T |hazard_k-hazard_l|<=B. The proof integrates the pointwise bound using the actual L1 derivative difference and the variation of l.

Theorem 1.3 (Every survival prefix uses the full hazard error).

$\forall c \in R e a l, T \in R e a l, t \in R e a l, k \in Function (R e a l, R e a l), c hi \in Function (R e a l, R e a l), l \in Function (R e a l, R e a l), p s i \in Function (R e a l, R e a l), ((OriginalControl (base (c), T, k, c hi) \land OriginalControl (base (c), T, l, p s i)) \land inIcc (t, 0, T)) \Rightarrow absSurvivalDifference (c, k, l, t) \leq integralAbsHazardDifference (c, T, k, l)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.survival_integral_error (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any two original controls and every t in [0,T], |S_k(t)-S_l(t)|<=integral_0^T |hazard_k-hazard_l|. No margin hypothesis is needed for this intermediate assertion. The hazard primitives are nonnegative; exp(-x) is one-Lipschitz for x>=0.

Theorem 1.4 (Uniform survival error).

$\forall c \in R e a l, T \in R e a l, e t a \in R e a l, d e lt a \in R e a l, t \in R e a l, k \in Function (R e a l, R e a l), c hi \in Function (R e a l, R e a l), l \in Function (R e a l, R e a l), p s i \in Function (R e a l, R e a l), ((positive (e t a) \land ((OriginalControl (base (c), T, k, c hi) \land OriginalControl (base (c), T, l, p s i)) \land (uniformPairMargin (T, e t a, c, k, l) \land uniformHeightErrorLe (T, k, l, d e lt a)))) \land inIcc (t, 0, T)) \Rightarrow absSurvivalDifference (c, k, l, t) \leq budget (e t a, d e lt a, derivativeError (T, k, l), variation (T, l))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.survival_error (✓ std3). ∎

Source. Repository-derived.

Commentary.

The accumulated hazard estimate therefore gives |S_k(t)-S_l(t)|<=B for every t in [0,T] under the common margin and height-error assumptions.

Theorem 1.5 (The exact loss-density estimate IS.28).

$\forall c \in R e a l, a \in R e a l, T \in R e a l, e t a \in R e a l, d e lt a \in R e a l, k \in Function (R e a l, R e a l), c hi \in Function (R e a l, R e a l), l \in Function (R e a l, R e a l), p s i \in Function (R e a l, R e a l), i \in F in F i v e, (cLessHalf (c) \land (initialInterior (a, c) \land (positive (e t a) \land ((OriginalControl (base (c), T, k, c hi) \land OriginalControl (base (c), T, l, p s i)) \land (uniformPairMargin (T, e t a, c, k, l) \land uniformHeightErrorLe (T, k, l, d e lt a)))))) \Rightarrow integralAbsLossDensityDifference (c, a, T, k, l, i) \leq (1 + variation (T, l) / e t a + variation (T, k)) budget (e t a, d e lt a, derivativeError (T, k, l), variation (T, l)) + d e lt a + derivativeError (T, k, l)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.loss_density_error (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every original mode i, integral_0^T |lossDensity_i(k)-lossDensity_i(l)|<=(1+M/eta+D)B+delta+e. lossDensity_i is the original unnormalized source-family density, modeCoefficient_i p_i(a); OriginalReferenceOutputMeasure.source_coefficient identifies it with the source failureDensity, and native_coefficient_deriv identifies it almost everywhere with minus the derivative of S p_i(k). No common initial-height equality is needed for this scalar estimate itself.

Product differentiation gives the four differences -(S_k prime-S_l prime)p_i(k), -S_l prime(p_i(k)-p_i(l)), -(S_k-S_l)sigma_i k prime, and -S_l sigma_i(k prime-l prime). Their integrated absolute values are bounded by (1+M/eta)B, delta, DB and e. Here integral |S_k prime-S_l prime|<=(1+M/eta)B follows from S prime=-hazard S and integral hazard_l<=M/eta. Monotone survival gives integral |S_l prime|=1-S_l(T)<=1. Each p_i is at most one, each probability coordinate is one-Lipschitz, and |sigma_i|<=1. This proves the displayed constants for all five modes.

Theorem 1.6 (No additional speed hypothesis is required).

$\forall c \in R e a l, T \in R e a l, k \in Function (R e a l, R e a l), c hi \in Function (R e a l, R e a l), l \in Function (R e a l, R e a l), p s i \in Function (R e a l, R e a l), (OriginalControl (base (c), T, k, c hi) \land OriginalControl (base (c), T, l, p s i)) \Rightarrow variation (T, k) \leq variation (T, l) + derivativeError (T, k, l)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.variation_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

Theorem 1.7 (The full complete-output estimate).

$\forall c \in R e a l, a \in R e a l, T \in R e a l, e t a \in R e a l, d e lt a \in R e a l, k \in Function (R e a l, R e a l), c hi \in Function (R e a l, R e a l), l \in Function (R e a l, R e a l), p s i \in Function (R e a l, R e a l), ((cLessHalf (c) \land (initialInterior (a, c) \land ((OriginalControl (base (c), T, k, c hi) \land OriginalControl (base (c), T, l, p s i)) \land (evaluate (k, 0) = a \land evaluate (l, 0) = a)))) \land (positive (e t a) \land (uniformPairMargin (T, e t a, c, k, l) \land uniformHeightErrorLe (T, k, l, d e lt a)))) \Rightarrow completeOperationalDistance (c, a, T, k, c hi, l, p s i) \leq rootBudget (c, a, budget (e t a, d e lt a, derivativeError (T, k, l), variation (T, l)), d e lt a) + phaseError (c, T, k, c hi, l, p s i) + densityBudget (c, a, e t a, d e lt a, derivativeError (T, k, l), variation (T, l), variation (T, k), budget (e t a, d e lt a, derivativeError (T, k, l), variation (T, l)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.complete_error_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Put d_min=initialFloor(c,a)=min(a,c-a,1-2c)>0 and C=(1+M/eta+D)B+delta+e. For the actual complete operational distance of OriginalCompleteOutputStability, d_op<=sqrt((B+delta)/d_min)+phaseError+C/(2 d_min). phaseError=max_i |character_i(k,chi,T)-character_i(l,psi,T)| is a separate terminal character certificate. In the display, rootBudget=sqrt((B+delta)/d_min) and densityBudget=C/(2 d_min). The result combines the complete joint-output estimate IS.27, the loss-density estimate IS.28 and the terminal Kraus estimate IS.29, on the same common data.

Theorem 1.8 (A common initial height gives uniform height control).

$\forall c \in R e a l, T \in R e a l, t \in R e a l, k \in Function (R e a l, R e a l), c hi \in Function (R e a l, R e a l), l \in Function (R e a l, R e a l), p s i \in Function (R e a l, R e a l), ((OriginalControl (base (c), T, k, c hi) \land OriginalControl (base (c), T, l, p s i)) \land (evaluate (k, 0) = evaluate (l, 0) \land inIcc (t, 0, T))) \Rightarrow absHeightDifference (k, l, t) \leq derivativeError (T, k, l)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.height_error_le_derivativeError (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any two original controls with k(0)=l(0), and every t in [0,T], |k(t)-l(t)|<=derivativeError(T,k,l). The fundamental theorem for absolutely continuous functions writes the difference as the integral of k prime-l prime on (0,t], which is bounded by the full L1 difference.

Theorem 1.9 (Convergence of the complete operational output).

$\forall c \in R e a l, a \in R e a l, T \in R e a l, e t a \in R e a l, M \in R e a l, k \in Sequence (Function (R e a l, R e a l)), c hi \in Sequence (Function (R e a l, R e a l)), l \in Sequence (Function (R e a l, R e a l)), p s i \in Sequence (Function (R e a l, R e a l)), (cLessHalf (c) \land (initialInterior (a, c) \land (positive (e t a) \land (allCommonOriginalControls (c, a, T, k, c hi, l, p s i) \land (allUniformPairMargins (T, e t a, c, k, l) \land (allVariationLe (T, l, M) \land (derivativeErrorsTendstoZero (T, k, l) \land terminalPhaseErrorsTendstoZero (c, T, k, c hi, l, p s i)))))))) \Rightarrow completeOperationalDistancesTendstoZero (c, a, T, k, c hi, l, p s i)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalDensityStability.complete_output_convergence (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix c,a,T,eta and a real bound M. Let (k_n,chi_n) and (l_n,psi_n) be two sequences of original controls on the common base and horizon, with both initial heights a and both heights in [eta,c-eta] for every n. Assume variation(T,l_n)<=M for every n, derivativeError(T,k_n,l_n) tends to zero, and phaseError(c,T,k_n,chi_n,l_n,psi_n) separately tends to zero. Then their completeOperationalDistance tends to zero, uniformly over all normalized positive joint trace-class inputs and unchanged Hilbert references in any fixed universe.

For convergence take delta_n=e_n, use D_n<=M+e_n and B_n=e_n/eta+M e_n/eta^2. The common initial probability floor is strictly positive. Continuity of the square root and the rational polynomial upper bound makes every term in the combined estimate tend to zero. Nonnegativity of the actual operational distance completes the squeeze argument. This proves a sufficient condition; it asserts neither necessity of derivative convergence nor acquisition of the phase certificate.

The actual output is the successful tensor Kraus congruence together with five Bochner failure-density measures on the same reference and physical time records. The result does not infer terminal phase control from height control, recover an intermediate phase waveform, grant access to old programme fields, construct an acquisition service, authorize a post-failure restart or establish physical realization.

References

Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.complete_error_bound
Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.complete_output_convergence
Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.hazard_integral_error
Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.hazard_pointwise_error
Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.height_error_le_derivativeError
Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.loss_density_error
Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.survival_error
Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.survival_integral_error
Truth anchor: D5/S3/Quantum/Fibers/OriginalDensityStability.variation_le
Dependency: D5/S3/Quantum/Fibers/OriginalCompleteOutputStability

Keyboard shortcuts

trureturing — Discovering truth

Loss density stability on the original clock

Abstract

References