TT-_continuousWithinAt_zero — the two-time gap is continuous at the left endpoint t = 0 (within Ioi 0).

The log N(s(t),r(t)) term is continuous via the matched-path continuity (IsMatchedTimePath.cont) + heat-flow endpoint continuity (heatFlowEntropyPower_continuousWithinAt_zero); the −t term is continuous. Mirrors csiszarLogRatioGap_continuousWithinAt_zero (EPI/Stam/ToBridge.lean).

Mechanism. On Set.Ioi 0 (where the matched velocities give s t, r t > 0), matchedSum_law_eq rewrites the two-time sum heat flow into the single-noise heat flow of X + Y at τ = s t + r t: sumHeatFlowEP X Y Z_X Z_Y P (s t)(r t) = heatFlowEP (X+Y) Z P (s t + r t). This eventual equality (on a neighborhood of 0 within Ioi 0) lets us transfer the continuity via ContinuousWithinAt.congr. The reduced single-noise heat flow is the composition of the endpoint continuity atom heatFlowEntropyPower_continuousWithinAt_zero with the continuous matched reparameterization τ(t) = s t + r t (IsMatchedTimePath.cont).

Added preconditions are regularity:

• IsHeatFlowEndpointRegular (X+Y) Z P — the single-noise endpoint atom's input.
• the matchedSum_law_eq preconditions (unit-noise laws of Z_X, Z_Y, Z, the joint/pairwise independences, measurability) — noise-distribution facts, not bundled EPI/derivative content.
• h_pos : ∀ t, 0 < t → 0 < s t ∧ 0 < r t — the matched-path positivity on the interior (the strict-mono inverse-function path satisfies it), threaded as a precondition exactly as _hasDerivAt threads hst/hrt. @audit:ok

TT-_antitoneOn_Ici_zero — the two-time gap is AntitoneOn (Set.Ici 0).

antitoneOn_of_deriv_nonpos (convex Set.Ici 0) with continuity (twoTimeLogRatioGap_continuousWithinAt_zero), differentiability + per-t deriv ≤ 0 (twoTimeLogRatioGap_hasDerivAt.deriv + _deriv_le_zero). Mirrors csiszarLogRatioGap_antitoneOn_Ici_zero (EPI/Stam/ToBridge.lean).

Surface structure (matched to the single-time model). On the interior Set.Ioi 0 AntitoneOn holds: continuity there is the interior differentiability (_hasDerivAt.differentiableAt.differentiableWithinAt), interior (Ioi 0) = Ioi 0, and per-t deriv ≤ 0 is (_hasDerivAt ...).deriv rewritten to the closed-form derivative J_S·(1/J_X + 1/J_Y) − 1, bounded ≤ 0 by _deriv_le_zero instantiated with the free J_S := J_S_embed(t) (= the directly-embedded sum Fisher info) and the per-t harmonic Stam supply. The endpoint 0 is then re-attached via AntitoneOn.insert_of_continuousWithinAt + the endpoint continuity (Task 1).

The added preconditions are all regularity / Stam-supply, not a bundling of the EPI conclusion (the h_per_t conjunction supplies positivity, the density-pin equalities, and the harmonic Stam 1/J_S ≥ 1/J_X + 1/J_Y — the same shape as the model's h_pos_stam; the harmonic Stam is the single-noise-sum producer's output, threaded per-t). @audit:ok

TT-_tendsto_zero_atTop — the two-time gap tends to 0 as t → ∞ (Gaussian-saturation limit along the matched paths). Mirrors csiszarLogRatioGap_tendsto_zero_atTop (EPI/Case1/RatioLimit/Assembly.lean).

§1 (reduction, sorry-free in this body). Using IsMatchedTimePath.matched_growth (for t ≥ 0, heatFlowEP A B P (s t) = heatFlowEP A B P 0 · eᵗ) and heatFlowEP A B P 0 = entropyPower (P.map A) (the √0 = 0 collapse), the matched-path denominator B t = heatFlowEP X Z_X P (s t) + heatFlowEP Y Z_Y P (r t) equals (eP X + eP Y)·eᵗ, whence log B t = log (eP X + eP Y) + t. Therefore the gap reduces (for t ≥ 0) to R t = log (A t) − log (B t), the log of the EPI saturation ratio A t / B t (A t = sumHeatFlowEP …(s t)(r t) is the numerator). The −t correction is absorbed by the eᵗ growth — established in the body via Real.log_mul/Real.log_exp, no sorry.

§2 (saturation core). The EPI saturation A t / B t → 1 as t → ∞, isolated into have h_ratio_tendsto; from it log (A t / B t) → log 1 = 0 (continuity of log at 1) and log (A/B) = log A − log B (both positive) recover R t → 0. The saturation is reduced to a single limit A t / eᵗ → N(X) + N(Y):

• A t (the matched-sum numerator) is identified with a single-noise heat flow of X+Y at τ = s t + r t via matchedSum_law_eq (@audit:ok), then split by entropyPower_path_scaling as A t = τ · NSr(τ) with NSr(σ) → ν and ν = N(𝒩(0,1)) the common noise entropy power.
• the component asymptotics s t / eᵗ → N(X)/ν, r t / eᵗ → N(Y)/ν come from combining matched growth (N_X(s t) = N(X)·eᵗ) with the scaling identity N_X(s t) = s t · NXr(s t) and the §3 envelope limit NXr(s t) → ν (composed with s, r → ∞). Hence τ / eᵗ → (N(X)+N(Y))/ν, so A t / eᵗ → (N(X)+N(Y)) and the ν factors cancel.

The §3 saturation machinery (entropyPower_rescaled_path_tendsto, IsRescaledPathRegular) is keyed to the single-time rescaling A/√t + B; the matched path uses different times s t ≠ r t, so the re-keying is exactly the matchedSum_law_eq reduction above. No EPI/Stam conclusion is bundled; the added preconditions (noise laws/independences, path divergence s,r → ∞, per-σ scaling regularity, the three IsRescaledPathRegular bundles) are regularity — none of them encodes A t / B t → 1. @audit:ok