From cdb6bdd40b215b9974050b449e0161e31a54bafd Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Sat, 26 Sep 2026 01:58:40 +0000 Subject: [PATCH] Record a nonauthor AMEND review of the shrinking-witness m=2 bound. The divided-difference Jacobian, covariance floor, determinant soft factors, cubic height gap, and separation integral support the uniform O(k r^3) expectation. The probability quantifiers and the second-window transition need a narrow repair. Scientific effect is none. Co-authored-by: Dylan Roy --- .../REVIEW.md | 180 +++++++++++++++++ .../algebra_check.py | 185 ++++++++++++++++++ 2 files changed, 365 insertions(+) create mode 100644 reviews/pr125_shrinking_witness_nonauthor_20260926/REVIEW.md create mode 100644 reviews/pr125_shrinking_witness_nonauthor_20260926/algebra_check.py diff --git a/reviews/pr125_shrinking_witness_nonauthor_20260926/REVIEW.md b/reviews/pr125_shrinking_witness_nonauthor_20260926/REVIEW.md new file mode 100644 index 000000000..c337823b5 --- /dev/null +++ b/reviews/pr125_shrinking_witness_nonauthor_20260926/REVIEW.md @@ -0,0 +1,180 @@ +# Nonauthor review — shrinking witness pairs, divided-difference m=2 bound + +Scientific effect: **NONE**. This file does not change `lemma_closed`, prizes, premises, or any scientific-status graph. It does not edit main pull request 125. It does not infer pin-neighborhood, intermediate-annulus, elder-pairing, or global RN / 24-jet closure. + +## Pickup + +One bounded nonauthor review of the shrinking-witness note. No child agent was launched. + +## Claim + +| Field | Value | +|---|---| +| Object | main pull request 125, `RN-SHRINKING-WITNESS-M2-20260926` | +| Immutable commit | `00c9d08a146c60cfc026f2167c5a1d9e5678e34d` | +| Path | `docs/rn_d5_shrinking_witness_20260926.md` | +| Blob | `d29d00f205f12ee9619651165ee588422d777fd4` | +| Size | 12367 bytes | +| SHA256 | `dc9000136ecab9a0d0269c4760b44400dca8e2f6882d136679b822f07c220333` | +| Companion test blob | `8112f93b340e75945caea442bd0ba81c6a07996a`, 5016 bytes, SHA256 `99ed5aeadc1a90e14370932cbf7c486a0e6351a1ad3f9d2072ad796dca7a6206` | +| Author of the object | Cursor Agent, co-authored with Dylan Roy, on main pull request 125 | +| Scope | Ordered index-`j` pairs inside the fixed remote region `D_ρ`, between-pin window of length `k r^3`, separation in `[η, δ_*]` with `δ_*≤ρ/4` fixed and `η` allowed to approach 0 | +| Interfaces | Divided-difference Jacobian, contact covariance floor, determinant soft factors, shared height-window cubic, separation integral, transition from the fixed-`η` bound | +| Excluded | Pin neighborhoods, the intermediate annulus, elder pairing, a sharp collision kernel, a matching lower bound, and global RN / 24-jet closure | +| State | Delivery record on publication of this file | + +The assigned subject was not retargeted. `frontiers/remote_window_20260924/PROOF.md` was not edited. + +## Reviewer provenance + +| Field | Value | +|---|---| +| Provider | xAI | +| Model | Grok 4.7 (`grok-4.7-high-fast`) | +| Agent | Cursor cloud run `bc-4428875b-e5ff-4f79-a1bb-a0e107ee81c6` | +| Run URL | https://cursor.com/agents/bc-4428875b-e5ff-4f79-a1bb-a0e107ee81c6 | +| Account wrapper | Cursor application, owning user Electric_Universe_Theory | + +Organizational independence is not awarded. This run is a different Cursor session from the session that wrote main pull request 125. A distinct session under the same application and workspace account is not organizational independence. The authoring model of pull request 125 was not available to this run, so provider separation is not claimed. + +## Source exposure + +Read in full: the immutable note above, and its companion test at the same commit. + +Read as the cited outer boundary, at the identity named in the note: Math- `frontiers/remote_window_20260924/PROOF.md`, commit `191ea7d541a486736ba7bbddfd4eac25a6c4567b`, 18355 bytes, SHA256 `a332bae9bdc0106ce17047f7e0409cc3d94eb610a0c7b74ba5ba2d01a1620cb7`. The digest matches the local file. This review uses the Fourier nondegeneracy paragraph in §2, the endpoint comparison (6)–(11), the one-point numerator (14), and the fixed-separation factorial moment (15)–(16). It does not reopen those acceptances and does not extend them. + +Author unit tests were not used as evidence. The Bargmann–Fock sampling figures in §5 of the note were not rerun and are not inputs to the bound. + +## Method + +The Jacobian, the singular-value comparison, the axial and height-gap coefficients, the radial exponent, and the model residual variance were rederived from the Taylor recipe and the Hermite evaluation of `exp(-t^2/2)`. Separately, `algebra_check.py` (standard library only) locks those rational identities and the arithmetic of the height-split ledger used in the transition section below. That ledger is a comparison of majorants. It is not a theorem about the periodized field and it does not replace the note's exponent. + +Command: + +```sh +python3 -B -S reviews/pr125_shrinking_witness_nonauthor_20260926/algebra_check.py +``` + +Script SHA256: `2ffe3a18ee0ee38eca0b5e5be749f21fd5b7cecdcdad22c4212be80475c4269f`. The run printed `all certificates passed`. + +## Dispositions + +| Interface | Disposition | +|---|---| +| Gradient divided-difference Jacobian `δ^d` | **ACCEPT** | +| Contact covariance floor for `(G_0, G_1)` | **ACCEPT** | +| Determinant soft factors, product `O(δ^2)` | **ACCEPT** | +| Shared height-window cubic `-μ δ^3/12` | **ACCEPT** | +| Separation integral `∫ s ds` near zero | **ACCEPT** | +| Exact transition to the fixed-`η` `O(r^6)` bound | **AMEND** | + +Overall disposition: **AMEND**. The expectation bound on `T_{r,j,2}(η)` stands. The printed passage from that bound to a probability for every pair of separation at least `η`, and the sentence that locates the whole second-window loss at the mere permission for `η` to shrink, need the repair in the transition section. No interface is a counterexample. + +## Jacobian — ACCEPT + +On `(G_0, G_1) ∈ R^d × R^d` the map + +`(G_0, G_1) ↦ (∇f(x), ∇f(y)) = (G_0, G_0 + δ G_1)` + +has block matrix `[[I, 0], [I, δ I]]`. Its determinant is `δ^d` for every `d≥1` and every `δ≠0`. The recursive expansion agrees with `δ^d` on dimensions 2, 3, and 4. Because the map is linear and sends the origin to the origin, + +`p_{∇f(x),∇f(y)}(0,0) = δ^{-d} p_{G_0,G_1}(0,0)` + +exactly, wherever the law of `(G_0, G_1)` is nondegenerate. The factor is the change-of-variable determinant of the gradient coordinates. It is not an extra spatial Jacobian. + +## Contact covariance floor — ACCEPT + +`G_1 - H_x u = O(δ)` in every fixed `L^p`, uniformly for `x∈D_ρ` and `|u|=1`, by Taylor expansion with the Lagrange remainder. The contact vector is `(∇f(x), H_x u)`. The `d` gradient functionals and the `d` forms `H ↦ H u` are linearly independent: the second family is surjective on symmetric matrices for every unit `u`. Together with the pin jet `U_0` at distance at least `ρ/2`, these are distinct derivative-evaluation functionals. The Fourier argument in §2 of the outer-boundary note gives a positive-definite joint covariance. That covariance is continuous in `(x, u)` on the compact set `D_ρ × S^{d-1}`, and the conditional covariance of `(∇f(x), H_x u)` given `U_0` is the Schur complement of a positive-definite matrix, hence positive definite at each point. Compactness supplies a positive lower bound. For small `δ_*` and small `r`, the passage from `(U_0, ∇f, H u)` to `(U_r, G_0, G_1)` is a small covariance perturbation, so the conditional covariance of `(G_0, G_1)` given the endpoint pins stays uniformly positive definite. + +The symbol `c_*/2` in the note is existence bookkeeping for that perturbed conditional gap. The gap that has room to be halved is the contact conditional gap. A Gaussian on `R^{2d}` whose covariance eigenvalues are at least that gap has density at the origin at most `(2π)^{-d}(det Σ)^{-1/2}`, and a nonzero conditional mean only decreases the density at `0`. Therefore + +`p_{∇f(x),∇f(y)|U_r}(0,0) ≤ C δ^{-d}`, + +with `C` depending on `d, L, ρ, δ_*, B, K` and independent of `δ` and `η`. + +Adjoining `f(x)` keeps the same conclusion. The value is an order-zero functional, independent of the gradient and of `H u` as a jet. The enlarged observation `(U_r, G_0, G_1, f(x))` remains uniformly nondegenerate for small `δ` and `r`, so conditioning on a height in a fixed compact interval does not remove the divided-difference gap. On the Bargmann–Fock covariance `exp(-|z|^2/2)`, the model calculation is the integer identity `15 - 9 = 6`: the third axial derivative has variance 15, covariance `-3` with the first derivative, and zero covariance with `H u`. That model variance is an illustration. The periodized floor uses the jet argument above. + +## Determinant soft factors — ACCEPT + +For a symmetric matrix and a unit vector, `σ_min(H) ≤ ||H u||` and `σ_max(H) ≤ ||H||_F`, so + +`|det H| ≤ ||H u|| ||H||_F^{d-1}`. + +The square comparison holds on the three `2×2` samples in the note and on three further `3×3` samples with `u = e_1`. + +Under `G_1 = 0`, the vector Taylor expansion gives + +`H_x u = -(δ/2) ∇_u(H_x) u + O(δ^2)`. + +The same expansion from `y` in the direction `-u` gives `||H_y u|| = O(δ)`. The third- and fourth-derivative factors stay bounded in every fixed `L^p` under the conditional law: the observation covariance is uniformly positive definite, the targets `(v_r, 0, 0, t)` stay bounded on the compact mark set, and Gaussian regression does not increase variances of fixed jets. Hölder therefore lifts the two vector bounds to + +`E[ |det H_x|^p |det H_y|^p | U_r, ∇f(x)=∇f(y)=0, f(x)=t ]^{1/p} ≤ C_p δ^2`. + +The endpoint identities `α_M = -6k + O(r M_4)` and `α_S = 6k + O(r M_4)` are consequences of the pins. Their fourth-derivative moments remain uniform under the added divided-difference and height conditioning by the same regression bound. The filtered-determinant comparison (8)–(10) of the outer boundary, applied to those uniform moments, gives `E[(W_r/r^2)^p | …] ≤ C_p`. One further Hölder step, using `F_j ≤ |det|`, gives + +`E[ W_r F_j(H_x) F_j(H_y) | U_r, ∇f(x)=∇f(y)=0, f(x)=t ] ≤ C r^2 δ^2`. + +`Z_r` remains the endpoint-only normalizer. Its accepted limit `Z_r/r^2 = z_0 + O(r)` with `inf z_0 > 0` is an endpoint statement, so for small `r` one has `Z_r ≥ c r^2` in the denominator of the pair formula. Remote pair conditioning changes the law of the numerator weight, which is the conditional expectation already estimated, and leaves that denominator in place. + +The resulting Kac–Rice integrand, after one height disintegration of length `k r^3` and deletion of the second height indicator, is at most `C k r^3 δ^{2-d}`. + +## Shared height-window cubic — ACCEPT + +Let `φ(s) = f(x + s u)` and let `h = φ'`. Impose `h(0) = h(δ) = 0` on a degree-four axial derivative with `h''(0) = μ`, `h'''(0) = ν`, and `h''''(0) = ρ`. Solving for `h'(0)` and integrating produces the exact gap + +`φ(δ) - φ(0) = -μ δ^3/12 - ν δ^4/24 - ρ δ^5/80`. + +The same solve gives `h'(0) = -(δ/2) μ + O(δ^2)` and `h'(δ) = +(δ/2) μ + O(δ^2)`. A pure third derivative forces those axial curvatures to have opposite signs. The degree-four window `μ = -3δ`, `ν = 6` puts both scaled curvatures at `+1/2`; the same fourth derivative with `μ = 0` returns opposite signs. Both evaluations agree with the rational certificates. + +Full vanishing of `∇f(x)` and `∇f(y)` implies vanishing of the axial derivatives, so the cubic applies on the critical-point set. For small `δ`, `||H u|| = O(δ)` in the whole ambient space, and the transverse block sees an axial Schur complement whose leading term is the axial curvature. When `μ` stays away from zero and the transverse Hessian stays a definite distance from the singular set, the indices differ by one. Same-index pairs require a further jet. The upper bound uses `F_j ≤ |det|` and does not need that jet. + +The conditional size of the gap is of order `δ^3` when the third derivative stays of order one. In the Bargmann–Fock model the contact standard deviation is exactly `√6 / 12`, whose square is `1/24`. The note's printed diagnostic `0.204 δ^3` is the three-digit truncation of that coefficient: `(51/250)^2 = 1/24 - 19/375000`. This matches the illustration in §5. It is not an input to the pinned bound. + +## Separation integral — ACCEPT + +The radial calculation is an identity for every `d≥2`: + +`∫_{η≤|h|≤δ_*} |h|^{2-d} dh = |S^{d-1}| ∫_η^{δ_*} s ds = |S^{d-1}| (δ_*^2 - η^2)/2`. + +The exponent `(2-d)+(d-1)` equals 1. The integral increases to `|S^{d-1}| δ_*^2/2` as `η↓0` and remains finite. On the torus, `δ_* ≤ ρ/4 < L/16` keeps the ball inside an injectivity chart, so the Euclidean polar coordinate is the torus coordinate. Pairs that would leave `D_ρ` are a subset of this ball, and the ball integral remains an upper bound. Integrating the center over `D_ρ` contributes a constant multiple of `|D_ρ|`. + +Combined with the integrand `C k r^3 δ^{2-d}` and with `Z_r ≥ c r^2`, this yields the expectation bound as stated for the count whose separation lies in `[η, δ_*]`: + +`E_{Q_r^W}[T_{r,j,2}(η)] ≤ C k r^3`, + +with `C` independent of `η∈(0, δ_*]`. The same majorant bounds the improper integral over `0<|x-y|≤δ_*`. The unnormalized numerator is `O(k r^5)`, the same power as the one-point numerator (14), because one endpoint product `W_r` and one window of length `k r^3` remain, and division by `Z_r` has not yet been taken. + +## Transition to fixed-η `O(r^6)` — AMEND + +Two repairs belong in §3 and §5. After them, the expectation bound above is unchanged. + +**Probability quantifiers.** `T_{r,j,2}(η)` counts ordered pairs whose separation lies in `[η, δ_*]`. Markov's inequality gives + +`P(an unordered index-j pair in the window, with separation in [η, δ_*]) ≤ E[T_{r,j,2}(η)] / 2`. + +The printed event, "separation at least `η`", also contains pairs with separation greater than `δ_*`. Those pairs are estimated by (15) at the fixed separation `δ_*`, so their ordered expectation is `O((k r^3)^2)`. The repaired probability is + +`P(separation at least η) ≤ E[T_{r,j,2}(η)]/2 + O((k r^3)^2)`. + +On the compact mark set, `(k r^3)^2 / (k r^3) = k r^3` tends to 0 with `r`, uniformly for `k∈[k_-, k_+]`. For small `r_*` the second summand is absorbed, and the probability is at most `C k r^3`. The absorption uses the fixed-separation theorem at separation `δ_*`. It does not extend (15) down to `η=0`. + +**Where the second window is lost.** A second factor `k r^3` remains available for every pair whose separation is bounded below by a positive constant independent of `r`. On that set `f(y)-f(x)` has conditional size of order one, and (15) supplies `O((k r^3)^2)`. The cubic gap `-μ δ^3/12` becomes smaller than the window when `δ = O((k r^3)^{1/3})`. That is the scale at which the second height stops producing an independent factor `r^3`. Letting the lower cutoff `η` tend to zero does not move the pairs with `δ` of order `δ_*` onto that scale. + +The identity `∫_η^{δ_*} s ds → δ_*^2/2` is the integral of the majorant after the second height indicator has been deleted. Its positive limit is the reason that deleted-indicator estimate is `O(k r^3)` rather than `O(r^6)`. The mass of that integral sits at separations of order `δ_*`, where the deleted indicator is small and (15) restores a second window. The sentence in §5 that reads this positive limit as the reason a fixed-`η` order `O(r^6)` fails therefore describes the majorant, not the location of the transition. + +A ledger that keeps the second height factor where `δ^3` exceeds the window, and uses the gap density bound coming from a third derivative of order one, integrates a radial piece of order `w^{5/3}` with `w = k r^3`. That arithmetic is certified in `algebra_check.py`. It is a comparison of majorants under those extra modeling assumptions. This review does not promote it to a proved exponent, and the note already leaves a matching lower bound open. + +The fixed-`η` statement (15)–(16) remains the outer boundary for separations bounded below independently of `r`. Its probability `O(r^6)` is the bound in that regime. The divided-difference argument adds a uniform majorant `O(k r^3)` down to separation zero inside `D_ρ`. Uniformity is the gain. Sharpness is not claimed. + +## What this review leaves open + +The following stay outside the amended statement: + +- the mesoscopic neighborhood of the pins and any witness within `O(r)` of `M` or `S`; +- the intermediate annulus, including `r ≪ |x| ≪ ρ`; +- remote critical points with no shrinking height window; +- legacy all-cell, 24-jet, and fixed-`r` inner-wedge selectors; +- a matching lower bound, a numerical constant, and a Poisson or factorial-moment limit for separations tending to zero; +- elder selection and any global RN closure. + +Issue 76 being closed records the fixed-`ρ` / fixed-`η` review. That closure is not a closure of the six items above. diff --git a/reviews/pr125_shrinking_witness_nonauthor_20260926/algebra_check.py b/reviews/pr125_shrinking_witness_nonauthor_20260926/algebra_check.py new file mode 100644 index 000000000..8b9bd87ca --- /dev/null +++ b/reviews/pr125_shrinking_witness_nonauthor_20260926/algebra_check.py @@ -0,0 +1,185 @@ +"""Independent certificates for the main PR125 shrinking-witness review. + +Rational arithmetic only. These checks rederive the note's displayed +identities. They do not sample a Gaussian field, do not evaluate the +periodized pinned kernel, and do not install a sharper radius exponent. +""" +from __future__ import annotations + +from fractions import Fraction + + +def det(matrix): + n = len(matrix) + if n == 1: + return matrix[0][0] + total = 0 + for col, entry in enumerate(matrix[0]): + minor = [row[:col] + row[col + 1 :] for row in matrix[1:]] + total += ((-1) ** col) * entry * det(minor) + return total + + +def jacobian_matrix(dim, delta): + """Columns (G0, G1), rows (G0, G0 + delta G1).""" + size = 2 * dim + matrix = [[Fraction(0) for _ in range(size)] for _ in range(size)] + for i in range(dim): + matrix[i][i] = Fraction(1) + matrix[dim + i][i] = Fraction(1) + matrix[dim + i][dim + i] = delta + return matrix + + +def axial_jets(delta, mu, nu, rho): + """Solve h(delta)=0 for the axial derivative h(0)=0, h'(0) unknown. + + h(s) = alpha*s + mu*s**2/2 + nu*s**3/6 + rho*s**4/24. + The field gap is the integral of h. alpha_far is h'(delta). + """ + alpha = -(mu * delta / 2 + nu * delta**2 / 6 + rho * delta**3 / 24) + alpha_far = alpha + mu * delta + nu * delta**2 / 2 + rho * delta**3 / 6 + gap = ( + alpha * delta**2 / 2 + + mu * delta**3 / 6 + + nu * delta**4 / 24 + + rho * delta**5 / 120 + ) + residual = alpha * delta + mu * delta**2 / 2 + nu * delta**3 / 6 + rho * delta**4 / 24 + return alpha, alpha_far, gap, residual + + +def det3(h11, h12, h13, h22, h23, h33): + return ( + h11 * (h22 * h33 - h23**2) + - h12 * (h12 * h33 - h13 * h23) + + h13 * (h12 * h23 - h13 * h22) + ) + + +def check_jacobian(): + for dim in (2, 3, 4): + for delta in (Fraction(1, 3), Fraction(2, 5), Fraction(1), Fraction(1, 8)): + if det(jacobian_matrix(dim, delta)) != delta**dim: + raise SystemExit(f"jacobian failed dim={dim} delta={delta}") + + +def check_singular_values(): + for alpha, beta, gamma in ( + (Fraction(1, 7), Fraction(1, 7), Fraction(3)), + (Fraction(-2, 5), Fraction(1, 4), Fraction(-6)), + (Fraction(0), Fraction(0), Fraction(4)), + ): + determinant = alpha * gamma - beta**2 + hu2 = alpha**2 + beta**2 + frobenius2 = alpha**2 + 2 * beta**2 + gamma**2 + if determinant**2 > hu2 * frobenius2: + raise SystemExit("d=2 singular-value comparison failed") + samples = ( + (Fraction(1, 3), Fraction(-1, 5), Fraction(2, 7), Fraction(4), Fraction(1, 2), Fraction(-3)), + (Fraction(1, 8), Fraction(0), Fraction(0), Fraction(5), Fraction(1, 9), Fraction(2)), + (Fraction(-1, 2), Fraction(1, 3), Fraction(-1, 4), Fraction(1), Fraction(0), Fraction(6)), + ) + for h11, h12, h13, h22, h23, h33 in samples: + determinant = det3(h11, h12, h13, h22, h23, h33) + hu2 = h11**2 + h12**2 + h13**2 + frobenius2 = ( + h11**2 + h22**2 + h33**2 + 2 * (h12**2 + h13**2 + h23**2) + ) + # |det| <= ||Hu|| ||H||_F^{2} squares to det**2 <= hu2 * (||H||_F^2)**2. + if determinant**2 > hu2 * frobenius2**2: + raise SystemExit("d=3 singular-value comparison failed") + + +def check_height_gap(): + delta, mu, nu, rho = Fraction(2, 7), Fraction(3), Fraction(-5), Fraction(11) + alpha, alpha_far, gap, residual = axial_jets(delta, mu, nu, rho) + if residual != 0: + raise SystemExit("axial derivative was not pinned at distance delta") + if alpha != -(delta / 2) * mu - (delta**2 / 6) * nu - (delta**3 / 24) * rho: + raise SystemExit("near axial coefficient mismatch") + if alpha_far != (delta / 2) * mu + (delta**2 / 3) * nu + (delta**3 / 8) * rho: + raise SystemExit("far axial coefficient mismatch") + if gap != -(mu * delta**3) / 12 - (nu * delta**4) / 24 - (rho * delta**5) / 80: + raise SystemExit("height-gap coefficient mismatch") + alpha, alpha_far, _gap, _residual = axial_jets(Fraction(1, 5), Fraction(4), 0, 0) + if alpha * alpha_far >= 0: + raise SystemExit("pure third derivative did not force opposite signs") + delta = Fraction(1, 4) + alpha, alpha_far, _gap, _residual = axial_jets(delta, delta * Fraction(-3), Fraction(6), 0) + if alpha / delta**2 != Fraction(1, 2) or alpha_far / delta**2 != Fraction(1, 2): + raise SystemExit("fourth-derivative same-sign window failed") + alpha, alpha_far, _gap, _residual = axial_jets(delta, 0, Fraction(6), 0) + if alpha * alpha_far >= 0: + raise SystemExit("pure fourth derivative did not force opposite signs") + + +def check_radial_integral(): + for dim in (2, 3, 5, 8): + if (2 - dim) + (dim - 1) != 1: + raise SystemExit(f"radial exponent failed in dimension {dim}") + eta, radius = Fraction(1, 10**8), Fraction(1, 8) + integral = (radius**2 - eta**2) / 2 + if not (0 < integral < radius**2 / 2): + raise SystemExit("radial integral left the expected range") + if radius**2 / 2 - integral != eta**2 / 2: + raise SystemExit("radial limit identity failed") + + +def check_bargmann_contact_scale(): + # Var(d^3 f / dx^3) = 15, Cov(df/dx, d^3 f/dx^3) = -3, Var(df/dx) = 1. + variance = 15 - ((-3) ** 2) // 1 + if variance != 6: + raise SystemExit("third-derivative residual variance failed") + # (sqrt(6)/12)^2 = 1/24. The printed diagnostic 0.204 is 51/250. + printed = Fraction(51, 250) + difference = Fraction(1, 24) - printed**2 + if difference != Fraction(19, 375000): + raise SystemExit("diagnostic square comparison failed") + if difference <= 0: + raise SystemExit("printed 0.204 is not below sqrt(6)/12") + + +def check_split_majorant_arithmetic(): + """Arithmetic of a height-split ledger. Not a field theorem. + + Integrate w * min(s, w/(kappa s**2)) from 0 to R. The kink is + t = (w/kappa)**(1/3). For w = kappa t**3 the integral equals + (3/2) kappa t**5 - kappa t**6 / R, which is the expanded form of + (3/2) kappa**(-2/3) w**(5/3) - w**2 / (kappa R). + """ + radius = Fraction(1) + kappa = Fraction(1) + for denominator in (2, 8, 100): + split_point = Fraction(1, denominator) + window = kappa * split_point**3 + if split_point >= radius: + raise SystemExit("ledger split point is outside the radius") + integrated = (window * split_point**2) / 2 + (window**2 / kappa) * ( + 1 / split_point - 1 / radius + ) + expected = ( + Fraction(3, 2) * kappa * split_point**5 + - kappa * split_point**6 / radius + ) + if integrated != expected: + raise SystemExit( + f"split ledger mismatch integrated={integrated} expected={expected}" + ) + crude = window * radius**2 / 2 + if crude <= integrated: + raise SystemExit("crude one-window majorant did not exceed the split") + + +def main(): + check_jacobian() + check_singular_values() + check_height_gap() + check_radial_integral() + check_bargmann_contact_scale() + check_split_majorant_arithmetic() + print("all certificates passed") + + +if __name__ == "__main__": + main()