Documentation

LeanMlir.Proofs.Certificates.SmoothingNetWitness

The net-semantics tie, INSTANTIATED — CERTIFY for a concrete trained net #

GENERATED by scripts/smoothing_net_witness_gen.py. The smoothing chain's last informal hypotheses — hC measurability and hp interiority for the abstract classifier — are here DISCHARGED for mlpT, the trained /128-rationalized 49→8→10 pooled-MNIST MLP (LipschitzCertInstance.lean): measurability from the logits' continuity, interiority from ONE strict-argmax witness per class (argmaxNet_smoothProb_mem_Ioo). Each witness is a pooled test image whose predicted class leads every other logit STRICTLY — checked in exact integer arithmetic at generation and re-proved in-kernel below.

smoothing_cp_certified_mlpT is Cohen's CERTIFY guarantee for THIS network's argmax with every semantic hypothesis discharged; the demo instantiates it at the deployed scorecard scale (N = 10112, α = 1/1000). Honest scope: mlpT is the Lipschitz-thread pooled net, not the 784-dim smoothing-driver checkpoint (that tie = the same generator pass at full width), and the driver's float forward vs this real-semantics net is the FloatBridge tier's story.

noncomputable def Proofs.LipschitzCertDemo.netW0 :

EuclideanSpace ℝ (Fin 49)

Class-0 witness: pooled test image #440 (label 0); exact logit margin over the runner-up is 836677782/66846720 ≈ 12.5164.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre0 :

Fin 8 → ℝ

