CertLayer — composing certified backward graphs, so a NET is one object #
Every conv net's *BackB0 file stops at a block capstone: r34DownBlockBackBatchedGraph_- faithful, mnv2ResidBlockBackBatchedGraph_faithful, mbResidBlockBackBatchedGraph_faithful,
cnxDownChBackGraph_faithful, and (2026-08-10) R50's three. So "the whole-net composed backward"
as §8 of planning/archive/mnv4_verified.md uses the phrase means block capstones — which is real, and
is not a net.
⛔ CORRECTION (2026-08-10). An earlier version of this paragraph said "Measured before
writing this file: nothing in LeanMlir/Proofs/ folds those blocks into a stage or a net."
That was wrong, and ViT is the counterexample. ViTBackB0.lean carried a depth-k reverse
fold of the block backward graph (by induction on k) and a direct proof of
vitNetBackGraph_faithful (patchEmbed → tower → final vec-LN → classifier, at every depth) the
whole time, both pinned in tests/AuditAxioms.lean. The measurement that produced that
sentence swept the conv nets and generalised — the same inference-by-analogy the MNv4 planning doc
records being wrong three times.
What ViT genuinely lacked was not a fold but a reusable one: its tower was a bespoke induction
that no other net could use and that reused nothing. ViTBackNet.lean closes that, and proves the
generic chain reproduces the bespoke tower term for term rather than replacing it.
⭐ The obstacle was never the mathematics; it was that the chaining was open-coded. Look at any
<body>BackBatchedGraph_faithful: it builds G₁ x (G₂ (f₁ x) e), rewrites with the two component
faithfulness lemmas, and closes by rfl on vjp_comp_at's definitional
backward dy = f₁.backward (f₂.backward dy). That argument is identical every time and is
re-typed per composition, so a 16-block net would be 16 copies of it with ever-larger terms.
This file does it once. CertLayer.comp is that proof; everything else is bookkeeping.
The structure #
A CertLayer m n is a forward map plus, at every input satisfying its own smoothness
precondition, a VJP, differentiability, a backward StableHLO graph, and the theorem that the
graph denotes the VJP. Carrying ok inside the layer is what makes composition work: relu nets
are _at, so a block is only certified where its pre-activations miss the kinks, and the composite
of two layers is certified exactly where the first is certified and the second is certified at
the first's output. That is ok x := L₁.ok x ∧ L₂.ok (L₁.fwd x), and it threads the deepening
hypothesis stack automatically instead of by hand.
⚠ This is not a new trust assumption. CertLayer.comp proves faithfulness of the composite
from the components' faithfulness; it introduces no axiom and no sorry. A chain built from
certified blocks is certified, and the fold is where that stops being a sentence and becomes a
theorem.
Reading the list order #
chain [L₁, L₂, L₃] runs L₁ first: fwd = L₃.fwd ∘ L₂.fwd ∘ L₁.fwd. List order is forward
execution order, which is how a block table reads. The backward graph nests the other way
automatically — L₁.graph x (L₂.graph _ (L₃.graph _ e)) — because that is what the chain rule
says, and getting it backwards is a silent wrong-gradient rather than a type error whenever the
widths happen to agree (the §3 trap, one level up).
A layer whose backward StableHLO graph is proven to denote its VJP, wherever its own
smoothness precondition ok holds.
ok is a predicate on the INPUT because that is what relu smoothness is: a condition on the
activations this particular layer sees. A globally-smooth layer (swish, a bare conv-bn) sets
ok := fun _ => True and loses nothing.
The forward map.
Where this layer is certified — the smoothness hypotheses, as a predicate on the input.
- diff (x : Vec m) : self.ok x → DifferentiableAt ℝ self.fwd x
Differentiability at any certified point (needed to compose via
vjp_comp_at). The proven VJP at any certified point.
The backward graph, as a function of the forward activation and the incoming cotangent.
- faithful (x : Vec m) (hx : self.ok x) (e : SHlo n) : den (self.graph x e) = (self.vjp x hx).backward (den e)
⭐ The theorem that makes it a certified layer: the graph denotes the VJP.
Instances For
The identity layer — certified everywhere, and its backward graph is the cotangent verbatim.
The unit of chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
⭐⭐ THE COMPOSITION THEOREM — the whole point of this file.
Two certified layers compose into a certified layer. The backward graph nests (L₁'s graph
fed L₂'s graph at L₁'s output), the smoothness preconditions conjoin, and faithfulness
follows from the components' faithfulness plus vjp_comp_at's definitional backward.
This is the argument every <body>BackBatchedGraph_faithful in the repo writes out by hand.
Proven once here, a chain of any length costs nothing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
⭐ Wrap a layer in an identity skip — x ↦ L.fwd x + x. The backward graph is the additive
fan-in addV (L.graph …) ecot: the body's input-cotangent plus the skip's verbatim cotangent.
Certified exactly where the body is (ok := L.ok), because an identity skip is smooth
everywhere and contributes no new condition. Every residual net in the repo hand-writes this
fan-in per block; here it is a combinator, so a residual block is residual (chain [...]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
⭐ A projected residual — x ↦ P.fwd x + F.fwd x, both paths nontrivial. The backward
graph is the fan-in addV (P.graph …) (F.graph …), certified where both paths are. The
downsample-block peer of residual: a projection skip changes the width, so the layer is
m → n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
⭐ The post-residual relu of a ResNet block, as a layer: certified where its input misses the
kink, with the %outR mask as its backward. (residual F).comp (reluOut _) is a whole identity
block, so its capstone is .faithful of that composite.
Equations
- One or more equations did not get rendered due to their size.
Instances For
⭐ The net-level statement, in one line. Whatever the chain's length, its backward graph
denotes its VJP — so a stage, a trunk, or a whole net assembled from certified blocks is
certified, with no per-length proof. This is just CertLayer.faithful at chain Ls; it is
restated here because it is the theorem the fold exists to provide.
⚠⚠ Projecting .fwd out of a composed CertLayer — the four lemmas below, and why they exist.
simp only [CertLayer.comp] rewrites L₁.comp L₂ to the full structure literal — fwd, ok,
diff, vjp, graph AND faithful — and only then projects .fwd out of it; over a 24-stage
chain that builds an enormous intermediate term whose bulk is PROOFS the goal never mentions
(MobileNetV4's T2 took three minutes without these, seconds with them). And at LITERAL widths the
peel itself is a kernel deterministic timeout by rfl / Function.comp_apply / Function.comp_assoc
— proved once here between variables, comp_fwd_apply is applied there in 2 s.