RebaseGeneralClauseRegated #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The interior chain's re-gated instance #
Conditional-free provider helper, not a node realization. The re-gated
sibling of RebaseGeneralClause's
exists_generalClauseReal_frontierEmpty_legMoved, at the frozen text: the
hoisted funding line and the good-event threshold of the general clause both
read C⁻¹ s⁴ instead of (1/2), at the statement's own existential constant.
Both edits are hypothesis-side here — the funding line is a hypothesis, and
so is the event membership hmem in the real-valued clause — so the re-gated
instance is a pure a-fortiori composition of the (1/2) one at the constant
re-choice C ↦ max C 2:
regime_le_of_const_leback-ports the standing regime;funding_le_of_epsilon_leback-ports the funding line (C⁻¹ s⁴ ≤ 1/2funds less);- the proved
GoodEvents.goodEventAt_mono_epback-ports the event membership (the re-gated event is the smaller set, sohmematC⁻¹ s⁴giveshmemat(1/2)); fourSummandBracket_nonnegpays the constant bump on the conclusion.
Nothing else moves. The flux index n+3, the binder n+3 ≤ m, the
frontier-empty gate at n+2, the windows W = (z+□_{n+2}) ∩ □_m and
W' = (z+□_{n+3}) ∩ □_m, the flux prefactor s^{-4}, the in-bracket companion
s^{-3/2}, the force leg s^{-7} and the two ∇h legs s^{-6} are the frozen
block's own: only the two literals (1/2) ↦ C⁻¹ s⁴ move.
References #
- ABK26,
l.harmonic.approximation.good.scales; the frozen block as realized inProviderEpsFree(read for comparison, never imported).
The Join's hgen, at frontier-empty windows, re-gated.
exists_generalClauseReal_frontierEmpty_legMoved read a fortiori at the
C⁻¹ s⁴ funding line and the C⁻¹ s⁴ good-event threshold. Same carriers,
same legs; only the two literals move, and both move the safe way.