Paper-faithful incoming input for R-324 Step 1 #
In (4.17) the kernel on the incoming leg is the input denoted G₀ in the
paper. Proper intervals lying to the left of the retained terminal block
may already have been collapsed into this leg, so it is not in general the
free Green kernel. The only property used for the frequency-independent
Step-1 estimate is the output of (4.13): measurability and the bound
|G₀(z)| ≤ A |z|⁻².
This file is the minimal generalization of R324PaperStep1.lean needed at
that seam. The terminal primitive kernel and all of the y/cosine/inserted
kernel argument are unchanged. The incoming x integral is paid in L¹,
as in the paper, rather than being incorrectly identified with the Fourier
multiplier of greenFn.
The corrected form of (4.17) #
The untranslated Fourier coefficient of the incoming removal output.
Equations
- Anderson4D.r324IncomingMode G0 α = ∫ (u : Anderson4D.T4), Anderson4D.charT4 α u * ↑(G0 u) ∂Anderson4D.paperMeasure
Instances For
The unchanged endpoint and symmetry calculation #
The y integral is exactly the one in the original Step-1 proof.
The x integral records the arbitrary incoming Fourier coefficient.
The terminal primitive kernel still supplies the identical
E-symmetry cancellation.
Paying the incoming removal output in L¹ #
The generalized Step-1 integral differs from the old one only by the
incoming L¹ factor.
The corrected normalized reduction interface #
Minimal paper-faithful replacement for R324Step1Reduction: the
incoming output of the proper-prefix removal is explicit and carries its
own scale.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The genuine terminal trace: the inserted-majorant estimate #
Removing the genuinely empty post-terminal carrier #
The carrier after the retained terminal head is empty, hence the apparently retained post-head Haar integral has mass one. This is the normalization fact deliberately left literal by the earlier Fubini bridge.
At the singleton stop the complete active-scale carrier is exactly the incoming predecessor, the terminal internal chain, and the one outgoing Green slot. This is the local product decomposition needed to compare the actual Step-1 charge with the global budget invariant.
Absolute integrability of the corrected four-point Step-1 kernel #
The corrected four-point integrand is absolutely integrable whenever
the incoming removal output and the retained primitive kernel are in L¹.
This is the Fubini license used below; no estimate is taken here.
The nested order used in the paper's display (4.17) is the grouped
(z,w)-then-(x,y) product integral.
Actual terminal inputs are in L¹ #
The terminal raw-local block, after the honest standard-block change of coordinates, is exactly the four physical kernels of (4.17). In particular the incoming factor is the actual predecessor edge of the reached trace.
Exact paper-(4.17) representation of the complete terminal Fourier
integral. This is the missing normalization seam: the incoming kernel is
the reached predecessor edge, not an unjustified fresh copy of greenFn.
All changes of integration order are licensed by the stopped-residual and
four-point L¹ theorems.
Proposition 4.1 applied to the normalized actual terminal edges makes the heterogeneous retained primitive kernel genuinely integrable.
The terminal primitive phase with all genuine internal edge scales,
paid by the inserted majorant of (4.4). This is the frequency-independent
analogue of norm_integral_terminalPrimitiveKernelDiff_mul_..._le_scaled;
the latter deliberately uses the Step-4 bound |cos-1| ≤ 2, whereas
Step 1 keeps the quadratic cosine gain.
The proof takes the modulus only after the signed primitive-pairing sum has
been integrated and the E-symmetry cancellation has been applied.
Fixed-endpoint Step 1 for the actual terminal trace. The predecessor
is the paper's G₀; its certificate scale is charged exactly once. The
terminal internal edge scales are charged by the preceding theorem, while
the outgoing Green difference is Fourier-integrated without a norm.
Uniform Step-1 estimate for the complete terminal Fourier half, with the two scale charges exposed exactly as they occur in the trace ledger. This is (4.17) followed by the paper's quadratic cosine cancellation and inserted-kernel majorant; no absolute value is taken before the signed terminal primitive sum has been integrated.
Closing the literal trace scale ledger #
The predecessor and all genuine internal terminal scales are no larger
than the complete active budget product. The missing outgoing factor is
exactly the initial Green scale A ≥ 1.
Public scalar ledger for reusing the complete full-half budget with a
different terminal Fourier calculation. The Step 4(A) endpoint proof has
the same stop-scale and suffix multiplier as Step 1; only its terminal
factor D changes.
Uniform complete-half producer #
Paper Step 1, complete full-pairing half.
For the canonical Proposition-4.1 trace, the complete endpoint-signature
half has the paper's uniform (C λ)^(2q) / |log ε| bound. This theorem
contains the finite-fibre producer, every proper-prefix collapse, the
corrected incoming G₀ form of (4.17), the terminal signed cancellation,
and the final scale/order absorption.
Direct closure of the full/full refined fibre #
Paper Step 1, full/full refined fibre.
The exact finite-fibre product factorization is combined with the two
unconditional normalized half estimates above. Fullness supplies the
even-order witness m = 2q; the paper range 1 ≤ m excludes the empty
q = 0 trace. The product has two logarithmic gains, one of which is
discarded using 1 ≤ |log ε|, and the remaining gain is exactly the
integrated inserted-majorant lower bound.
The statement includes the degenerate coupling lam = 0, so downstream
full/full routing needs no separate analytic interface.
Paper Step 1, full/full refined fibre at an arbitrary positive support constant.
The loss supportConstant² / min supportConstant 1⁴ in the quantitative
inserted-majorant lower bound is independent of the order. Enlarging the
primitive constant by that loss absorbs it uniformly because m ≥ 1.
No new reduction interface is introduced.