Documentation

LeanMlir.Proofs.Training.TrainedLinearDescent

Descent at TRAINED weights (post_audit_roadmap §3) #

REDUCED CERTIFICATE MODEL — this file's concrete net is the 4×4-pooled 49-dim MNIST family (width-8 hidden, /128–/256 rational weights), NOT the canonical 784→512→512→10 mlpVerified; chosen so every margin/norm/SOS check is exact rational arithmetic in-kernel. Canonical surface: Proofs/MlpCanonical.lean.

binary32_linear_sgd_descends_concrete (the suite's only concrete descent instance) holds at the degenerate W = 0 net — a satisfiability witness. This file retires that caveat: one binary32 SGD step on a TRAINED, /128-rationalized bias-free 49→10 pooled-MNIST linear classifier (test acc 0.874) provably decreases the real cross-entropy loss, at MNIST test image #8 with learning rate 1/8192. The rounding model is the CONSTRUCTED rndP 23 grid (binary32), so the whole statement is axiom-free.

The trick that closes the descent window with zero exp evaluations: the witness sample is MISCLASSIFIED (true label 5, predicted 6), so z_5 ≤ z_6 is an exact rational inequality (hz_lbl_le) and exp-monotonicity alone gives softmax_5 ≤ 1/2 (sm_lbl_le_half) — whence the two gradient sums the window needs are bracketed by rationals: Σ|∇| ≤ 2·Σxᵢ (gradL1_le, softmax sums to 1) and Σ∇² ≥ (Σxᵢ²)/4 (gradSq_lower). The float-forward drift hδ is the proven dense_close_fresh budget evaluated exactly per class column (norm_num computes the exact (1+2⁻²⁴)⁵¹); the exp(2δ)−1 term inside cotErr is bounded by the γ-form exp_sub_one_le. Every hypothesis of linear_float_sgd_descends is discharged — nothing assumed.

Being misclassified also makes the guaranteed drop STRICTLY positive (trained_linear_sgd_strictly_descends): the loss drops by ≥ lr·(Σxᵢ²)/8 ≈ 6.93e-05. Generated by scripts/trained_linear_descent.py; weights/input are DATA.

noncomputable def Proofs.TrainedLinearDescent.Wd :

Mat 49 10

Trained linear weights (input×class, entries k/128), test acc 0.874.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.TrainedLinearDescent.bd :

Vec 10

Equations

Proofs.TrainedLinearDescent.bd x✝ = 0

Instances For

noncomputable def Proofs.TrainedLinearDescent.xd :

Vec 49

MNIST test image #8 (digit 5), 4×4-pooled exact pixel sums.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Proofs.TrainedLinearDescent.lblD :

Fin 10

Equations

Proofs.TrainedLinearDescent.lblD = 5

Instances For

def Proofs.TrainedLinearDescent.cD :

Fin 10

Equations

Proofs.TrainedLinearDescent.cD = 6

Instances For

theorem Proofs.TrainedLinearDescent.xd_nonneg (i : Fin 49) :

0 ≤ xd i

theorem Proofs.TrainedLinearDescent.xd_le_one (i : Fin 49) :

theorem Proofs.TrainedLinearDescent.xd_sum :

∑ i : Fin 49, xd i = 15367 / 2040

Σᵢ xᵢ exactly (all coordinates nonneg).

theorem Proofs.TrainedLinearDescent.xd_sq_sum :

∑ i : Fin 49, xd i ^ 2 = 1511461 / 332928

theorem Proofs.TrainedLinearDescent.hz_lbl_le :

dense Wd bd xd lblD ≤ dense Wd bd xd cD

The witness is misclassified: logit 5 ≤ logit 6, exactly.

theorem Proofs.TrainedLinearDescent.sm_pos (j : Fin 10) :

0 < softmax 10 (dense Wd bd xd) j

theorem Proofs.TrainedLinearDescent.sm_sum :

∑ j : Fin 10, softmax 10 (dense Wd bd xd) j = 1

theorem Proofs.TrainedLinearDescent.sm_lbl_le_half :

softmax 10 (dense Wd bd xd) lblD ≤ 1 / 2

Softmax at the true label ≤ 1/2 — from misclassification alone: exp z_lbl ≤ exp z_c and both terms sit inside the positive sum.

theorem Proofs.TrainedLinearDescent.sm_cot_l1 :

∑ j : Fin 10, |softmax 10 (dense Wd bd xd) j - oneHot 10 lblD j| ≤ 2

Σⱼ |softmaxⱼ − onehotⱼ| = 2(1 − softmax_lbl) ≤ 2.

theorem Proofs.TrainedLinearDescent.sm_cot_sq :

1 / 4 ≤ ∑ j : Fin 10, (softmax 10 (dense Wd bd xd) j - oneHot 10 lblD j) ^ 2

Σⱼ (softmaxⱼ − onehotⱼ)² ≥ 1/4 — the label term alone, via softmax_lbl ≤ 1/2.

theorem Proofs.TrainedLinearDescent.grad_key (i : Fin 49) (j : Fin 10) :

gradAt (fun (w : Vec (49 * 10)) => crossEntropy 10 (dense (Mat.unflatten w) bd xd) lblD) Wd.flatten (finProdFinEquiv (i, j)) = xd i * (softmax 10 (dense Wd bd xd) j - oneHot 10 lblD j)

theorem Proofs.TrainedLinearDescent.gradL1_le :

∑ idx : Fin (49 * 10), |gradAt (fun (w : Vec (49 * 10)) => crossEntropy 10 (dense (Mat.unflatten w) bd xd) lblD) Wd.flatten idx| ≤ 15367 / 1020

Σ|∇L| ≤ ((15367 : ℝ)/1020) (= 2·Σxᵢ, exact).

theorem Proofs.TrainedLinearDescent.gradSq_lower :

1511461 / 332928 / 4 ≤ ∑ idx : Fin (49 * 10), gradAt (fun (w : Vec (49 * 10)) => crossEntropy 10 (dense (Mat.unflatten w) bd xd) lblD) Wd.flatten idx ^ 2

Σ(∇L)² ≥ ((1511461 : ℝ)/332928)/4 (= (Σxᵢ²)/4, exact).

theorem Proofs.TrainedLinearDescent.hdelta (k : Fin 10) :

|binary32.dense Wd bd xd k - dense Wd bd xd k| ≤ 1 / 25000

Float-forward drift: denseErr at b = 0, e = 0, evaluated exactly per class column — ((1+2⁻²⁴)⁵¹ − 1)·Σᵢ|Wᵢₖ|·|xᵢ| ≤ ((1 : ℝ)/25000).

theorem Proofs.TrainedLinearDescent.hrho :

FloatModel.smRho binary32.u 0 10 < 1

theorem Proofs.TrainedLinearDescent.heta :

FloatModel.mulErr binary32.u 1 1 0 (FloatModel.cotErr binary32.u 0 (1 / 25000) 10) ≤ 81 / 1000000

The gradient-oracle budget η = mulErr u32 1 1 0 (cotErr u32 0 δ 10), bounded by ((81 : ℝ)/1000000) — the exp(2δ)−1 term via the γ-form.

theorem Proofs.TrainedLinearDescent.heta0 :

0 ≤ FloatModel.mulErr binary32.u 1 1 0 (FloatModel.cotErr binary32.u 0 (1 / 25000) 10)

theorem Proofs.TrainedLinearDescent.trained_linear_sgd_descends_concrete :

crossEntropy 10 (dense (Mat.unflatten (Wd.flatten - (1 / 8192) • binary32.linearFloatGrad Wd bd xd Real.exp lblD)) bd xd) lblD ≤ crossEntropy 10 (dense (Mat.unflatten Wd.flatten) bd xd) lblD - (1 / 8192 * ∑ idx : Fin (49 * 10), gradAt (fun (w : Vec (49 * 10)) => crossEntropy 10 (dense (Mat.unflatten w) bd xd) lblD) Wd.flatten idx ^ 2) / 2

Descent at TRAINED weights. One binary32 SGD step (lr = ((1 : ℝ)/8192)) on the trained linear classifier, at the misclassified witness, decreases the real cross-entropy by ≥ lr·‖∇L‖²/2 — every hypothesis of linear_float_sgd_descends discharged, the rounding model constructed (rndP 23), zero axioms. Retires the W = 0 degeneracy caveat of binary32_linear_sgd_descends_concrete.

theorem Proofs.TrainedLinearDescent.trained_linear_sgd_strictly_descends :

crossEntropy 10 (dense (Mat.unflatten (Wd.flatten - (1 / 8192) • binary32.linearFloatGrad Wd bd xd Real.exp lblD)) bd xd) lblD < crossEntropy 10 (dense (Mat.unflatten Wd.flatten) bd xd) lblD

The drop is strictly positive: the witness is misclassified, so Σ∇² ≥ ((1511461 : ℝ)/332928)/4 > 0 and the loss strictly decreases.