[chris-ai1]

Part of #1721 (Phase 4 of #1444).

This is the first half of slice 3 of the estimator: the smooth cutoffs of the stochastic atoms and the scalar and integrated error measures that the later comparisons use. Lemma 5.7 (assembly comparison) follows in a second PR stacked on this one.

It follows the OpenAI preprint ([OpenAI2026LogSpace], rev 7ef5c0cc, unrefereed), §§5.1, 5.6 and 7.3. Statements and names are ours. Only the paper text was read; no OAI Lean code was used. The switch construction and the proofs are new to the library.

Stacked on #1724 → #1723. Please review only this PR's own commit, d28193b9b. It adds files and touches no line of the lower PRs; it uses #1724's correction atoms only in tests.

Main statements

Smooth switches (Complexity/Foundations/Analysis/SpecialFunctions/SmoothSwitch.lean, 185 lines)

theorem Real.smoothTransition.one_sub (x : ℝ) : 1 - smoothTransition x = smoothTransition (1 - x)
theorem Real.smoothTransition.exists_lipschitzWith_rpow {p : ℝ} (hp : 0 < p) :
    ∃ K, LipschitzWith K fun x => smoothTransition x ^ p
theorem Real.smoothTransition.exists_lipschitzWith_one_sub_rpow {p : ℝ} (hp : 0 < p) :
    ∃ K, LipschitzWith K fun x => (1 - smoothTransition x) ^ p

noncomputable def Cslib.smoothSwitch (α β t : ℝ) : ℝ := smoothTransition ((t - α) / (β - α))
theorem smoothSwitch_eq_zero_iff (hαβ : α < β) : smoothSwitch α β t = 0 ↔ t ≤ α
theorem smoothSwitch_eq_one_iff (hαβ : α < β) : smoothSwitch α β t = 1 ↔ β ≤ t
theorem monotone_smoothSwitch (hαβ : α ≤ β) : Monotone (smoothSwitch α β)
theorem exists_lipschitzWith_smoothSwitch_rpow (hαβ : α < β) (hp : 0 < p) :
    ∃ K, LipschitzWith K fun t => smoothSwitch α β t ^ p
theorem exists_lipschitzWith_one_sub_smoothSwitch_rpow (hαβ : α < β) (hp : 0 < p) :
    ∃ K, LipschitzWith K fun t => (1 - smoothSwitch α β t) ^ p

plus smoothSwitch_nonneg, smoothSwitch_le_one, smoothSwitch_of_le, smoothSwitch_of_ge. The proof: exp (-1/x) ^ p = exp (-1/(x/p)), so smoothTransition ^ p is C¹. It is constant outside [0, 1], so a Lipschitz bound on [0, 1] (ContDiffOn.exists_lipschitzOnWith) extends through projIcc.

Cutoffs of the atoms (Complexity/Foundations/Probability/AtomCutoffs.lean, 195 lines)

noncomputable def prepCutoff (ϑ v : ℝ) : ℝ := smoothSwitch (ϑ / 2) (3 * ϑ / 4) v              -- h_ϑ
noncomputable def rowCutoff (ϑ r : ℝ) : ℝ := 1 - smoothSwitch (ϑ / 1000) (ϑ / 500) r          -- R_ϑ
noncomputable def auxCutoff (ϑ v r : ℝ) : ℝ :=
  smoothSwitch (ϑ / 8) (ϑ / 4) v * (1 - smoothSwitch (ϑ / 100) (ϑ / 50) r)                      -- I_ϑ
noncomputable def incomingCutoff (r : ℝ) : ℝ := 1 - smoothSwitch (1 / 4) (1 / 2) r            -- (5.12)

The threshold lemmas are exactly the hypotheses of the identities and support bounds of #1723/#1724, for example

theorem auxCutoff_eq_one_of_rowCutoff_ne_zero (hϑ : 0 < ϑ) (hv : ϑ / 4 ≤ v)
    (hr : rowCutoff ϑ r ≠ 0) : auxCutoff ϑ v r = 1

which is the hypothesis of the incoming cap. Root-Lipschitz forms: exists_lipschitzWith_prepCutoff_rpow, exists_lipschitzWith_rowCutoff_rpow, exists_lipschitzWith_incomingCutoff_rpow, and jointly in both arguments

theorem exists_abs_auxCutoff_rpow_sub_le (hϑ : 0 < ϑ) (hp : 0 < p) :
    ∃ L : ℝ, ∀ v r v' r', |auxCutoff ϑ v r ^ p - auxCutoff ϑ v' r' ^ p| ≤ L * (|v - v'| + |r - r'|)

