RootClauseBGateGeometry #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The window's volume, at the gate #
The window IS the translate at the gate, so its volume is exactly 3^{dj}.
RootClauseBCloseArith.volume_toReal_truncatedWindow_inner_gen with the
printed pair replaced by (GATE j).
2. The K_g slot of the chain, at the gate #
The window-to-cube step at the gate.
ν^{1/2}‖∇u‖_{L²((z+□_j) ∩ □_m)} ≤ 3^{(m-j)d/2} · ν^{1/2}‖∇u‖_{L²(□_m)} .
RootClauseBCloseArith.stepSevenNuGradNorm_window_le_cube at (GATE j). Not
an estimate on u: integral monotonicity on nested sets plus the exact volume
computation of §1.
6. The dataB field at the free coarse scale, at the gate #
dataB at the re-cut coarse cube, at the gate.
RootClauseBClosePayload.rootClauseB_dataB_free with the printed interiority
replaced by (GATE k_c); k_c ≤ m is kept as the pure scale comparison the
final 3^{k_c/2} ≤ 3^{m/2} step needs.
7. The dataM field, at the gate #
dataM at the gate.
RootPayloadDataM.rootClauseB_dataM with the printed interiority replaced by
(GATE n'). The remaining n' ≤ m - 1 is the pure scale comparison of the
σ-reconciliation (n' + 1 ≤ m ≤ m₀) and of the exponent budget; no
geometry rides on it.