← Mathematical handbook

The normalization derivative and all four substitutions in Lemma 4.2

theorem Papers.Rockel2026XiBlest.normalizationMean_eq_clampedSquareMean (b : ℝ) : normalizationMean b = Verification.clampedSquareMean b

theorem Papers.Rockel2026XiBlest.normalizationMean_hasDerivAt (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) : HasDerivAt (normalizationMean b) (-b * (Verification.quadraticUpper b q - Verification.quadraticLower q)) q

theorem Papers.Rockel2026XiBlest.quadratic_switch_strict (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Ioo (-1 / b) 1) : Verification.quadraticLower q < Verification.quadraticUpper b q

The unclamped part of an interior normalization section has positive width.

theorem Papers.Rockel2026XiBlest.extremalQ_interior (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) (hv : ↑v ∈ Set.Ioo 0 1) : extremalQ b hb v ∈ Set.Ioo (-1 / b) 1

At every interior response threshold, the normalization inverse stays strictly inside its effective parameter interval.

theorem Papers.Rockel2026XiBlest.normalizationMean_deriv_neg_at_extremalQ (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) (hv : ↑v ∈ Set.Ioo 0 1) : deriv (normalizationMean b) (extremalQ b hb v) < 0

The inverse normalization has a nonzero slope wherever the response is strictly between zero and one.

noncomputable def Papers.Rockel2026XiBlest.extremalQExtension (b : ℝ) (hb : 0 < b) (v : ℝ) : ℝ

A real-domain extension of the source normalization inverse. On the interior of the unit interval it agrees with the manuscript's q(v).

Equations

• Papers.Rockel2026XiBlest.extremalQExtension b hb v = Papers.Rockel2026XiBlest.extremalQ b hb ⟨Verification.unitClamp v, ⋯⟩

theorem Papers.Rockel2026XiBlest.extremalQExtension_coe (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : extremalQExtension b hb ↑v = extremalQ b hb v

theorem Papers.Rockel2026XiBlest.extremalQExtension_hasDerivAt (b : ℝ) (hb : 0 < b) (v : ℝ) (hv : v ∈ Set.Ioo 0 1) : HasDerivAt (extremalQExtension b hb) (-b * (Verification.quadraticUpper b (extremalQExtension b hb v) - Verification.quadraticLower (extremalQExtension b hb v)))⁻¹ v

The manuscript's inverse normalization parameter is differentiable at every interior response threshold, with an explicit reciprocal slope.

theorem Papers.Rockel2026XiBlest.extremalQExtension_density_coefficient (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) (hv : ↑v ∈ Set.Ioo 0 1) : -b * deriv (extremalQExtension b hb) ↑v = 1 / (Verification.quadraticUpper b (extremalQ b hb v) - Verification.quadraticLower (extremalQ b hb v))

The coefficient -b q'(v) in the revised density formula equals the reciprocal length of the unclamped conditional-density band.

theorem Papers.Rockel2026XiBlest.quadratic_active_interval_integral (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) : (∫ (x : ↑unitInterval), if 0 < b * (↑x ^ 2 - q) ∧ b * (↑x ^ 2 - q) < 1 then 1 else 0) = Verification.quadraticUpper b q - Verification.quadraticLower q

The active set in the clamped-square normalization has exact Lebesgue length given by the difference of its switch points.

theorem Papers.Rockel2026XiBlest.quadratic_closed_active_reflected_integral (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) : (∫ (u : ↑unitInterval), if 0 ≤ b * ((1 - ↑u) ^ 2 - q) ∧ b * ((1 - ↑u) ^ 2 - q) ≤ 1 then 1 else 0) = Verification.quadraticUpper b q - Verification.quadraticLower q

The reflected closed active strip has the same length: switching equalities occur only on two null square-level sets.

theorem Papers.Rockel2026XiBlest.quadratic_active_iff_switch (b q t : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) (ht : t ∈ Set.Ioo 0 1) : 0 < b * (t ^ 2 - q) ∧ b * (t ^ 2 - q) < 1 ↔ Verification.quadraticLower q < t ∧ t < Verification.quadraticUpper b q

Away from the unit-square edges, the strict clamped-square active condition is precisely the interval between the two switching points.

theorem Papers.Rockel2026XiBlest.substitution_upper (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) (hqneg : q ≤ 0) (hR : √(q + 1 / b) ≤ 1) : -(2 * √(q + 1 / b)) * deriv (normalizationMean b) q = 2 * b * √(q + 1 / b) ^ 2

Lemma 4.2(i), including the zero-radius endpoint.

theorem Papers.Rockel2026XiBlest.substitution_unclamped (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) (hqneg : q ≤ 0) (hR : 1 ≤ √(q + 1 / b)) : -(2 * √(q + 1 / b)) * deriv (normalizationMean b) q = 2 * b * √(q + 1 / b)

Lemma 4.2(ii).

theorem Papers.Rockel2026XiBlest.substitution_double (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) (hqpos : 0 ≤ q) (hR : √(q + 1 / b) ≤ 1) : -(2 * √(q + 1 / b)) * deriv (normalizationMean b) q = 1 + b * (√(q + 1 / b) - √q) ^ 2

Lemma 4.2(iii), including q=0.

theorem Papers.Rockel2026XiBlest.substitution_lower (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) (hqpos : 0 ≤ q) (hR : 1 ≤ √(q + 1 / b)) : -(2 * √q) * deriv (normalizationMean b) q = 2 * b * √q * (1 - √q)

Lemma 4.2(iv), including both boundary radii.