Analytic side conditions for reachable R-322 states #
The production R-322 state machine replaces one edge at a time by a genuine two-variable collapse. This file records analytic properties of those reachable heterogeneous edge families. In particular, measurability is derived from the construction and is not carried as an extra hypothesis by the residual-integral induction.
The substantially stronger section-integrability statements needed by the current one-step Fubini API are kept separate below: they require absolute integrability of generalized primitive blocks, not merely measurability of their input kernels.
Measurability of a genuine collapse #
The R-322 collapse integrand is jointly measurable in its external argument and its two integration variables.
A collapse of measurable kernels is measurable, independently of whether a later quantitative argument has established its integrability. This is legitimate for mathlib's totalized Bochner integral.
Absolute integrability of a generalized primitive block #
At every order at least two, the R-51 lintegral estimate implies
genuine Bochner integrability of each individual primitive summand.
This extraction is deliberately separate from Proposition 4.1's pointwise kernel bound: it rules out the junk value of the totalized integral.
At primitive order one there are no internal variables. Consequently every assembled primitive summand is integrable over the zero-fold paper product, without any analytic hypothesis on the input edge.
Absolute integrability of each raw generalized primitive summand from the exact hypotheses carried by an edge certificate.
For orders at least two, each input edge is normalized off the identity, the R-51 estimate is applied to the resulting admissible family, and the heterogeneous scale product is restored. The two integrands agree almost everywhere because every primitive-chain edge avoids its diagonal almost surely. Order one is the zero-dimensional base case.
Joint integrability of heterogeneous Haar paths #
Reachable edge families #
Every edge in a production-reachable R-322 state is measurable.
The induction is over the actual absorption history. At the updated slot the new edge is a collapse whose middle kernel is the genuine primitive kernel built from the previous state's measurable edges; all other slots are definitionally unchanged.
The current primitive middle kernel at any proper step issued from a reachable state is measurable.
The generalized closed primitive integrand at a reachable proper step is jointly measurable in its complete block tuple.
Every closed primitive summand occurring at a production-reachable proper step has an absolutely integrable internal section.
This is the concrete discharge of the hinternal side condition in the
one-step R-322 Fubini identity. It uses only reachability for measurability
and the current edge certificate for the class-E and off-diagonal
majorant hypotheses.
Uniform-in-pairing, almost-everywhere endpoint form consumed by the production proper-step Fubini API. In fact the section theorem above is pointwise in both endpoints; the weaker a.e. packaging prevents downstream interfaces from demanding unnecessary diagonal statements.
The complete local integrand of a reachable proper step is measurable in its standard block coordinates.
The complete local integrand at a production-reachable proper step is jointly integrable in the external predecessor point and every block coordinate.
The proof uses only the actual edge certificate. Each reachable edge is
L¹ by its measurable off-diagonal inverse-square bound. The two terms
of the outgoing difference are then heterogeneous Haar paths, while the
finite primitive covariance sum is a bounded measurable multiplier at a
fixed positive mollification scale.
The exact a.e. section form required as hstandard by the production
proper-step Fubini API.