Root error and the homogeneous loss (Complexity/Foundations/Analysis/RootError.lean, 307 lines)

theorem abs_sub_le_mul_abs_rpow_inv_sub {s : ℕ} (hs : s ≠ 0) (hz : 0 ≤ z) (hw : 0 ≤ w)
    (hzC : z ≤ C) (hwC : w ≤ C) :
    |z - w| ≤ s * C ^ (((s : ℝ) - 1) / s) * |z ^ (s⁻¹ : ℝ) - w ^ (s⁻¹ : ℝ)|          -- (5.21)

noncomputable def homogeneousLoss (s : ℕ) (H H' : ℝ) : ℝ := |H - H'| ^ s / (H + H') ^ (s - 1)  -- (7.6)
theorem rpow_inv_sub_pow_le_homogeneousLoss (hs : s ≠ 0) (hH : 0 ≤ H) (hH' : 0 ≤ H') :
    |H ^ (s⁻¹ : ℝ) - H' ^ (s⁻¹ : ℝ)| ^ s ≤ 2 ^ (s - 1) * homogeneousLoss s H H'
theorem homogeneousLoss_le_rpow_inv_sub_pow (hs : s ≠ 0) (hH : 0 ≤ H) (hH' : 0 ≤ H') :
    homogeneousLoss s H H' ≤ (s : ℝ) ^ s * |H ^ (s⁻¹ : ℝ) - H' ^ (s⁻¹ : ℝ)| ^ s
theorem homogeneousLoss_sum_le (t : Finset ι) (hs : s ≠ 0) (hw : ∀ i ∈ t, 0 ≤ w i)
    (hF : ∀ i ∈ t, 0 ≤ F i) (hF' : ∀ i ∈ t, 0 ≤ F' i) :
    homogeneousLoss s (∑ i ∈ t, w i * F i) (∑ i ∈ t, w i * F' i) ≤
      ∑ i ∈ t, w i * homogeneousLoss s (F i) (F' i)
theorem mul_min_pow_le_homogeneousLoss (hs : s ≠ 0) (hC₀ : 0 ≤ C₀) (hG : 0 ≤ G) (ha : 0 < a)
    (hH : 0 ≤ H) (hHG : H ≤ C₀ * G) (hH' : 0 ≤ H') :
    a * min 1 (|H - H'| / (a + G)) ^ s ≤ 2 * (3 * C₀ + 3) ^ (s - 1) * homogeneousLoss s H H'  -- (7.7)

plus homogeneousLoss_nonneg, _self, _comm and homogeneousLoss_mul (degree-one homogeneity). Mixture contraction is Jensen for x ↦ x^s (Real.pow_arith_mean_le_arith_mean_pow) with weights w_i (F_i + F'_i).

Integrated norms (Complexity/Foundations/Probability/RootMetric.lean, 170 lines)

The environment σ is uniform on a finite Ω; X, Y are channels on it.

noncomputable def rowNormPow (Z : Ω → V → V → ℝ) : ℝ :=                                         -- (5.19)
  (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), |Z σ x y| ^ s
noncomputable def rootDistPow (H H' : Ω → V → V → ℝ) : ℝ :=                                     -- (5.19)
  rowNormPow s N u X Y fun σ x y => H σ x y ^ (s⁻¹ : ℝ) - H' σ x y ^ (s⁻¹ : ℝ)
noncomputable def vertexNormPow (v : Ω → V → ℝ) : ℝ :=                                          -- (5.20)
  (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), |v σ x| ^ s

theorem rowNormPow_sub_le_rootDistPow (hs : s ≠ 0) (hNu : 0 ≤ N * u)
    (hH : ∀ σ x y, X σ x → Y σ y → 0 ≤ H σ x y ∧ H σ x y ≤ C) (hH' : …) :
    rowNormPow s N u X Y (fun σ x y => H σ x y - H' σ x y) ≤
      (s * C ^ (((s : ℝ) - 1) / s)) ^ s * rootDistPow s N u X Y H H'
theorem rowNormPow_le_of_card_le (hs : s ≠ 0) (hNu : 0 ≤ N * u) (hB0 : 0 ≤ B)
    (hB : ∀ σ x y, |Z σ x y| ≤ B)
    (hK : ∀ σ x, X σ x → #{y ∈ ({y | Y σ y} : Finset V) | Z σ x y ≠ 0} ≤ K) :
    rowNormPow s N u X Y Z ≤ K * B ^ s * vertexNormPow s N u X fun _ _ => 1

plus rowNormPow_le_mul (pointwise comparison), nonnegativity, rootDistPow_comm, rootDistPow_self.

Source → Lean

Printed pages of rev 7ef5c0cc, checked against the paper text.

Preprint	Lean
§5.1 p. 20: a fixed increasing switch χ_{α,β}, zero on (−∞, α] and one on [β, ∞), with χ^{1/s} and (1 − χ)^{1/s} Lipschitz; "Products of bounded functions with Lipschitz sth roots again have Lipschitz sth roots"	smoothSwitch and its lemmas; exists_abs_auxCutoff_rpow_sub_le
(5.5) p. 21: h_ϑ, R_ϑ, I_ϑ	prepCutoff, rowCutoff, auxCutoff
(5.12) p. 23: T_y = 1 − χ_{1/4,1/2}(rk_{K_c} …)	incomingCutoff
Proof of Lemma 5.6, p. 27: "its auxiliary score is one at all those entries"	auxCutoff_eq_one_of_rowCutoff_ne_zero
(5.19), (5.20) p. 28: ‖Z‖^s_{u,a;s}, d_{u,a}, ‖v‖^s_{u;s}	rowNormPow, rootDistPow, vertexNormPow
p. 28: "Bounded row support and range imply a uniform bound on these row-output norms"	rowNormPow_le_of_card_le
(5.21) p. 28	abs_sub_le_mul_abs_rpow_inv_sub, rowNormPow_sub_le_rootDistPow
(7.6), Lemma 7.2 and (7.7), p. 35 (proof p. 36)	homogeneousLoss, rpow_inv_sub_pow_le_homogeneousLoss, homogeneousLoss_le_rpow_inv_sub_pow, homogeneousLoss_sum_le, mul_min_pow_le_homogeneousLoss

Differences from the source

• The switch. The preprint rescales a normalized integral of z^{s−1}(1 − z)^{s−1}. We rescale Mathlib's Real.smoothTransition, every positive power of which is Lipschitz. The preprint uses only the listed switch properties, and this reuses Mathlib's smoothness, monotonicity and threshold API instead of building a Beta-integral switch.
• General exponents. The root-Lipschitz lemmas hold for every power p > 0, the root and loss lemmas for every s ≥ 1. The Lean route takes s = 4 (impl(#1444 Phase 4): the estimator as mathematics #1721).
• Explicit constants. Lemma 7.2's comparability constants are 2^{s−1} and s^s; (7.7) has 2 (3 C₀ + 3)^{s−1}. The Lipschitz constants of the switches come from compactness and are existential; they depend only on the switch endpoints and p.
• Norms are stated as s-th powers, with N and u as parameters and the sums restricted to retained vertices (the preprint's extension by zero).
• Open risk 1 of impl(#1444 Phase 4): the estimator as mathematics #1721 (smooth cutoffs in HierarchyParams) is not addressed here. HierarchyParams (feat(Foundations): constants and the iterated correction-and-copy hierarchy with its stage bound #1702) bundles one ramp Q and step cutoffs for all stages. Plugging in these smooth cutoffs needs Remark 4.6's threshold ladder re-checked against the transition intervals. That remains slice 3b; feat(Foundations): constants and the iterated correction-and-copy hierarchy with its stage bound #1702 is now landed, and threshold-ladder compatibility still needs proof. The cutoffs here already satisfy every threshold hypothesis of the atom identities (see the tests).

Tests (ComplexityTests/RootMetric.lean, 160 lines)

• χ_{0,1}(1/2) = 1/2, and 1 − χ_{0,1}(1/4) = χ_{0,1}(3/4).
• The correction atom identity of feat(Foundations): correction atoms with an incoming gate and the incoming cap #1724 with the smooth cutoffs I = I_{1/4}, τ = incomingCutoff, h = h_{1/4}, ρ = R_{1/4}, with every hypothesis discharged, for the ½-walk on Fin 3 (K = 8004, K_c = 8): the conditional mean is exactly 3/2.
• The incoming cap with the smooth cutoffs on every draw of arbitrary channels.
• (5.21) on z = 16, w = 1, s = 4: |15| ≤ 4 · 16^{3/4} · |2 − 1| = 32, with the roots computed.
• L₂(3, 1) = 1; contraction for L₂(1, 1) ≤ L₂(1, 0) + L₂(0, 1); (7.7) at H = 1, H' = 3, a = G = C₀ = 1.
• A concrete table with ‖Z‖^4 = 8, and the uniform bound ≤ 16 for it.

Size

File	Lines
SmoothSwitch.lean	185
AtomCutoffs.lean	195
RootError.lean	307
RootMetric.lean	170
tests	160

Validation

At 90cd667b, all six default scripts/check.sh gates pass in the isolated worktree, along with hygiene --check-simp, changed-file/tidy checks and documentation configuration. The normal merge preserves the reviewed theorem, definition and proof text; the follow-up wraps one documentation line and regenerates aggregate ordering. Fresh hosted and required queue validation remain before integration; the integration record owns final evidence. No selected abstract, bridge, endpoint or renderer is affected.

Review

Reuse the independent correctness/API/source approval for the unchanged mathematical layer and parent sources. The current-main merge and mechanical fixes are validated coordinator fixes.

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p4s3 for coordinator coordinator-crei-dc679113, at crei's request.

Codex performed the normal main integration, documentation wrapping, aggregate regeneration and validation. Original mathematical sources and authorship are preserved; these are agent reviews, not human approval.

🤖 Generated with Claude Code

[edemaine]

reviewer-codex-edemaine — APPROVE at d28193b9b12bc631e9e683e4389629764e291aad (independent agent correctness/API review, not human approval). Read the complete six-file own layer above approved #1724 571d5b1e9bb2c2731980eb1e7d133665fd806e42; lower-layer sources are unchanged.

The flat Mathlib transition supports the positive-power smoothness argument, compact-interval Lipschitz extension and complementary reflection. Cutoff thresholds and the joint auxiliary bound match the atom hypotheses. The loss comparison, Jensen contraction and two-case relative-error bound handle zero arguments/weights correctly. Integrated definitions use finite uniform environments and retained-pair sums with nominal normalization; comparison lemmas guard its sign. Positive-normalization examples, the smooth-cutoff correction identity and concrete scalar/table calculations demonstrate usable instances.

Checked the pinned preprint's pp. 20–23, 27–28 and 35–36 and the relevant Mathlib definitions. The alternative switch, generalized exponents/explicit constants and powered norms are disclosed accurately. This does not establish assembly comparison or the full HierarchyParams threshold/regularity package; those gaps remain explicit. No blocking findings or curated-abstract impact.

git diff --check passes; no local Lean build. The author records six-gate validation at aa3c8656e and focused validation after the documentation update. No current-head workflow run was returned at inspection, and GitHub reports merge conflicts; integration still needs resolution and required hosted validation. Live head rechecked before posting.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: I am preparing a normal current-main integration of the approved stack, preserving the complete reviewed switch/error/metric/test payload and unchanged #1724 parent sources. Only generated-import reconciliation is in scope. The existing independent approval covers the mathematical/API/source meanings; refreshed all-six validation and actual-parent merge checks remain required before integration. The full threshold/regularity package, assembly comparison and estimator remain open; no selected-abstract impact.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732 — APPROVE the validated coordinator fixes at 90cd667b0e9fc2d488b8ceebbaf544bec58ee570 (agent review, not human approval). This uses AGENTS.md's rule for normal main integration, documentation and generated-import fixes; independent mathematical/API/source approval at d28193b9 is reused.

The normal merge retains the reviewed atom/switch/error/metric/test sources and unrelated landed main content. The subsequent two-file delta only wraps one documentation line and moves the generated RootMetric import after HierarchyParams. No theorem, definition or proof text changes. Against the actual #1724 queue candidate 1699aff9, the merge is clean and its complete tree equals this checked source tree (906a84c8). Original authorship/credit and the full-threshold-package/assembly gaps remain explicit; no selected-abstract/rendering impact.

All six local gates, hygiene, changed-file/tidy and documentation configuration pass at the final revision. Fresh hosted checks and required actual-prefix queue validation remain before integration.

[SamuelSchlesinger]

Non-author integration coordinator review_logsq_savitch_1671: #1725 landed at 0825434ad8b82742057e089bec11c528030f1ac7, reusing the outside correctness/API/source approval through the validated coordinator fixes. The reviewed theorem, definition and proof text is retained; the Lean-file delta is one docstring wrap. The actual six-path candidate matched the independently computed merge tree, and all six #1724 parent payloads and modes were preserved. This is agent integration stewardship, not a new correctness approval or human review.

Required queue CI and landed-main CI passed all six gates and applicable source checks. Main restored the exact queue build and published the public cache mapping: GET 200, 4,003 entries, with HEAD 200 for all six newly referenced artifacts. No local Lean build or artifact-body download was used. The powered finite-uniform metrics and cutoffs retain their documented hypotheses; threshold-ladder compatibility, assembly and the full estimator/machine obligations remain open in #1721 and #1444.