Exact hidden pre-activations of netW0 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre0 = ![2344404 / 522240, 308115 / 522240, 3650232 / 522240, 1571308 / 522240, 3083975 / 522240, -271024 / 522240, -270807 / 522240, 2145824 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW0_pre (k : Fin 8) :

(denseE W1t netW0).ofLp k = netWpre0 k

theorem Proofs.LipschitzCertDemo.netW0_strict (j : Fin 10) :

j ≠ 0 → (mlpT netW0).ofLp j < (mlpT netW0).ofLp 0

In-kernel STRICT argmax at the class-0 witness.

noncomputable def Proofs.LipschitzCertDemo.netW1 :

EuclideanSpace ℝ (Fin 49)

Class-1 witness: pooled test image #3231 (label 1); exact logit margin over the runner-up is 476292520/66846720 ≈ 7.1251.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre1 :

Fin 8 → ℝ

Exact hidden pre-activations of netW1 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre1 = ![405890 / 522240, 1700321 / 522240, -12390 / 522240, 1494728 / 522240, 10510 / 522240, -693193 / 522240, 272428 / 522240, 476958 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW1_pre (k : Fin 8) :

(denseE W1t netW1).ofLp k = netWpre1 k

theorem Proofs.LipschitzCertDemo.netW1_strict (j : Fin 10) :

j ≠ 1 → (mlpT netW1).ofLp j < (mlpT netW1).ofLp 1

In-kernel STRICT argmax at the class-1 witness.

noncomputable def Proofs.LipschitzCertDemo.netW2 :

EuclideanSpace ℝ (Fin 49)

Class-2 witness: pooled test image #1895 (label 2); exact logit margin over the runner-up is 929615405/66846720 ≈ 13.9067.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre2 :

Fin 8 → ℝ

Exact hidden pre-activations of netW2 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre2 = ![507504 / 522240, 730889 / 522240, 164933 / 522240, 245813 / 522240, 2734742 / 522240, -21615 / 522240, 1483431 / 522240, 2664061 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW2_pre (k : Fin 8) :

(denseE W1t netW2).ofLp k = netWpre2 k

theorem Proofs.LipschitzCertDemo.netW2_strict (j : Fin 10) :

j ≠ 2 → (mlpT netW2).ofLp j < (mlpT netW2).ofLp 2

In-kernel STRICT argmax at the class-2 witness.

noncomputable def Proofs.LipschitzCertDemo.netW3 :

EuclideanSpace ℝ (Fin 49)

Class-3 witness: pooled test image #1845 (label 3); exact logit margin over the runner-up is 638124398/66846720 ≈ 9.5461.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre3 :

Fin 8 → ℝ

Exact hidden pre-activations of netW3 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre3 = ![1671665 / 522240, 1877481 / 522240, 1610285 / 522240, 664777 / 522240, 300203 / 522240, 408152 / 522240, 1235760 / 522240, 1232358 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW3_pre (k : Fin 8) :

(denseE W1t netW3).ofLp k = netWpre3 k

theorem Proofs.LipschitzCertDemo.netW3_strict (j : Fin 10) :

j ≠ 3 → (mlpT netW3).ofLp j < (mlpT netW3).ofLp 3

In-kernel STRICT argmax at the class-3 witness.

noncomputable def Proofs.LipschitzCertDemo.netW4 :

EuclideanSpace ℝ (Fin 49)

Class-4 witness: pooled test image #8000 (label 4); exact logit margin over the runner-up is 691947893/66846720 ≈ 10.3513.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre4 :

Fin 8 → ℝ

Exact hidden pre-activations of netW4 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre4 = ![2555993 / 522240, -1290672 / 522240, -1307681 / 522240, -241933 / 522240, 2307751 / 522240, 1289408 / 522240, 1797085 / 522240, 1672581 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW4_pre (k : Fin 8) :

(denseE W1t netW4).ofLp k = netWpre4 k

theorem Proofs.LipschitzCertDemo.netW4_strict (j : Fin 10) :

j ≠ 4 → (mlpT netW4).ofLp j < (mlpT netW4).ofLp 4

In-kernel STRICT argmax at the class-4 witness.

noncomputable def Proofs.LipschitzCertDemo.netW5 :

EuclideanSpace ℝ (Fin 49)

Class-5 witness: pooled test image #6908 (label 5); exact logit margin over the runner-up is 644875950/66846720 ≈ 9.6471.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre5 :

Fin 8 → ℝ

Exact hidden pre-activations of netW5 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre5 = ![1755282 / 522240, 45753 / 522240, 2104805 / 522240, 2544886 / 522240, 46180 / 522240, -868603 / 522240, 680653 / 522240, 1359915 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW5_pre (k : Fin 8) :

(denseE W1t netW5).ofLp k = netWpre5 k

theorem Proofs.LipschitzCertDemo.netW5_strict (j : Fin 10) :

j ≠ 5 → (mlpT netW5).ofLp j < (mlpT netW5).ofLp 5

In-kernel STRICT argmax at the class-5 witness.

noncomputable def Proofs.LipschitzCertDemo.netW6 :

EuclideanSpace ℝ (Fin 49)

Class-6 witness: pooled test image #7843 (label 6); exact logit margin over the runner-up is 867723980/66846720 ≈ 12.9808.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre6 :

Fin 8 → ℝ

Exact hidden pre-activations of netW6 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre6 = ![2082231 / 522240, 528761 / 522240, 558786 / 522240, 2451382 / 522240, 3703499 / 522240, -1735868 / 522240, 1048876 / 522240, 1180197 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW6_pre (k : Fin 8) :

(denseE W1t netW6).ofLp k = netWpre6 k

theorem Proofs.LipschitzCertDemo.netW6_strict (j : Fin 10) :

j ≠ 6 → (mlpT netW6).ofLp j < (mlpT netW6).ofLp 6

In-kernel STRICT argmax at the class-6 witness.

noncomputable def Proofs.LipschitzCertDemo.netW7 :

EuclideanSpace ℝ (Fin 49)

Class-7 witness: pooled test image #5297 (label 7); exact logit margin over the runner-up is 748210150/66846720 ≈ 11.1929.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre7 :

Fin 8 → ℝ

Exact hidden pre-activations of netW7 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre7 = ![2722470 / 522240, 1821025 / 522240, 2470904 / 522240, 23165 / 522240, 1777794 / 522240, 733076 / 522240, -458199 / 522240, 752459 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW7_pre (k : Fin 8) :

(denseE W1t netW7).ofLp k = netWpre7 k

theorem Proofs.LipschitzCertDemo.netW7_strict (j : Fin 10) :

j ≠ 7 → (mlpT netW7).ofLp j < (mlpT netW7).ofLp 7

In-kernel STRICT argmax at the class-7 witness.

noncomputable def Proofs.LipschitzCertDemo.netW8 :

EuclideanSpace ℝ (Fin 49)

Class-8 witness: pooled test image #7919 (label 8); exact logit margin over the runner-up is 593814126/66846720 ≈ 8.8832.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre8 :

Fin 8 → ℝ

Exact hidden pre-activations of netW8 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre8 = ![3131303 / 522240, 1547971 / 522240, 1418373 / 522240, 2051426 / 522240, 2739909 / 522240, 895902 / 522240, 206892 / 522240, 3634063 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW8_pre (k : Fin 8) :

(denseE W1t netW8).ofLp k = netWpre8 k

theorem Proofs.LipschitzCertDemo.netW8_strict (j : Fin 10) :

j ≠ 8 → (mlpT netW8).ofLp j < (mlpT netW8).ofLp 8

In-kernel STRICT argmax at the class-8 witness.

noncomputable def Proofs.LipschitzCertDemo.netW9 :

EuclideanSpace ℝ (Fin 49)

Class-9 witness: pooled test image #2478 (label 9); exact logit margin over the runner-up is 509675629/66846720 ≈ 7.6245.

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.netWpre9 :

Fin 8 → ℝ

Exact hidden pre-activations of netW9 (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.netWpre9 = ![3456857 / 522240, 1098256 / 522240, 1070775 / 522240, 1088239 / 522240, 760810 / 522240, -72542 / 522240, 835586 / 522240, 836129 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.netW9_pre (k : Fin 8) :

(denseE W1t netW9).ofLp k = netWpre9 k

theorem Proofs.LipschitzCertDemo.netW9_strict (j : Fin 10) :

j ≠ 9 → (mlpT netW9).ofLp j < (mlpT netW9).ofLp 9

In-kernel STRICT argmax at the class-9 witness.

noncomputable def Proofs.LipschitzCertDemo.netW :

Fin 10 → EuclideanSpace ℝ (Fin 49)

The witness bundle: one strict-argmax point per class.

Equations

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

Instances For

theorem Proofs.LipschitzCertDemo.netW_strict (c j : Fin 10) :

j ≠ c → (mlpT (netW c)).ofLp j < (mlpT (netW c)).ofLp c

theorem Proofs.LipschitzCertDemo.smoothing_cp_certified_mlpT {σ : ℝ} (hσ : 0 < σ) (x : EuclideanSpace ℝ (Fin 49)) (y : Fin 10) {N k₀ : ℕ} (hk₀ : k₀ ≤ N) {α q₀ : ℝ} (hα : 0 ≤ α) (hα1 : α < 1) (hq₀ : q₀ ∈ Set.Ioo 0 1) (htail : binomTail N k₀ q₀ ≤ α) :

1 - α ≤ (MeasureTheory.Measure.pi fun (x : Fin N) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 49))).real {ω : Fin N → EuclideanSpace ℝ (Fin 49) | (∑ i : Fin N, if argmaxNet (fun (v : EuclideanSpace ℝ (Fin 49)) (j : Fin (9 + 1)) => (mlpT v).ofLp j) (x + σ • ω i) = y then 1 else 0) = k₀ → ∀ (δ : EuclideanSpace ℝ (Fin 49)), ‖δ‖ < σ * stdNormalQuantile q₀ → ∀ (j : Fin 10), j ≠ y → ∫ (z : EuclideanSpace ℝ (Fin 49)), if argmaxNet (fun (v : EuclideanSpace ℝ (Fin 49)) (j : Fin (9 + 1)) => (mlpT v).ofLp j) (x + δ + σ • z) = j then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 49)) < ∫ (z : EuclideanSpace ℝ (Fin 49)), if argmaxNet (fun (v : EuclideanSpace ℝ (Fin 49)) (j : Fin (9 + 1)) => (mlpT v).ofLp j) (x + δ + σ • z) = y then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 49))}

CERTIFY for the CONCRETE net. smoothing_cp_certified_net with the classifier = mlpT's argmax: measurability and hp interiority both DISCHARGED (continuity + the ten witnesses above). With probability ≥ 1 − α over the N Gaussian samples: if the vote count for y at x comes out k₀, every ‖δ‖ < σ·Φ⁻¹(q₀) leaves y the strict argmax of the smoothed mlpT.

theorem Proofs.LipschitzCertDemo.smooth_cp_mlpT_demo {σ : ℝ} (hσ : 0 < σ) (x : EuclideanSpace ℝ (Fin 49)) (y : Fin 10) :

1 - 1 / 1000 ≤ (MeasureTheory.Measure.pi fun (x : Fin 10112) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 49))).real {ω : Fin 10112 → EuclideanSpace ℝ (Fin 49) | (∑ i : Fin 10112, if argmaxNet (fun (v : EuclideanSpace ℝ (Fin 49)) (j : Fin (9 + 1)) => (mlpT v).ofLp j) (x + σ • ω i) = y then 1 else 0) = 10084 → ∀ (δ : EuclideanSpace ℝ (Fin 49)), ‖δ‖ < σ * stdNormalQuantile (9952 / 10000) → ∀ (j : Fin 10), j ≠ y → ∫ (z : EuclideanSpace ℝ (Fin 49)), if argmaxNet (fun (v : EuclideanSpace ℝ (Fin 49)) (j : Fin (9 + 1)) => (mlpT v).ofLp j) (x + δ + σ • z) = j then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 49)) < ∫ (z : EuclideanSpace ℝ (Fin 49)), if argmaxNet (fun (v : EuclideanSpace ℝ (Fin 49)) (j : Fin (9 + 1)) => (mlpT v).ofLp j) (x + δ + σ • z) = y then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 49))}

The deployed-protocol demo: at the scorecard's N = 10112, α = 1/1000, a count of 10084 certifies radius σ·Φ⁻¹(0.9952) for the smoothed mlpT — the per-image scorecard shape with NO abstract-classifier hypotheses left (the tail check is one kernel evaluation). The count is SmoothingCPScorecard.lean's MNIST-MLP image-1 entry, from a 784-dim driver run; no Monte-Carlo count has been taken on mlpT itself, so the hypothesis is the protocol's, not a measurement of this net.