Real-BN input-sensitivity (the per-block composition enabler)

Composing the float bridge through a ResNet block chains each op as "float-op-at-float-input vs real-op-at-real-input". flatConvF_close, mul_close, add_close, relu_close all take an input-error hypothesis — but bnForward_close_of compares the float and real BN at the same input (it models only rounding). So block composition needs the missing piece: how the real bnForward moves when its input moves — its input-Lipschitz behavior.

This file proves that sensitivity chain over ℝ: mean (bnMean_input_close), variance (bnVar_input_close), and inverse-stddev (bnIstd_input_close, which reuses rsqrt_lipschitz). With these + the rounding wrappers, a per-block closeness |bnForwardF(float input) − bnForward(real input)| splits as rounding-at-fixed-input (bnForward_close_of) + input-shift (these), so the block chain is mechanical from here.

theorem Proofs.bnMean_abs_le {n : ℕ} (x : Vec n) {A : ℝ} (hn : 0 < n) (hA : ∀ (i : Fin n), |x i| ≤ A) : |bnMean n x| ≤ A

The real mean stays within the input range: |μ| ≤ A under |xᵢ| ≤ A.

theorem Proofs.bnMean_input_close {n : ℕ} (x y : Vec n) (hn : 0 < n) : |bnMean n x - bnMean n y| ≤ (∑ i : Fin n, |x i - y i|) / ↑n

Mean input-sensitivity. |μ(x) − μ(y)| ≤ (Σ|xᵢ−yᵢ|)/n.

theorem Proofs.bnVar_input_close {n : ℕ} (x y : Vec n) {A : ℝ} (hn : 0 < n) (hAx : ∀ (i : Fin n), |x i| ≤ A) (hAy : ∀ (i : Fin n), |y i| ≤ A) : |bnVar n x - bnVar n y| ≤ 8 * A * ((∑ i : Fin n, |x i - y i|) / ↑n)

Variance input-sensitivity. |σ²(x) − σ²(y)| ≤ 8A·(Σ|xᵢ−yᵢ|)/n under |xᵢ|,|yᵢ| ≤ A — each centered-square difference factors as ((cx)−(cy))·((cx)+(cy)), bounded by (|xᵢ−yᵢ|+δ)·4A with δ = (Σ|x−y|)/n the mean shift; the nδ = Σ|x−y| collapse gives the 8A constant.

theorem Proofs.bnIstd_input_close {n : ℕ} (x y : Vec n) {A ε : ℝ} (hn : 0 < n) (hε : 0 < ε) (hAx : ∀ (i : Fin n), |x i| ≤ A) (hAy : ∀ (i : Fin n), |y i| ≤ A) : |bnIstd n x ε - bnIstd n y ε| ≤ 8 * A * ((∑ i : Fin n, |x i - y i|) / ↑n) / (2 * ε * √ε)

Inverse-stddev input-sensitivity. |istd(x) − istd(y)| ≤ 8A·(Σ|xᵢ−yᵢ|)/n / (2ε√ε) — the variance shift pushed through rsqrt_lipschitz (both σ²+ε ≥ ε). The BN-input piece that, with the rounding bnIstd_close, the per-block composition needs.

theorem Proofs.bnIstd_abs_le {n : ℕ} (x : Vec n) {ε : ℝ} (hε : 0 < ε) : |bnIstd n x ε| ≤ 1 / √ε

|istd| ≤ 1/√ε (the ε-floor caps the inverse-stddev).

theorem Proofs.bnForward_input_close {n : ℕ} (x y : Vec n) {A ε γ β : ℝ} (hn : 0 < n) (hε : 0 < ε) (hAx : ∀ (i : Fin n), |x i| ≤ A) (hAy : ∀ (i : Fin n), |y i| ≤ A) (i : Fin n) : |bnForward n ε γ β x i - bnForward n ε γ β y i| ≤ |γ| * ((|x i - y i| + (∑ j : Fin n, |x j - y j|) / ↑n) * (1 / √ε) + 2 * A * (8 * A * ((∑ j : Fin n, |x j - y j|) / ↑n) / (2 * ε * √ε)))

BN forward input-sensitivity (the assembled real-BN input-Lipschitz). |bnForward x − bnForward y| per coordinate, under |xᵢ|,|yᵢ| ≤ A: the β cancels and γ·x̂ splits as (centered shift)·istd + centered·(istd shift), bounded via the mean shift δ = (Σ|x−y|)/n, |istd| ≤ 1/√ε, and bnIstd_input_close. The normalize stage of the real-BN input-Lipschitz; with the rounding bnForward_close_of, the per-block float composition is |bnForwardF(float) − bnForward(real)| ≤ rounding + this.