bitDelta
plain-language theorem explainer
Signed single-bit change between two Boolean record entries: +1 for 0→1, −1 for 1→0, 0 if unchanged. Gravity/holography proofs cite it when turning exterior cut records into integer channel weights and heat. The body is the plain difference of 0–1 indicators.
Claim. For booleans $b,b'$, define the integer bit delta $\Delta(b,b')=[b']-[b]$, where $[\mathrm{true}]=1$ and $[\mathrm{false}]=0$. Thus $\Delta\in\{-1,0,1\}$.
background
The module builds one probe-independent symmetric stress-like matrix from signed exterior cut-channel events and an explicit model covector assignment. Honesty tags stress that the covector is a model interface, weights come from posted cut records, and the construction does not claim continuum stress-energy, Unruh, Ricci, focusing, EFE, or C-gap1 closure.
Boolean lists encode exterior cut records. Flux between two successive records is the sum of per-bit signed changes. This definition supplies that per-bit integer: the difference of the two bits as 0–1 values. Downstream, channel deltas and exterior step heat are assembled from these integers so heat accounting matches the committed cut heat.
proof idea
Pure definition: return the integer difference of the two Boolean indicators, (if b' then 1 else 0) - (if b then 1 else 0). No lemmas or tactics.
why it matters
Local arithmetic atom for the heat ↔ channel-delta bridge. recordFlux_eq_sum_bitDelta is definitional equality of record flux with the sum of zipWith bitDelta. That lemma is rewritten in exteriorStepHeat_eq_sum_channelDeltaZ, which states that posted exterior heat equals the sum of signed exterior channel deltas and "links the new channel weights to the committed cut heat." zipWith_bitDelta_ofFn moves the same delta under List.ofFn so Fin-indexed channel readouts stay aligned.
In the gravity/holography stack this keeps stress weights derived from posted cut records rather than a tautological ∀k ∃T(k) interface, matching the module’s anti-tautology stance. It does not itself touch T0–T8, RCL, or the alpha band; it only feeds the discrete heat bookkeeping those bridges use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.