zipWith_bitDelta_ofFn
plain-language theorem explainer
Zipping the signed bit-change over two length-n boolean lists equals the list of componentwise bit-changes. Anyone equating exterior cut heat to a sum of channel deltas needs this commutation. The proof is list extensionality: matching lengths, then matching entries via the ofFn/zipWith get lemmas.
Claim. For $n\in\mathbb{N}$ and $f,g:\{0,\ldots,n-1\}\to\{\mathrm{true},\mathrm{false}\}$, if $\delta(b,b')=[b']-[b]\in\mathbb{Z}$ denotes the signed bit change, then $\mathrm{zipWith}(\delta,\mathrm{ofFn}(f),\mathrm{ofFn}(g))=\mathrm{ofFn}(i\mapsto\delta(f(i),g(i)))$.
background
The module builds one probe-independent symmetric stress-like matrix from signed exterior cut-channel events and an explicit model covector. Honesty tags stress that the construction does not claim continuum stress-energy, Unruh, Ricci, focusing, EFE, or C-gap1 closure: the matrix is defined once from weights and the covector, then contracted.
The helper $\delta(b,b')=[b']-[b]\in\mathbb{Z}$ records a single boolean flip as $+1$, $-1$, or $0$. Exterior cut records are finite boolean vectors; converting a pair of such records into a list of signed channel increments is exactly zipWith of $\delta$ on the two ofFn-lists. That algebraic identity is what this lemma isolates.
proof idea
Tactic proof by List.ext_getElem. First goal: lengths agree, discharged by simp on length_zipWith and length_ofFn. Second goal: for each valid index $i$, the $i$-th entries agree. The length hypothesis is rewritten to $i<n$ via length_ofFn, then simp on getElem_zipWith and getElem_ofFn finishes. No arithmetic on $\delta$ itself is needed; only the list constructors commute.
why it matters
Downstream, exteriorStepHeat_eq_sum_channelDeltaZ rewrites posted exterior heat as the sum of signed exterior channel deltas, linking new channel weights to the committed cut heat. That theorem unfolds exterior heat, applies a record-flux sum-of-bitDelta identity, and rewrites both exterior records as channel lists; the present lemma is the ofFn/zipWith bridge that makes the channel-wise sum well-defined and equal to the list-level flux.
In the gravity stack this is bookkeeping, not a physical law: it keeps the discrete cut-channel accounting honest so the later event-stress matrix and its quadratic contractions sit on a single, probe-independent weight vector. It does not touch the forcing chain (T5–T8) or the RCL; it only stabilizes the record-flux side of the Clausius–Einstein bridge scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.