Conv and max-pool index facts — the flat ↔ tensor index vocabulary #
The flat-index plumbing every conv-net proof reads tensors through (t3Idx and its
flat-sum sum_t3), and the 2×2 max-pool's window facts: the pool with its routing frozen
(poolGatherFlat, which agrees with the pool at its selection) is ℓ1-contractive
(poolGatherFlat_l1_contract), and a selection margin beyond 2δ freezes the argmax
(MaxPool2MarginQ). The conv reads its input through the zero-padded window convPad
and its kernel through the flat index k4Idx; cells with identical padded patches are twins
(ConvPatchEq, and ConvPatchEq2 two convs deep), equal under every kernel and bias
(conv2d_eq_of_convPatchEq). The conv as a dense layer with weight sharing and its float forward
are in ConvFloat.
Flat index of a Tensor3 coordinate (the suite's row-major layout).
Note: on Lean ≥ 4.33 the proofs below fail without @[reducible]:
t3Idx_def folds the raw encoding into the ite CONDITION below, but simp does not rewrite
inside the Decidable INSTANCE argument, so the goal carries a folded condition over an
unfolded instance and every ite_eq_left/ite_eq_right here fails to match. basisVec, which produces
that ite, is @[reducible] for the same reason.
Equations
- Proofs.t3Idx ci hi wi = finProdFinEquiv (finProdFinEquiv (ci, hi), wi)
Instances For
Column version of winRowEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The 2×2 gather as a continuous linear map: each output reads one input coordinate.
Equations
- Proofs.poolGatherCLM σ = { toFun := Proofs.poolGatherFlat σ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
The gather's Jacobian: input (ci, hi, wi) feeds pooled (co, ho, wo) exactly when it is
that window's selected cell.
The flat pool is the flat gather at a dominating selection.
Quantitative pool-selection margin: in every 2×2 window, a cell that dominates the
window is more than 2δ above every other cell of it. The quantitative form of
MaxPool2Smooth — a perturbation of at most δ per entry can neither tie the max nor move
it to another cell, so the pool's argmax routing freezes. The other cells may tie with each
other. The pool peer of the ReLU margin a·D < |zⱼ|.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every point within δ of a margined point is smooth (every window's max is attained once).
A margined point is itself smooth.
The argmax freezes: within δ of a margined point, every window's
argmax cell is the same as at the margined point.
Quantitative pool margin up to twins (2×2), on the PRE-activation: WindowMarginUpTo
at the 2×2 windows. Every window is dead (all cells ≤ 0), or a cell dominating it is more
than 2δ above every other cell except its T-twins. Unlike MaxPool2MarginQ, a window of
equal cells qualifies when its cells are twins: the descent rungs take T to relate cells
that read identical input patches, which are equal for every value of the moving parameter.
That is the case real MNIST forces (a constant background patch makes a window's cells
equal for every kernel); see scripts/probes/mnist_pool_twin_probe.py.
Equations
Instances For
The post-ReLU MaxPool2MarginQ gives the pre-activation MaxPool2MarginQUpTo, with any
twins: the dominating pre-activation cell is positive unless the window is dead, and below a
positive cell the pre-activation gaps are at least the post-ReLU ones.
MaxPool2MarginQ.to_marginQUpTo in the flat spelling the descent rungs use, the post-ReLU
tensor as unflatten ∘ relu ∘ flatten.
The padded input read that multiplies kernel entry (·, c, kh, kw) at
output position (hi, wi) — names the dite inside conv2d so the
affine-in-the-kernel structure can be stated. Depends on the input
only, never the kernel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Flat index of a Kernel4 entry (the suite's row-major layout).
Equations
- Proofs.k4Idx o c kh kw = finProdFinEquiv (finProdFinEquiv (finProdFinEquiv (o, c), kh), kw)
Instances For
Kernel4.flatten reads off at a k4Idx — the forward peer of
unflatten_k4Idx, lifting a per-entry kernel bound to the flattened vector.
Folds the raw finProdFinEquiv encoding back into t3Idx.
Twin cells of a conv input: positions p and q whose zero-padded kH×kW input
patches are identical in every input channel. The conv output is then the same at p and
q for EVERY kernel and bias (conv2d_eq_of_convPatchEq), so a tie between them is a tie
along any step on the conv's parameters. A flat image region gives such pairs.
Equations
- Proofs.ConvPatchEq kH kW x p q = ∀ (cc : Fin ic) (kh : Fin kH) (kw : Fin kW), Proofs.convPad kH kW x cc kh kw p.1 p.2 = Proofs.convPad kH kW x cc kh kw q.1 q.2
Instances For
Two cells whose patches are entirely zero are twins: the form a blank image region gives, and the one a concrete instance discharges cell by cell.
Twin cells have equal conv outputs, for every kernel and bias.
Two-layer twins: positions p and q whose two-conv receptive fields are identical.
For every offset of the outer kH×kW window, both reads fall in the zero padding, or both
land on cells whose inner patches of x are identical (ConvPatchEq). Then the outer conv's
input patches at p and q agree for every inner kernel and bias
(convPatchEq_relu_conv), so a tie between the outer outputs there is a tie along any step
on the inner conv's parameters. A flat image region away from the border gives such pairs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two-layer twins are twins of the outer conv's input, for every inner kernel and bias.
Float pool-backward closeness. Under the pool
margin the float post-relu argmax matches the real one
(isArgmax_iff), so the pool's backward selector
𝟙[(ci,hi,wi) is its window's argmax]·(pooled cotangent) differs from the
certified one only through the pooled cotangent value — an indicator
pass-through (indicator ∈ {0,1}), the pool peer of reluMask_close.
The two cotangent values ay (float) / ax (real) enter only via their
closeness |ay − ax| ≤ e.