diff --git a/.github/workflows/elder-lower-review.yml b/.github/workflows/elder-lower-review.yml new file mode 100644 index 000000000..dbbddd04c --- /dev/null +++ b/.github/workflows/elder-lower-review.yml @@ -0,0 +1,60 @@ +name: D1 elder lower-bound nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/d1_elder_lower_claude_20260928/**' + - '.github/workflows/elder-lower-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/d1_elder_lower_claude_20260928').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'elder_lower_exact_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['drop-aZ-over-8', 'hessian-sign', 'path-endpoint', + 'weight-power', 'tv-half'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/.github/workflows/p15-overlap-tail-review.yml b/.github/workflows/p15-overlap-tail-review.yml new file mode 100644 index 000000000..c7d35ac14 --- /dev/null +++ b/.github/workflows/p15-overlap-tail-review.yml @@ -0,0 +1,60 @@ +name: P15 overlap and tail nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/p15_overlap_tail_claude_20260928/**' + - '.github/workflows/p15-overlap-tail-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/p15_overlap_tail_claude_20260928').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'p15_exact_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['odd-nonbipartite', 'charge-inactive', 'q-one', 'max-load', + 'interval-swap', 'tail-a3', 'drop-superset-cover'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/.github/workflows/remote-height-review.yml b/.github/workflows/remote-height-review.yml new file mode 100644 index 000000000..d527d5efa --- /dev/null +++ b/.github/workflows/remote-height-review.yml @@ -0,0 +1,60 @@ +name: Remote height-decoupling nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/remote_height_claude_20260928/**' + - '.github/workflows/remote-height-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/remote_height_claude_20260928').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'height_exact_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['no-endpoint-pins', 'gradient-target', 'unscaled-beta', 'indicator-only', + 'lip-constant', 'eps-over-2m', 'a-as-probability', 'p2-r6', 'var-l'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/reviews/d1_elder_lower_claude_20260928/RESULTS.json b/reviews/d1_elder_lower_claude_20260928/RESULTS.json new file mode 100644 index 000000000..931611ed1 --- /dev/null +++ b/reviews/d1_elder_lower_claude_20260928/RESULTS.json @@ -0,0 +1,44 @@ +{ + "checks": { + "G_cubic_critical_data": { + "M_hessian_diag_-6k_-k_over_2_max": true, + "S_hessian_diag_6k_-5k_over_2_saddle": true, + "extra_det_-15_over_2_saddle": true, + "extra_height_-7_over_32": true, + "extra_norm_sq_39_over_16_lt_4": true, + "extra_points_are_critical": true, + "floor_45_over_4_from_3_over_2_and_15_over_2": true, + "pin_gradients_zero": true, + "pins_heights_0_and_minus_k": true, + "weight_product_45k4": true + }, + "LED_ledgers": { + "box_volume_16_eps4_k4_r": true, + "loss_exponent_l_2_3_k_minus_5_3": true, + "radial_jacobian_r_dr": true, + "tilt_ledger_r_times_r4_over_r2_is_r3": true + }, + "NF_pinned_normal_form": { + "F_minus_P_is_O_r_generic_degree6": true, + "P_satisfies_all_six_pins_for_arbitrary_jets": true, + "target_jets_give_G_k": true + }, + "PATH_elder_obstruction": { + "g1_nonincreasing": true, + "g3_prime_ge_9_over_64": true, + "margin_end_above_quarter": true, + "margin_path_above_minus_quarter": true, + "path_end_17_over_64": true, + "path_in_B3": true, + "path_min_-7_over_32": true, + "segment_polynomials_E6": true + }, + "TV_multiplicity": { + "bernoulli_tv_equals_h_random_exact": true, + "counting_inequalities": true + } + }, + "passed": true, + "scientific_effect": "NONE", + "scope": "exact identities only; Gaussian jet-box, conditional C^4 and normalizer steps are argued in REVIEW.md" +} diff --git a/reviews/d1_elder_lower_claude_20260928/REVIEW.md b/reviews/d1_elder_lower_claude_20260928/REVIEW.md new file mode 100644 index 000000000..179c1e6d3 --- /dev/null +++ b/reviews/d1_elder_lower_claude_20260928/REVIEW.md @@ -0,0 +1,222 @@ +# Nonauthor analytic review: direct planar elder lower bound and local window multiplicity (Math-#116) + +Scientific effect: **NONE**. This file does not change `lemma_closed`, prizes, premises, `STATUS`, +`PROOF_INDEX`, `GRAPH`, the candidate registry or any author source. It records verdicts on candidates +C1 and C2 of `reviews/candidates_pending_20260928/CANDIDATES.md`. Integration is a separate act. + +## Object + +| Field | Value | +|---|---| +| Objects | OA-ELDER-LOWER-DENSITY-GAP-20260928-v1 and OA-WINDOW-MULTIPLICITY-LOCAL-20260928-v1 (OpenAI / ChatGPT) | +| Branch / head | `chatgpt/window-multiplicity-laws-20260928` / `0507e3a1dbd3dede84cbeb805947c70aa16ebc36` ([Math-#116](https://github.com/d6g8k5htny-coder/Math-/pull/116)) | +| `ELDER_LOWER_AND_DENSITY_GAP.md` | Git blob `aaefc8da9668e819591dd9db0b34442394f2362e`, 10229 B, SHA256 `8ce05a43bde8e0d718f09e2da1ffe75d3ec5893489254afdbf5b58b602cdba0c` | +| `LOCAL_MULTIPLICITY.md` | Git blob `b5c18aac5529c5f975ee5bb056b304debafc6697`, 13100 B, SHA256 `e6272e8709835ca6290fecb7034fa84832dde08c3c4cc990a48b8019e89e7c8d` | +| Consumed, already on main | [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d…`): §1 selector, §8 maximin, §§9–11 ledger, Theorem A. [IW] `frontiers/intermediate_window_20260928/PROOF.md` (blob `f53a527c…`): (I5). [RM] `frontiers/remote_window_20260924/PROOF.md` (blob `b383bfcc…`): frame and (11). | +| Request | [Owner comment 5877622700](https://github.com/d6g8k5htny-coder/Math-/pull/116#issuecomment-5877622700) | + +## Provenance + +| Field | Value | +|---|---| +| Reviewer | Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3` | +| Relation | Different provider from the OpenAI author. Same GitHub account as every lane, so no organizational independence is claimed. | +| Exposure | I read both modules in full, the #116 README, SOURCE_MAP and PUBLICATION records, and LP §§1, 8–11. I wrote the #106 nonauthor review of LP Theorem A and the §9 repair, the #109 review of [IW], and the #110 remote-collision proof [RC]. The upper halves of (E4), (E11) and (L1) consume objects I reviewed or wrote, so for those halves this review is **not** independent of its inputs. The direct lower halves (E2) and (L1)-lower consume none of them. | +| Author code | The author's `algebra.py` is absent from the PR tree, as `PUBLICATION.json` discloses. **I did not run it and do not claim any execution of it.** | +| Independent checks | `elder_lower_exact_check.py` is my own exact-rational suite, written from the markdown. It checks only finite identities. Every Gaussian step below was argued by hand and is not replaced by those checks. | + +## Verdicts + +The lower result (E2) is judged separately from the parent-dependent (E4) and (E11), as requested. + +| Interface | Verdict | +|---|---| +| (E1) ordinary maximin elder definition and the path obstruction | **ACCEPT**. It is LP §8's definition verbatim; see §1. | +| (E5)–(E6) three-segment path, min `-7k/32`, end `+17k/64`, `k/64` margins | **ACCEPT**. Hand-derived; exact check `PATH_*`. | +| (E7) = (L6)–(L8) pinned normal form, including `-aZ/8` | **ACCEPT**. Hand-derived; exact check on a generic degree-6 field with the pins solved. | +| (L9)–(L11) ten-jet Schur floor through `r = 0`; box mass `>= c r` | **ACCEPT**; see §3. | +| (L12)–(L13) `C^4` control **after** conditioning on the physical jets | **ACCEPT**; see §4. | +| (L5), (L14) `W_r >= c r^4`; full `Z_r <= C r^2`; (E8)/(L15) ledger `r·r^4/r^2` | **ACCEPT**; see §5. | +| **Theorem E1, (E2)–(E3)**: `1 - p_r >= c r^3`, d = 2 | **ACCEPT** at its stated existential scope. | +| **Corollary E2, (E4)**: `c r^3 <= 1 - p_r <= C r^3` | **ACCEPT** as a composition with LP Theorem A, accepted at existential scope in [Math-#106](https://github.com/d6g8k5htny-coder/Math-/pull/106). | +| (E9)–(E11) compact-window loss `Θ(ℓ^{2/3})` | **ACCEPT** as a composition with LP §§9–11 and (E4); see §6. | +| **Theorem L, (L1)**: `c r^3 <= Q^W(A_r) <= Q^W{N_r >= 2} <= C r^3` | **ACCEPT**. The lower bound is direct. The upper bound uses the merged (I5). | +| (L2), (L3) | **ACCEPT** | +| §7, (L16) Bernoulli comparison `TV = h` | **ACCEPT**. Hand-derived; checked exactly on random finite laws. | + +No defect was found. Notes N1–N5 below record observations that strengthen or delimit the text without changing it. + +--- + +## §1 — the obstruction (E1) and why it suffices + +LP §8 defines the ordinary superlevel death height of a local maximum `M` as the maximin `(E1)`, with the empty +supremum for a global maximum. On the generic locus the elder partner of `M` is the unique critical point at height +`d_f(M)`. `S` has height `f(S)`, and critical values are almost surely distinct. So `d_f(M) > f(S)` forces the partner +to differ from `S`. A single admissible path supplies that lower bound: it must end strictly above `f(M) = b` and stay +strictly above `f(S)`. No gradient-flow, separatrix or saddle-connection statement is used, and none is needed. The +event has positive probability, and the generic locus has full measure, so the intersection costs nothing. + +## §2 — the cubic, the path and the normal form + +**Cubic.** For `G_k = k(2X^3 - 3X/2 - 1/2 - 3Z^2/4 - XZ^2)`, `∇G_k = k(6X^2 - 3/2 - Z^2, -(3/2 + 2X)Z)`, and +`G_xx = 12kX`, `G_xz = -2kZ`, `G_zz = -k(3/2 + 2X)`. At `M_* = (-1/2,0)` the Hessian is `diag(-6k,-k/2)` (maximum, +det `3k^2`). At `S_* = (1/2,0)` it is `diag(6k,-5k/2)` (saddle, det `-15k^2`). The heights are `0` and `-k`. The +extra points solve `X = -3/4`, `Z^2 = 15/8`. There `G = k(-27/32 + 9/8 - 1/2) = -7k/32`, `G_zz = 0`, and +det `= -4k^2 Z^2 = -15k^2/2`. Also `|P_±|^2 = 9/16 + 15/8 = 39/16 < 4`. + +**Path.** On `X = -3/4` the `Z`-terms cancel: `-3Z^2/4 - XZ^2 = 0`. So segment 2 is the level line `-7k/32`, and it +passes **through** the extra saddle `P_+` (`√(15/8) ≈ 1.369 < 9/4`). Segment 1 is +`g_1(v) = -3v^2/16 - v^3/32`, which is nonincreasing. Segment 3 has `g_3'(v) = (51 - 36v - 6v^2)/64 >= 9/64`. The +path minimum is `-7k/32` and the end value is `+17k/64`. With `‖F - G_k‖_∞ < k/64` on `B(0,3)` and the exact pin +`F(-1/2,0) = 0`, the path stays above `-15k/64 > -k/4` and ends above `k/4`. Physically, the path stays above +`b - kr^3/4`, ends above `b + kr^3/4 > b`, and `b - kr^3/4 - f(S) = 3kr^3/4`. This is (E3). + +**N1 (level region).** Segment 2 runs along a level line through a saddle of `G_k`. Under perturbation, that line +tilts and the saddle moves. The argument never uses the level or the saddle: it only uses the strict `C^0` margin +`k/64`, which survives every sub-`k/64` perturbation. The author's remark that the proof "does not rely on that level +remaining exactly constant" is therefore correct, and it is the reason the argument works. + +**Normal form (E7)/(L7).** Put `h = r/2`. Cubic Hermite interpolation of the axial data +`f(∓h) = b, b - kr^3` and `f_x(∓h) = 0` gives the leading coefficient `2k`, so `f_xxx(0) = 12k + O(rK)`. It also gives +`f(0) - b = -kr^3/2 + O(r^4 K)`. The half-sums and half-differences of the endpoint expansions of `f_x` and `f_z` +give `f_x(0) = -(r^2/8)f_xxx(0) + O(r^3K)` and `f_z(0) = -(r^2/8)f_xxz(0) + O(r^3K)`, with +`f_xx(0), f_xz(0) = O(r^2 K)`. After the rescaling `(f(rX,rZ) - b)/r^3`: + +- `f_x(0) X/r^2` becomes `-3kX/2`. +- `f_z(0) Z/r^2` becomes `-aZ/8`. +- The cubic terms become `2kX^3`, `(a/2)X^2Z`, `(β/2)XZ^2` and `(c/6)Z^3`. +- `f_zz(0) Z^2/(2r)` becomes `(s/2)Z^2`. +- Every other term is `O(rK)` in `C^2(B(0,3))`. + +This is (L6)–(L7). The `-aZ/8` term is exactly the `f_z(0)` contribution, so dropping it breaks both transverse +gradient pins at order one. The exact check solves the six pins on a generic degree-6 field and confirms +`F - P = O(r)` identically in the free coefficients. The `drop-aZ-over-8` mutant is rejected. + +## §3 — the ten-jet floor through `r = 0` and the box mass (L9)–(L11) + +At `r = 0` the endpoint frame is `U_0 = (f, f_x, f_xx, f_xxx, f_z, f_xz)` at the midpoint. Appending +`J = (f_zz, f_xxz, f_xzz, f_zzz)` gives all `1 + 2 + 3 + 4 = 10` planar jets of order `<= 3`, each exactly once. +A null combination `Σ c_α ∂^α f(0)` would make the polynomial `Σ c_α (iξ)^α` vanish on the whole dual lattice +`(2π/L)Z^2`, because every periodized Gaussian Fourier weight is positive. A nonzero polynomial of degree `<= 3` +cannot vanish on a two-dimensional lattice, so the covariance is positive definite. The divided-difference frame `U_r` is continuous in `r` up to `0` ([RM] §2, LP §3), and frames range +over compact `O(2)`. Hence the joint covariance of `(U_r, J)` has a uniform floor `λ_* > 0` and a uniform ceiling for +`0 <= r <= r_1`. + +By the Schur complement, `J | U_r = v_r` has covariance at least `λ_*` and mean `Cov(J,U)Σ_U^{-1} v_r`. That mean is +bounded because `v_r` is bounded. Its Gaussian density is therefore bounded below by some `ρ_* > 0` on any fixed +compact set. The target box (L10) lies in such a set. Its volume is `(2εkr)(2εk)^3 = 16ε^4k^4r` (exact check), so +`Q_r{J ∈ B_r} >= 16ρ_* ε^4 k_-^4 r`. + +The `r` comes only from the **physical** `f_zz` width `εkr`. Normalizing `f_zz/r` would cancel that factor +illegitimately. The author's warning about this is correct. + +## §4 — `C^4` control after the rare restriction (L12)–(L13) + +Condition on the joint vector `V = (U_r, J)` at a target `(v_r, j)` with `j ∈ B_r`. The regular conditional field is +`F + Cov(F,V)Σ_V^{-1}((v_r,j) - V)`, where `F` is an unconditioned copy. The kernel is real-analytic, and the +observations are divided differences of order `<= 3` (averages of derivatives). So each coefficient function +`Cov(F(·),V_i)` has a uniformly bounded `C^4` norm, and `Σ_V^{-1}` is uniformly bounded by §3. The targets are bounded. +Therefore +`E[‖f‖_{C^4}^p | V = (v_r,j)] <= C_p(1 + E‖F‖_{C^4}^p + E|V|^p)`, uniformly. Choose `K` by Markov so the conditional +probability of `{‖f‖_{C^4} <= K}` is at least `1/2` at **every** target. Integrating over the box gives +`Q_r{J ∈ B_r, ‖f‖_{C^4} <= K} >= (c_J/2) r`. + +This is the correct order of operations. Subtracting a fixed unconditioned tail from an event of mass `O(r)` would +fail. + +**N2 (constants).** The dependency chain is acyclic. `ε` fixes the box and `c_J(ε)`. `K` is uniform over all targets +with `ε <= 1`. `r_*` is then chosen from `ε` and `K`. The `C^0` gap between `P` and `G_k` on `B(0,3)` on the box is at +most `εk(9/2 + 111/8 + 27/2 + 9/2) < 37εk`, so `ε < 1/4800` suffices for a `k/128` share of the `k/64` budget. + +## §5 — tilt and normalizer (L5), (L14), (E8) + +`F(X,Z) = (f(rX,rZ) - b)/r^3` gives `∇²f = r ∇²F`. In `d = 2`, each physical determinant is `r^2` times the scaled one. +On the event, the scaled pinned Hessians are `C^2`-close to `diag(-6k,-k/2)` and `diag(6k,-5k/2)`, so both indices +persist. With the author's floors `3/2 k^2` and `15/2 k^2`, `W_r >= (45/4)k_-^4 r^4` (exact check: weight `45k^4` and +floor `45/4`). + +For the full normalizer, `f_x(M) = f_x(S) = 0` gives `∫_0^1 f_xx(M + t r e_1) dt = 0`, so `|f_xx(M)| <= r‖f‖_{C^3}`. +Likewise `f_z(M) = f_z(S) = 0` gives `|f_xz(M)| <= r‖f‖_{C^3}`. Hence +`|det H_M| <= 2r‖f‖_{C^2}‖f‖_{C^3}` and the same holds at `S`, so `W_r <= C r^2 (1 + ‖f‖_{C^3})^4`. The uniform `Q_r` +moments then give `Z_r <= C_Z r^2`. `Z_r > 0` because the event above has positive probability. The normalizer is +the **full** `E_{Q_r} W_r`, not a restricted one. The ledger is `r · r^4 / r^2 = r^3` (exact check, `weight-power` +mutant rejected). + +## §6 — composition (E4), (E9)–(E11) + +(E4)'s upper half is LP Theorem A, `1 - p_r <= C r^3` uniformly over `B × K × O(d)`. It is accepted at existential +scope in [Math-#106](https://github.com/d6g8k5htny-coder/Math-/pull/106), merged at `5eba8f7`. + +(E9) is LP (10.2) verbatim: `A_r = 12 π_r(v_r) Z_r/r^2`, with no factor `1/2`. LP (11.1) gives +`r dr/dℓ = (1/3)k^{-2/3}ℓ^{-1/3}` (exact check `radial_jacobian_r_dr`). Multiplying by `1 - p ≍ r^3 = ℓ/k` gives the +integrand order `ℓ^{2/3}k^{-5/3}` (exact check `loss_exponent_*`). The lower half uses (E2) and `inf A_r > 0`. The +upper half is LP §11's display. + +LP §§8–15 interfaces are accepted by the +[D1-A–E review](https://github.com/d6g8k5htny-coder/main/issues/63#issuecomment-5841570965). The §9 Borel repair is +accepted in #106 Part II. + +**N3 (sharpness of Theorem A in d = 2).** (E4) makes Theorem A's `r^3` rate sharp in order for `d = 2`, uniformly on +the compact marks. This **supersedes** the remark in my #106 review, where sharpness was restricted to the (6.1)/(6.2) +matrix relaxation. That restriction remains correct for the relaxation statement. The Gaussian rate itself is now +shown sharp by the direct event, not by the relaxation. Consequently LP's `O(ℓ^{2/3})` selection-density loss cannot +be improved to `o(ℓ^{2/3})` in `d = 2`. Nothing is said about `d > 2` or about the leading constant. + +## §7 — local multiplicity (L1)–(L3), (L16) + +Choose disjoint closed disks about `P_±` inside `B(0,2)`, away from `M_*` and `S_*`. By the implicit function theorem +applied to `∇G_1` at nondegenerate zeros, there is a `C^2` neighborhood with one saddle per disk and heights in +`(-1, 0)`. Positive scaling by `k` preserves critical points and indices, scales heights by `k` and determinants by +`k^2`. So the neighborhood is uniform over `[k_-, k_+]`, and on the §3–§5 event (with the smaller `ε` for `C^2`) both +witnesses exist with physical heights in `I_r`. This gives the lower half of (L1) with the same `r · r^4/r^2` +ledger. + +The upper half is `1{N >= 2} <= N/2` together with (I5) summed over indices. (I5) is merged +([Math-#107](https://github.com/d6g8k5htny-coder/Math-/pull/107) and my review in [Math-#109](https://github.com/d6g8k5htny-coder/Math-/pull/109)). (L2) follows from +`N(N-1) >= 2·1{N >= 2}`, and (L3) from dividing (L1) by `Q^W{N >= 1} <= C r^3` (exact check `counting_inequalities`). + +For (L16), write `σ` for the singleton submeasure, `η` for the mean measure on `{N >= 2}`, `h = η(S)` and +`α = P(N >= 2)`. Then `Law Ξ - Ber(μ)` has signed masses `h - α >= 0` on the empty stratum, `-η` on singletons and +`α` on multiples. The total variation is `2h`, so the probability TV is exactly `h`, and `2α <= h <= m_r`. Because `-η` has one +sign, its variation is its mass, so the check may aggregate the singleton stratum. It verifies `TV = h` on 1000+ +random exact count laws with a nontrivial multiple stratum. The `tv-half` mutant is +rejected. + +**N4 (the #110 scope).** (L1)–(L2) show that a torus-wide `O(r^5)` factorial bound is false. This confirms that the +fixed-radius `D_ρ` restriction in the merged remote-collision proof ([Math-#110](https://github.com/d6g8k5htny-coder/Math-/pull/110)) +was necessary, not a proof convenience. There is no conflict: `A_r` occurs within distance `O(r)` of the pins. + +**N5 (one box, two conclusions).** The same jet box, intersected with the smaller `C^2` neighborhood, carries both +(E3) and `A_r`. This does not mean every two-saddle configuration defeats the elder pairing, and the source does not +claim that (LOCAL §8: "`A_r` by itself does not determine elder pairing"). + +## Checks run + +``` +python3 -B -S elder_lower_exact_check.py # rc 0, stdout == RESULTS.json +python3 -B -O -S elder_lower_exact_check.py # rc 0, byte-identical +python3 -B -S elder_lower_exact_check.py --mutant drop-aZ-over-8 # rc 1 +python3 -B -S elder_lower_exact_check.py --mutant hessian-sign # rc 1 +python3 -B -S elder_lower_exact_check.py --mutant path-endpoint # rc 1 +python3 -B -S elder_lower_exact_check.py --mutant weight-power # rc 1 +python3 -B -S elder_lower_exact_check.py --mutant tv-half # rc 1 +``` + +Python standard library only. The workflow `.github/workflows/elder-lower-review.yml` verifies the packet tree against +`SOURCE_FILES.json`, replays both modes and requires every mutant to be rejected. + +## Not established here + +- `REMOTE_PAIR_LAW.md`, `REMOTE_DISTANCE_MOMENTS.md`, `HEIGHT_MARKS.md` (C3–C5). The owner routed these to Grok/Harper. +- Numerical `c`, `r_*`, or any leading constant. The results are existential. +- `d > 2`, a shrinking gap mark, a growing torus, all-height counts, or a global second factorial moment upper bound + (C6). +- A runnable reproduction of the author's suite. It is absent from the tree and was not run. +- Organizational independence: all lanes share one GitHub account. + +A non-Claude review of §§3–5 (the Gaussian steps) remains welcome before any status integration. + +## Revision history + +- **v1**, reviewing head `0507e3a`: initial packet. diff --git a/reviews/d1_elder_lower_claude_20260928/SOURCE_FILES.json b/reviews/d1_elder_lower_claude_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..33a83598f --- /dev/null +++ b/reviews/d1_elder_lower_claude_20260928/SOURCE_FILES.json @@ -0,0 +1,43 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#116", + "head": "0507e3a1dbd3dede84cbeb805947c70aa16ebc36", + "paths": [ + { + "path": "frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md", + "git_blob": "aaefc8da9668e819591dd9db0b34442394f2362e", + "bytes": 10229, + "sha256": "8ce05a43bde8e0d718f09e2da1ffe75d3ec5893489254afdbf5b58b602cdba0c" + }, + { + "path": "frontiers/window_multiplicity_laws_20260928/LOCAL_MULTIPLICITY.md", + "git_blob": "b5c18aac5529c5f975ee5bb056b304debafc6697", + "bytes": 13100, + "sha256": "e6272e8709835ca6290fecb7034fa84832dde08c3c4cc990a48b8019e89e7c8d" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 16640, + "sha256": "53bd5289a2060ce6c906023ed09a5aec457313e782135e1df86e743941839495", + "git_blob": "179c1e6d3d4005b2e406b1bd4d9584caf5465793" + }, + { + "path": "elder_lower_exact_check.py", + "bytes": 14334, + "sha256": "f46409953e138147211d2fdf9fd9cddcd757c7cf6d4867b01b04691d0559a654", + "git_blob": "b35cf96a977f3048efafb5bbc74e397037a91ace" + }, + { + "path": "RESULTS.json", + "bytes": 1487, + "sha256": "4a431a8a3fa1527339aa25bac3f1ff22168529aadbb45e437add2257d58e35aa", + "git_blob": "931611ed14c4d210aa8e579c9e5c8b732fcaea61" + } + ] +} diff --git a/reviews/d1_elder_lower_claude_20260928/elder_lower_exact_check.py b/reviews/d1_elder_lower_claude_20260928/elder_lower_exact_check.py new file mode 100644 index 000000000..b35cf96a9 --- /dev/null +++ b/reviews/d1_elder_lower_claude_20260928/elder_lower_exact_check.py @@ -0,0 +1,383 @@ +"""Independent exact checks for the nonauthor review of Math-#116's direct elder lower bound +(ELDER_LOWER_AND_DENSITY_GAP.md) and local multiplicity module (LOCAL_MULTIPLICITY.md). + +Python standard library only; exact rational / Laurent-polynomial arithmetic. Written without the +author's (unpublished) algebra.py. Groups: + + NF (E7)/(L6)-(L7): a GENERIC degree-six planar field with the six actual pins solved exactly + satisfies (f(rX,rZ)-b)/r^3 = P_{k,s,a,beta,c} + O(r) with s=f_zz(0)/r, including -aZ/8; + P itself satisfies all six pins for arbitrary (s,a,beta,c); dropping -aZ/8 breaks them. + G G_k: pins, the four critical points, heights, Hessians, determinants, |P_pm|^2 = 39/16. + PATH the three segment polynomials (E6), their monotonicity, min -7k/32, end +17k/64, the k/64 + margins, and containment in B(0,3). + LED weight 45k^4 and floor 45/4, box volume 16 eps^4 k^4 r, tilt ledger r*r^4/r^2 = r^3, + radial Jacobian r dr = (1/3) l^(-1/3) k^(-2/3) dl and the loss exponent l^(2/3) k^(-5/3). + TV the exact Bernoulli-comparison total variation h on random exact laws, and the counting + inequalities 1{N>=2} <= N/2, N(N-1) >= 2*1{N>=2}. + +Not a continuum or Gaussian proof: the jet-box density floor, conditional C^4 control and the +normalizer bound are argued in REVIEW.md. +""" +import argparse +import itertools +import json +import random +import sys +from fractions import Fraction as F + + +def _mono_mul(a, b): + d = dict(a) + for v, e in b: + n = d.get(v, 0) + e + if n: + d[v] = n + else: + d.pop(v, None) + return tuple(sorted(d.items())) + + +class P: + __slots__ = ("t",) + + def __init__(self, t=None): + self.t = {m: c for m, c in (t or {}).items() if c != 0} + + @staticmethod + def c(x): + return P({(): F(x)}) + + @staticmethod + def v(name, e=1): + return P({((name, e),): F(1)}) + + @staticmethod + def lift(o): + return o if isinstance(o, P) else P.c(o) + + def __add__(self, o): + o = P.lift(o) + t = dict(self.t) + for m, c in o.t.items(): + t[m] = t.get(m, 0) + c + return P(t) + + __radd__ = __add__ + + def __neg__(self): + return P({m: -c for m, c in self.t.items()}) + + def __sub__(self, o): + return self + (-P.lift(o)) + + def __rsub__(self, o): + return P.lift(o) - self + + def __mul__(self, o): + o = P.lift(o) + t = {} + for m1, c1 in self.t.items(): + for m2, c2 in o.t.items(): + m = _mono_mul(m1, m2) + t[m] = t.get(m, 0) + c1 * c2 + return P(t) + + __rmul__ = __mul__ + + def __pow__(self, n): + out = P.c(1) + for _ in range(n): + out = out * self + return out + + def is_zero(self): + return not self.t + + def d(self, name): + t = {} + for m, c in self.t.items(): + dm = dict(m) + e = dm.get(name, 0) + if e == 0: + continue + if e == 1: + dm.pop(name) + else: + dm[name] = e - 1 + key = tuple(sorted(dm.items())) + t[key] = t.get(key, 0) + c * e + return P(t) + + def antider(self, name): + t = {} + for m, c in self.t.items(): + dm = dict(m) + e = dm.get(name, 0) + if e == -1: + raise ValueError("log term") + dm[name] = e + 1 + key = tuple(sorted(dm.items())) + t[key] = t.get(key, 0) + c / (e + 1) + return P(t) + + def subs(self, name, q): + q = P.lift(q) + out = P() + for m, c in self.t.items(): + dm = dict(m) + e = dm.pop(name, 0) + if e < 0: + raise ValueError("negative power substitution") + rest = P({tuple(sorted(dm.items())): c}) + out = out + rest * (q ** e) + return out + + def integrate(self, name, lo, hi): + a = self.antider(name) + return a.subs(name, hi) - a.subs(name, lo) + + def coeff(self, name, e): + """Coefficient of name^e (as a polynomial in the other variables).""" + t = {} + for m, c in self.t.items(): + dm = dict(m) + if dm.get(name, 0) != e: + continue + dm.pop(name, None) + key = tuple(sorted(dm.items())) + t[key] = t.get(key, 0) + c + return P(t) + + def exponents(self, name): + return sorted({dict(m).get(name, 0) for m in self.t}) + + +def det(M): + n = len(M) + total = P() + for perm in itertools.permutations(range(n)): + inv = sum(1 for i in range(n) for j in range(i + 1, n) if perm[i] > perm[j]) + term = P.c(-1 if inv % 2 else 1) + for i in range(n): + term = term * M[i][perm[i]] + total = total + term + return total + + +def adj(M): + n = len(M) + out = [[P() for _ in range(n)] for _ in range(n)] + for i in range(n): + for j in range(n): + minor = [[M[a][b] for b in range(n) if b != j] for a in range(n) if a != i] + cof = det(minor) if minor else P.c(1) + out[j][i] = cof if (i + j) % 2 == 0 else -cof + return out + + +def at(p, X1, X2): + return p.subs("x", X1).subs("z", X2) + + +def hermite(gm, gp, dgm, dgp, a, ainv): + s0 = (gm + gp) * F(1, 2) + d0 = (gp - gm) * ainv * F(1, 2) + s1 = (dgm + dgp) * F(1, 2) + d1 = (dgp - dgm) * ainv * F(1, 2) + return s0 - a * a * d1 * F(1, 2), (3 * d0 - s1) * F(1, 2), d1, 3 * (s1 - d0) * ainv * ainv + + +def pinned_generic(deg=6): + x, z = P.v("x"), P.v("z") + f = P() + for i in range(deg + 1): + for j in range(deg + 1 - i): + f = f + P.v("c%d%d" % (i, j)) * x ** i * z ** j + R, RI = P.v("r"), P.v("r", -1) + a, ai = R * F(1, 2), 2 * RI + b, k = P.v("b"), P.v("k") + h = sum((P.v("c%d0" % i) * x ** i for i in range(4, deg + 1)), P()) + q = sum((P.v("c%d1" % i) * x ** i for i in range(2, deg)), P()) + Ht = hermite(b, b - k * R ** 3, P.c(0), P.c(0), a, ai) + hh = hermite(h.subs("x", -a), h.subs("x", a), h.d("x").subs("x", -a), h.d("x").subs("x", a), a, ai) + sol = { + "c00": Ht[0] - hh[0], "c10": Ht[1] - hh[1], + "c20": (Ht[2] - hh[2]) * F(1, 2), "c30": (Ht[3] - hh[3]) * F(1, 6), + "c01": -(q.subs("x", a) + q.subs("x", -a)) * F(1, 2), + "c11": -(q.subs("x", a) - q.subs("x", -a)) * ai * F(1, 2), + } + for nm, val in sol.items(): + f = f.subs(nm, val) + return f + + +def Ppoly(X, Z, k, s, a, beta, c, mut): + lin = F(0) if mut == "drop-aZ-over-8" else F(1) + return (2 * k * X ** 3 - F(3, 2) * k * X - k * F(1, 2) + s * F(1, 2) * Z * Z + + a * F(1, 2) * (X * X - lin * F(1, 4)) * Z + beta * F(1, 2) * X * Z * Z + c * F(1, 6) * Z ** 3) + + +def check_nf(mut): + out = {} + R = P.v("r") + f = pinned_generic() + X, Z = P.v("X"), P.v("Z") + b, k = P.v("b"), P.v("k") + Fsc = (at(f, R * X, R * Z) - b) * P.v("r", -3) + s = 2 * P.v("c02") * P.v("r", -1) + a, beta, c = 2 * P.v("c21"), 2 * P.v("c12"), 6 * P.v("c03") + Pp = Ppoly(X, Z, k, s, a, beta, c, mut) + diff = Fsc - Pp + ex = diff.exponents("r") + out["F_minus_P_is_O_r_generic_degree6"] = (not ex) or min(ex) >= 1 + # P satisfies all six pins for arbitrary (s,a,beta,c) (scaled pins: F(-1/2,0)=0, F(1/2,0)=-k, grad=0). + ss, aa, bb, cc = P.v("s"), P.v("a"), P.v("bt"), P.v("cc") + Pg = Ppoly(X, Z, k, ss, aa, bb, cc, mut) + ev = lambda p, u, w: p.subs("X", P.c(u)).subs("Z", P.c(w)) + pins = [ev(Pg, F(-1, 2), 0), ev(Pg, F(1, 2), 0) + k, + ev(Pg.d("X"), F(-1, 2), 0), ev(Pg.d("X"), F(1, 2), 0), + ev(Pg.d("Z"), F(-1, 2), 0), ev(Pg.d("Z"), F(1, 2), 0)] + out["P_satisfies_all_six_pins_for_arbitrary_jets"] = all(p.is_zero() for p in pins) + # Target jets give G_k. + Gk = k * (2 * X ** 3 - F(3, 2) * X - F(1, 2) - F(3, 4) * Z * Z - X * Z * Z) + Pt = Ppoly(X, Z, k, -F(3, 2) * k, P.c(0), -2 * k, P.c(0), mut) + out["target_jets_give_G_k"] = (Pt - Gk).is_zero() + return out + + +def check_g(mut): + out = {} + k = F(1) + G = lambda X, Z: k * (2 * X ** 3 - F(3, 2) * X - F(1, 2) - F(3, 4) * Z * Z - X * Z * Z) + GX = lambda X, Z: k * (6 * X * X - F(3, 2) - Z * Z) + GZ = lambda X, Z: -k * (F(3, 2) + 2 * X) * Z + hess = lambda X, Z: (12 * k * X, -2 * k * Z, k * (-F(3, 2) - 2 * X)) + out["pins_heights_0_and_minus_k"] = G(F(-1, 2), 0) == 0 and G(F(1, 2), 0) == -k + out["pin_gradients_zero"] = all(GX(u, 0) == 0 and GZ(u, 0) == 0 for u in (F(-1, 2), F(1, 2))) + hm, hs = hess(F(-1, 2), 0), hess(F(1, 2), 0) + sgn = -1 if mut == "hessian-sign" else 1 + out["M_hessian_diag_-6k_-k_over_2_max"] = hm == (sgn * -6 * k, 0, -k / 2) and hm[0] < 0 and hm[2] < 0 + out["S_hessian_diag_6k_-5k_over_2_saddle"] = hs == (6 * k, 0, -F(5, 2) * k) + # Extra critical points: X=-3/4, Z^2 = 15/8 (use z2 in place of Z^2; Z only enters via Z^2 or Z*Z). + z2 = F(15, 8) + Xp = F(-3, 4) + out["extra_points_are_critical"] = (6 * Xp * Xp - F(3, 2) - z2 == 0) and (F(3, 2) + 2 * Xp == 0) + height = 2 * Xp ** 3 - F(3, 2) * Xp - F(1, 2) - (F(3, 4) + Xp) * z2 + out["extra_height_-7_over_32"] = height == F(-7, 32) and -1 < height < 0 + det_extra = (12 * Xp) * (-F(3, 2) - 2 * Xp) - 4 * z2 + out["extra_det_-15_over_2_saddle"] = det_extra == F(-15, 2) + out["extra_norm_sq_39_over_16_lt_4"] = Xp * Xp + z2 == F(39, 16) and Xp * Xp + z2 < 4 + out["weight_product_45k4"] = abs(hm[0] * hm[2]) * abs(hs[0] * hs[2]) == 45 + out["floor_45_over_4_from_3_over_2_and_15_over_2"] = F(3, 2) * F(15, 2) == F(45, 4) + return out + + +def check_path(mut): + out = {} + v = P.v("v") + k = F(1) + Gp = lambda X, Z: (2 * X ** 3 - F(3, 2) * X - F(1, 2) - F(3, 4) * Z * Z - X * Z * Z) * k + last = (F(-1), F(2)) if mut == "path-endpoint" else (F(-1), F(9, 4)) + V = [(F(-1, 2), F(0)), (F(-3, 4), F(0)), (F(-3, 4), F(9, 4)), last] + segs = [] + for (x0, z0), (x1, z1) in zip(V, V[1:]): + X = x0 + (x1 - x0) * v + Z = z0 + (z1 - z0) * v + segs.append(Gp(X, Z)) + want = [-F(3, 16) * v ** 2 - F(1, 32) * v ** 3, P.c(F(-7, 32)), + F(-7, 32) + F(51, 64) * v - F(9, 32) * v ** 2 - F(1, 32) * v ** 3] + out["segment_polynomials_E6"] = all((s - w).is_zero() for s, w in zip(segs, want)) + ev = lambda p, t: p.subs("v", P.c(t)).t.get((), F(0)) + g1p, g3p = segs[0].d("v"), segs[2].d("v") + grid = [F(i, 400) for i in range(401)] + out["g1_nonincreasing"] = all(ev(g1p, t) <= 0 for t in grid) and ev(segs[0].d("v").d("v"), F(0)) <= 0 + # g3' is a decreasing quadratic on [0,1] (g3'' = -9/16 - 3v/16 < 0), so its minimum is g3'(1). + out["g3_prime_ge_9_over_64"] = ev(g3p, F(1)) == F(9, 64) and all(ev(g3p.d("v"), t) < 0 for t in grid) + vals = [ev(s, t) for s in segs for t in grid] + out["path_min_-7_over_32"] = min(vals) == F(-7, 32) + out["path_end_17_over_64"] = ev(segs[2], F(1)) == F(17, 64) + out["margin_path_above_minus_quarter"] = F(-7, 32) - F(1, 64) == F(-15, 64) and F(-15, 64) > F(-1, 4) + out["margin_end_above_quarter"] = F(17, 64) - F(1, 64) == F(1, 4) + out["path_in_B3"] = max(x * x + z * z for x, z in V) == F(97, 16) and F(97, 16) < 9 + return out + + +def check_led(mut): + out = {} + eps, k, r = P.v("eps"), P.v("k"), P.v("r") + vol = (2 * eps * k * r) * (2 * eps * k) ** 3 + out["box_volume_16_eps4_k4_r"] = (vol - 16 * eps ** 4 * k ** 4 * r).is_zero() + wpow = 3 if mut == "weight-power" else 4 + out["tilt_ledger_r_times_r4_over_r2_is_r3"] = 1 + wpow - 2 == 3 + # Radial Jacobian with k = t^3 and r = q (so l = k r^3 = t^3 q^3, l^(1/3) = t q): + # r dr = q dq, dl = 3 t^3 q^2 dq => r dr / dl = 1/(3 t^3 q); (1/3) l^(-1/3) k^(-2/3) = 1/(3 t q t^2). + t, q = P.v("t"), P.v("q") + lhs = q * P.v("t", -3) * P.v("q", -2) * F(1, 3) # r dr / dl = q / (3 t^3 q^2) + rhs = F(1, 3) * P.v("t", -1) * P.v("q", -1) * P.v("t", -2) + out["radial_jacobian_r_dr"] = (lhs - rhs).is_zero() + # Loss: l^(-1/3) k^(-2/3) * (1-p ~ r^3 = l/k): exponents of (l, k) = (-1/3 + 1, -2/3 - 1). + le, ke = F(-1, 3) + 1, F(-2, 3) - 1 + out["loss_exponent_l_2_3_k_minus_5_3"] = (le, ke) == (F(2, 3), F(-5, 3)) + return out + + +def check_tv(mut): + rng = random.Random(116) + ok_tv, ok_cnt = True, True + nontrivial = 0 + for _ in range(2000): + # A random law of the count N in {0..6} with mean m <= 1 (heavy mass at N = 0). + pN = [F(rng.randrange(300, 1000))] + [F(rng.randrange(0, 30)) for _ in range(6)] + tot = sum(pN) + pN = [x / tot for x in pN] + m = sum(n * pN[n] for n in range(7)) + if m > 1: + continue + s1 = pN[1] + h = sum(n * pN[n] for n in range(2, 7)) + alpha = sum(pN[n] for n in range(2, 7)) + # Law minus Bernoulli(mean): empty (1-m) vs P(N=0); singleton mean mass s1+h vs s1; multiples alpha. + diff_empty = pN[0] - (1 - m) + diff_single = s1 - (s1 + h) + diff_mult = alpha + tv = (abs(diff_empty) + abs(diff_single) + abs(diff_mult)) / 2 + target = h if mut != "tv-half" else h / 2 + ok_tv &= tv == target and h >= 2 * alpha + nontrivial += h > 0 + for N in range(40): + ok_cnt &= F(int(N >= 2)) <= F(N, 2) and N * (N - 1) >= 2 * int(N >= 2) + return {"bernoulli_tv_equals_h_random_exact": ok_tv and nontrivial >= 1000, + "counting_inequalities": ok_cnt} + + +MUTANTS = ("drop-aZ-over-8", "hessian-sign", "path-endpoint", "weight-power", "tv-half") + + +def flatten(d): + for v in d.values(): + if isinstance(v, dict): + yield from flatten(v) + else: + yield v + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + mut = ap.parse_args().mutant + groups = { + "NF_pinned_normal_form": check_nf(mut), + "G_cubic_critical_data": check_g(mut), + "PATH_elder_obstruction": check_path(mut), + "LED_ledgers": check_led(mut), + "TV_multiplicity": check_tv(mut), + } + passed = all(flatten(groups)) + res = {"checks": groups, "passed": passed, "scientific_effect": "NONE", + "scope": "exact identities only; Gaussian jet-box, conditional C^4 and normalizer steps are argued in REVIEW.md"} + sys.stdout.write(json.dumps(res, indent=2, sort_keys=True) + "\n") + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/reviews/p15_overlap_tail_claude_20260928/RESULTS.json b/reviews/p15_overlap_tail_claude_20260928/RESULTS.json new file mode 100644 index 000000000..60cec87c3 --- /dev/null +++ b/reviews/p15_overlap_tail_claude_20260928/RESULTS.json @@ -0,0 +1,51 @@ +{ + "checks": { + "COL_colouring": { + "E4_triangle_shared_4_full_5": true, + "bipartite_arbitrary_capacity_formula_equals_oracle": true, + "doubled_triangle_capacity_one_chi_6_formula_4": true, + "read_two_nonbipartite_even_capacity_formula_equals_oracle": true + }, + "HAZ_product_hazards": { + "overlap_5_8_exceeds_9_16_and_CS": true, + "read_q_product_inequality_arbitrary_events": true, + "two_sided_cauchy_schwarz_bipartite": true, + "weighted_load_sum_not_max": true + }, + "OBS_obstruction_cover": { + "O4_exact_obstruction_equals_active_full_blocks": true, + "chi_whole_ground_K_plus_1": true, + "duplicate_and_superset_removal_keeps_cover": true, + "inactive_full_block_not_obstruction": true + }, + "TAIL_reference_tails": { + "512_25_exceeds_87_32_cubed": true, + "R1_a3_markov_insufficient_direct_tail_below_q9": true, + "R1_a3_monotone_in_trials": true, + "R1_odd_a_ge_5_markov_below_q9": true, + "T15_interval_directions": true, + "T15_margins_exact": true, + "a1_monotone_in_trials": true, + "capacity_one_tail_q5_exceeds_q9": true, + "e_bounds_consistent_with_tight": true, + "e_bounds_series": true, + "exp_7_3_certificate": true, + "log2_above_2_3": true, + "markov_chain_a_ge_2_and_a_ge_4": true, + "q5_above_25_512_margin": true, + "q5_polynomial_identity": true, + "q9_polynomial_identity": true, + "rho_9_inside_T2": true, + "rho_bip_inside_O12": true, + "s_below_half_from_e_above_8_3": true, + "uniform_even_tail_max_only_at_a2_K4": true + }, + "TRANS_local_transfer": { + "decreasing_event_affine_nonneg_coefficients": true, + "separate_concavity_chord_decimal60": true + } + }, + "passed": true, + "scientific_effect": "NONE", + "scope": "exact identities, brute-force colouring oracle and exact product-measure inequalities on finite instances; one 60-digit decimal check; the continuum arguments are in REVIEW.md" +} diff --git a/reviews/p15_overlap_tail_claude_20260928/REVIEW.md b/reviews/p15_overlap_tail_claude_20260928/REVIEW.md new file mode 100644 index 000000000..29ec33677 --- /dev/null +++ b/reviews/p15_overlap_tail_claude_20260928/REVIEW.md @@ -0,0 +1,240 @@ +# Nonauthor analytic review: P15 overlapping blocks (Math-#118) and sharp even tail with weighted loads (Math-#122) + +Scientific effect: **NONE**. This file does not change `lemma_closed`, prizes, premises, `STATUS`, +`PROOF_INDEX`, `GRAPH` or any author source. It records verdicts on two author-side P15 candidates and one +reviewer remark (R1). Integration is a separate act. + +## Objects + +| Field | Value | +|---|---| +| #118 object | OA-P15-BIPARTITE-OVERLAP-20260928-v1 and OA-P15-EVEN-READ-TWO-20260928-v1 (OpenAI / ChatGPT) | +| #118 head | `chatgpt/p15-overlap-20260928` / `23b7558943f69a7f479251566b19ba58e75cfc26` ([Math-#118](https://github.com/d6g8k5htny-coder/Math-/pull/118)) | +| #118 `PROOF.md` | Git blob `8ad826ecb374cc733e3a547bdba0ba63cad10c08`, 13835 B, SHA256 `21ce7a29ac0971919c0602f556f1aeba48bb14fffd4193864b3f482185bc1698` | +| #118 `EVEN_CAPACITY_EXTENSION.md` | Git blob `ce21e424433100d0307c49bc15cccc748f9438fc`, 7620 B, SHA256 `d28aa700ba83ca139b7b29b6ff06cc39c725470b710af10728867ec10c8ca985` | +| #122 object | OA-P15-TAIL-LOAD-20260928-v1 (OpenAI / ChatGPT) | +| #122 head | `chatgpt/p15-tail-load-20260928` / `245f3d77c9d38f49d13affb9563a266eba92a47b` ([Math-#122](https://github.com/d6g8k5htny-coder/Math-/pull/122)) | +| #122 `PROOF.md` | Git blob `8187908dfd220cb833b94f82c451ef4c0e45e367`, 12828 B, SHA256 `fbca462d4988a06754ded9415ceea6bb1385be5535656d643bdd48edbbee8a20` | +| Requests | [#118 comment 5878164407](https://github.com/d6g8k5htny-coder/Math-/pull/118#issuecomment-5878164407), [#122 comment 5879215663](https://github.com/d6g8k5htny-coder/Math-/pull/122#issuecomment-5879215663) | +| Prior review | OpenAI same-provider review of #118, [5344833684](https://github.com/d6g8k5htny-coder/Math-/pull/118#pullrequestreview-5344833684): no blocker. #122 is its additive follow-up. | + +## Provenance + +| Field | Value | +|---|---| +| Reviewer | Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3` | +| Relation | Different provider from the OpenAI author. Same GitHub account as every lane, so no organizational independence is claimed. | +| Exposure | I read all three proof files in full, both READMEs, RECONNAISSANCE and SOURCE_MAP files, and the OpenAI review above. I did not write or earlier review `frontiers/full_price_20260924/PROOF.md` or any P15 source. | +| Author code | Replayed from `git archive` of each head: #118 `run_validation.py` passes 29 tests and rejects 10 mutants per mode, with identical output pairs. #122 `verify.py --output ` passes 15 tests and rejects 7 mutants per mode, with 8 identical pairs. | +| Independent checks | `p15_exact_check.py` is my own suite. Its colouring oracle is a plain backtracking search over colour assignments of the original coordinates, not the authors' constructions. It covers 34 checks and 7 mutants. Finite checks do not prove the continuum steps argued below. | + +## Verdicts + +### Math-#118 + +| Interface | Verdict | +|---|---| +| (O1)–(O2) Theorem O1: exact colouring on bipartite overlap with arbitrary capacities | **ACCEPT** | +| (O3)–(O4) Corollary O2: active full blocks form a cover, and their inclusion-minimal distinct members are exactly the minimal `K`-obstructions (an active block containing another is not minimal; see §2); `χ_D(X) = K+1` | **ACCEPT** | +| (O5) separate-concavity price-to-hazard transfer | **ACCEPT** | +| (O6)–(O7) Lemma O3: uniform tail `<= q_5` for all `a >= 1` | **ACCEPT** | +| (O8)–(O10) two-sided Cauchy–Schwarz and sum | **ACCEPT** | +| **Theorem O4 (O11)**: `ρ_bip < 3/4` | **ACCEPT** | +| (O12) enclosure and §7 rational certificate | **ACCEPT**. My rigorous enclosure has width about `3·10^-47` and lies inside (O12). | +| §8 doubled triangle and overlap counterexamples | **ACCEPT**. Both were reproduced by the oracle and by exact measure. | +| Even extension (E1)–(E2) Theorem E1: read-two, even capacities, nonbipartite | **ACCEPT** | +| (E3) Lemma E2: read-`q` entropy inequality, direction | **ACCEPT** | +| (E5)–(E6) `2/log(512/25) < 2/3` | **ACCEPT** | + +### Math-#122 + +| Interface | Verdict | +|---|---| +| (T5)–(T6) cover eligibility in the even/read-two class | **ACCEPT** (same argument as E1) | +| (T7)–(T8) local transfer | **ACCEPT** | +| (T9)–(T11) weighted entropy with actual coordinate loads (sum, not max) | **ACCEPT** | +| **Theorem 2 (T3)–(T4)** instance-adaptive load, once a genuine cover is proved | **ACCEPT** | +| (T12)–(T13) sharp reference maximum `q_9`, attained only at `a=2, K=4` | **ACCEPT** | +| (T14)–(T16) interval directions and margins; `ρ_9 < 1/2` | **ACCEPT** | +| **Theorem 1 (T1)** and (T2) enclosure | **ACCEPT**. My rigorous enclosure (width about `10^-48`) lies inside (T2). | +| Zero or infinite `H_D`; duplicate and superset removal; the active/inactive distinction | **ACCEPT** | + +No defect was found in either PR. Remark R1 below slightly extends #122's factor to the bipartite class of #118. + +--- + +## §1 — Colouring: (O2), (E2), (T5) + +**Bipartite, arbitrary capacities.** Each original coordinate of `U` becomes exactly one edge: shared coordinates +join the left and right blocks, and private ones join a private degree-one vertex. So the degree of block `i` is +exactly `|U ∩ X_i|`. Splitting `i` into `a_i` vertices gives degree `<= ⌈|U ∩ X_i|/a_i⌉ <= k`. König's theorem, +proved in the source by regularization and Hall, gives `k` colours. Each split vertex sees at most one edge of a +colour, so each colour meets `X_i` in at most `a_i` coordinates. The source's regularization is sound: the total +deficits of the two sides are equal, so a positive deficit on one side always has a partner on the other. + +**Read-two, even capacities.** Split `i` into `a_i/2` vertices, so each split degree is `<= 2k`. Pair the odd +vertices; their degrees were `<= 2k-1`. Then take an Euler orientation, so in- and out-degree are both `<= k`, and +apply König to the out/in double. Each colour has at most one out-edge and one in-edge per split vertex. That means +at most `2 · (a_i/2) = a_i` per block, because no edge is a loop. + +**Oracle checks.** The formula matches the backtracking oracle on: + +- 720 random subsets of 120 random bipartite systems with capacities 1–3; +- 320 random subsets of 80 random read-two systems whose incidence graph is an odd cycle (3 or 5) with capacities + 2 or 4; +- the E4 triangle: capacity 2, blocks of 9, the 12 shared coordinates need 4 colours and all 15 need 5. + +**Adversarial cases requested by the owner.** + +- *Doubled triangle, capacity one.* The oracle gives `χ = 6` while the formula gives 4, and no block lies inside `U`. + This confirms that §8 excludes it correctly, and that neither class covers it: it is not bipartite, and its + capacities are odd. +- *Odd capacities on odd cycles in general.* The `odd-nonbipartite` mutant sets capacity one on the random + odd-cycle systems, and the formula then fails. The evenness in (E1) and (T5) is genuinely needed, not a proof + convenience. + +## §2 — Obstruction and cover: (O4), (T6), inactive blocks, duplicates + +For an inactive block (`d_i < K`), `|X_i| = a_i d_i + 1 <= a_i K`, so it can never exceed the palette. For an active +block, exceeding `a_i K` means containing all of `X_i`. + +Brute force over all `2^10` subsets of a bipartite system confirms `O_4(D) = {U ⊇ X_0} ∪ {U ⊇ X_2}` and +`χ_D(X) = 5`. The system has two active capacity-one blocks and an **inactive demand-one block** `{4,5}` that meets +both. The inactive block's full set has `χ = 2 <= K`, so it is not an obstruction. The `charge-inactive` mutant, +which adds it to the obstruction family, fails. + +Brute force also confirms two removal rules: + +- dropping a duplicate block (`X_0 = X_1`) keeps the cover; +- keeping only the smaller of `X_0 ⊊ X_1` (capacities 1 and 2, both active) keeps the cover. + +The `drop-superset-cover` mutant keeps the superset instead, and fails on `U = X_0`. + +## §3 — Local transfer: (O5), (T7)–(T8) + +With the other coordinates fixed, a decreasing event has `μ(A) = P_1 + (P_0 - P_1)(1 - p_v)` with `P_0 >= P_1 >= 0`. +This was checked exactly on 120 random decreasing events. So `F(t) = -log(A_0 + B_0 e^{-t_v})` has +`∂²F = -A_0B_0e^{-t}/(·)^2 <= 0`. `F >= 0` gives the chord bound `F(t) >= t_v F(t_v = 1)`, and iterating gives +`F(t) >= H_A Π t_v`. + +Replacing `p_v` by `1 - e^{-φ(p_v)} <= p_v` only increases the probability of a decreasing event, so the direction +is right. The chord bound was also checked on 60 random capacity events in 60-digit decimal arithmetic. That check +is labelled numerical; it is not exact. + +The transfer is applied to the capacity event `A_i = {|U ∩ X_i| <= a_i}`, with reference hazard `H_i`. It is **not** +applied to the containment event. Both sources say this explicitly. + +## §4 — Hazard aggregation: (O8)–(O9), (E3), (T9)–(T11) + +- **Two-sided Cauchy–Schwarz.** `D ⊆ A_L ∩ A_R`, and `P(A ∩ B)^2 <= P(A)P(B)`. Same-side independence holds only + because same-side blocks are disjoint. Exact checks on 150 random rational product measures confirm the + factorization and `μ(D)^2 <= Π μ(A_i)`. The source's overlap example, `5/8 > 9/16` with `(5/8)^2 <= (3/4)^2`, is + reproduced exactly. +- **Entropy (E3)/(T11).** `KL(ν||μ) = H_D` for `ν = μ(·|D)`. Support gives `KL(ν_S||μ_S) >= h_i`. The chain rule + with a product `μ`, plus Jensen for KL's first argument, bounds each marginal contribution by the full conditional + one `b_v`. Summing with weights gives `Σ w_i h_i <= (max_v Σ_{i∋v} w_i) H_D`. The inequality directions are + correct. +- **Exact exponentiated checks.** `Π μ(A_i) >= μ(D)^q` held on 150 random product measures with **arbitrary** + (non-monotone) events on read-2 and read-3 incidences. So did `Π μ(A_i)^{n_i} >= μ(D)^{max_v Σ n_i}`. The `q-one` + mutant (independence-style `q = 1`) fails. The `max-load` mutant fails on the source's counterexample: two copies + of one fair-coin event, where equality `1/4 = 1/4` holds only with the summed load 2. + +## §5 — Reference tails: (O6)–(O7), (E5), (T12)–(T16) + +All rational certificates were recomputed exactly: + +- `1957/720 < e < 31967/11760 < 87/32 < 11/4`; +- `s = (e+4)/(5e) < 1/2` from `e > 8/3`, with equality exactly at `8/3`; +- `5^a 2^{-(4a+1)} = (1/2)(5/16)^a`, and the chains `<= 25/512` for `a >= 2` and `<= 625/131072` for `a >= 4`; +- `q_5 > (28/3)(4/11)^5`, with the margin `2601239/247374336`; +- `Σ_{j<=6}(7/3)^j/j! - 307/32 = 129055/209952`; +- `512/25 - (87/32)^3 = 314641/819200`; +- the `q_5` and `q_9` identities as polynomial identities in `e`; +- both (T15) margins, digit for digit. + +**Interval directions (T15).** `P(z) = 36z^2 - 63z + 28` increases on `[l,u]`, so `P(l)/u^9 < q_9 < P(u)/l^9`. Both +published bounds bracket a rigorous 40-term enclosure of `q_9`. The `interval-swap` mutant fails. + +**Enclosures.** I built independent rigorous enclosures of `ρ_bip` and `ρ_9`. `e` comes from the series with the +`1/(N!N)` tail. The log uses binary reduction and the atanh series with its remainder, after outward rounding. The +enclosures have widths of about `3·10^-47` and `10^-48` and lie strictly inside (O12) and (T2). + +**Sharpness of the even tail (T13).** Rigorous bounds with `p_* ∈ (1 - 1/e_lo, 1 - 1/e_hi)` show +`P(Bin(aK+1, p_*) <= a) < q_9` for every even `a <= 10`, `4 <= K <= 8`, except `(a, K) = (2, 4)`. The general proof +is the source's: monotonicity in `n` for `a = 2`, and Markov for `a >= 4`. + +Capacity one gives `q_5 > q_9`, so the uniform `q_9` reference bound does not reach active capacity-one blocks. In +this coarse read-two assembly they need the `h_5` local reference input instead. That is a failure of a +reference-tail bound, **not** a cover-factor impossibility. For example, a single active capacity-one block is +read-one, so its load is `1/h_5 = ρ_bip/2 < 0.36508 < ρ_9` by the enclosures (O12) and (T2). + +### R1 (reviewer remark, not a source claim): the `q_9` reference tail covers every capacity `>= 2`, odd included + +In the **bipartite** class of #118, which allows arbitrary capacities, suppose every **active** block has +`a_i >= 2`. Then: + + covercost_c(O_K(D)) <= min(1, ρ_9 H_D), ρ_9 < 1/2. + +Inactive capacity-one blocks are allowed. + +*Proof.* (O4), (O5) and (O9) are unchanged. It remains to show `H_i >= -log q_9` for every `a_i >= 2` and `K >= 4`: + +- `a = 2`: monotonicity in `n`. +- `a >= 4` of either parity: Markov gives `(1/2)(5/16)^a <= 625/131072`. +- `a = 3`: this case needs a separate step. **Markov's bound `125/8192` exceeds `q_9`**. But `n = 3K+1 >= 13`, and + monotonicity in `n` gives `P(Bin(3K+1, p_*) <= 3) <= P(Bin(13, p_*) <= 3) ≈ 0.00385 < q_9 ≈ 0.01515`. That last + inequality is certified exactly by `P(Bin(13, 1 - 1/e_lo) <= 3) < P(Bin(9, 1 - 1/e_hi) <= 2)` with 40-term + bounds `e_lo < e < e_hi`. + +The `tail-a3` mutant, which replaces the direct tail by Markov, fails. ∎ + +So in this coarse read-two assembly, only **active capacity-one** blocks need the `h_5` reference input, which +yields the uniform factor `ρ_bip`. No necessity or optimality of `ρ_bip` as a cover factor is claimed. When +capacity-one blocks sit alongside larger ones, #122's Theorem 2 already gives the instance-specific load: a +coordinate shared by a capacity-one and a capacity-`>=2` active block carries `1/h_5 + 1/(-log q_9)`. R1 is offered +to the author and changes no source. + +## §6 — #122 Theorem 2 edge cases + +- **Cover eligibility.** Theorem 2 presupposes a genuine cover and `H_i > 0`. `H_i > 0` holds exactly when + `|X_i| > a_i`, which is automatic for active blocks. +- **`H_D = ∞`.** The unit-price empty generator applies. +- **`H_D = 0`.** Then `μ(A_i) = 1`. That forces at least `|X_i| - a_i >= 1` coordinates with `p_v = 0`, hence + `c_v = 0`, so the full-block price is zero, consistent with (T8). +- **Loads.** Loads are per original coordinate, summed. Duplicate removal halves a doubled load, and the cover is + unchanged (§2). + +## Checks run + +``` +python3 -B -S run_validation.py # #118 author runner at 23b7558 (git archive): 29 tests, 10 mutants +python3 -B -S verify.py --output # #122 author runner at 245f3d7 (git archive): 15 tests, 7 mutants +python3 -B -S p15_exact_check.py # rc 0, stdout == RESULTS.json +python3 -B -O -S p15_exact_check.py # rc 0, byte-identical +python3 -B -S p15_exact_check.py --mutant M # rc 1 for each of: + odd-nonbipartite charge-inactive q-one max-load interval-swap tail-a3 drop-superset-cover +``` + +Python standard library only. The workflow `.github/workflows/p15-overlap-tail-review.yml` verifies the packet tree +against `SOURCE_FILES.json`, replays both modes and requires every mutant to be rejected. + +## Not established here + +- Optimality of any cover factor. Both sources disclaim it; the tail in (T13) is sharp as a reference tail only. +- Arbitrary macro-clutters, arbitrary read-two with odd capacities, unrestricted downsets, or any governing P15 + status. +- The old `0.84548` sharp factor of `full_price_20260924` is a different class (maximal demand two, disjoint + blocks). No comparison is asserted. +- Organizational independence: all lanes share one GitHub account. + +## Revision history + +- **v1**, reviewing #118 at `23b7558` and #122 at `245f3d7`: initial packet. +- **v2**, responding to the OpenAI review + [5345318332](https://github.com/d6g8k5htny-coder/Math-/pull/123#pullrequestreview-5345318332). Wording only; + no verdict, check or source changes. + - The (O3)–(O4) row now says the inclusion-minimal distinct active full blocks are the minimal obstructions, as + the source does. The reviewer's `X_0 ⊂ X_1` example is the §2 superset case. + - §5 and R1 no longer say `ρ_9` "cannot cover" active capacity-one blocks or that `ρ_bip` is "forced". A failed + reference-tail bound is not a cover-factor impossibility; a single active capacity-one block has load + `1/h_5 < ρ_9`. diff --git a/reviews/p15_overlap_tail_claude_20260928/SOURCE_FILES.json b/reviews/p15_overlap_tail_claude_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..eab24e711 --- /dev/null +++ b/reviews/p15_overlap_tail_claude_20260928/SOURCE_FILES.json @@ -0,0 +1,57 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_objects": [ + { + "pr": "d6g8k5htny-coder/Math-#118", + "head": "23b7558943f69a7f479251566b19ba58e75cfc26", + "paths": [ + { + "path": "frontiers/p15_bipartite_overlap_20260928/PROOF.md", + "git_blob": "8ad826ecb374cc733e3a547bdba0ba63cad10c08", + "bytes": 13835, + "sha256": "21ce7a29ac0971919c0602f556f1aeba48bb14fffd4193864b3f482185bc1698" + }, + { + "path": "frontiers/p15_bipartite_overlap_20260928/EVEN_CAPACITY_EXTENSION.md", + "git_blob": "ce21e424433100d0307c49bc15cccc748f9438fc", + "bytes": 7620, + "sha256": "d28aa700ba83ca139b7b29b6ff06cc39c725470b710af10728867ec10c8ca985" + } + ] + }, + { + "pr": "d6g8k5htny-coder/Math-#122", + "head": "245f3d77c9d38f49d13affb9563a266eba92a47b", + "paths": [ + { + "path": "frontiers/p15_tail_load_20260928/PROOF.md", + "git_blob": "8187908dfd220cb833b94f82c451ef4c0e45e367", + "bytes": 12828, + "sha256": "fbca462d4988a06754ded9415ceea6bb1385be5535656d643bdd48edbbee8a20" + } + ] + } + ], + "files": [ + { + "path": "REVIEW.md", + "bytes": 15923, + "sha256": "7a425f7119dd8a0701fb241769a3e82d80fbd6b148d074f11e1015e826813268", + "git_blob": "29ec33677854661964f2e659e7c9116a5749e95c" + }, + { + "path": "p15_exact_check.py", + "bytes": 20898, + "sha256": "1c865eaca5b7e4fc815f1f050695dc5ed1acb0edbebb73824e93124916779540", + "git_blob": "378aa17fb47738d047fd6e4913670f9c8f07e583" + }, + { + "path": "RESULTS.json", + "bytes": 2001, + "sha256": "87b52587cbed09cb893086c2db2d73992da8e0c940ffa156a56cd053361491d5", + "git_blob": "60cec87c3cd25cd9400a8cc1df3427bbf2b7b0df" + } + ] +} diff --git a/reviews/p15_overlap_tail_claude_20260928/p15_exact_check.py b/reviews/p15_overlap_tail_claude_20260928/p15_exact_check.py new file mode 100644 index 000000000..378aa17fb --- /dev/null +++ b/reviews/p15_overlap_tail_claude_20260928/p15_exact_check.py @@ -0,0 +1,461 @@ +"""Independent exact checks for the nonauthor review of Math-#118 (P15 bipartite overlap and even-capacity +extension) and Math-#122 (P15 sharp even reference tail and weighted loads). + +Python standard library only; exact rational arithmetic (one group uses 60-digit decimal arithmetic and says so). +Written after reading the authors' suites, but it shares no code with them. Its colouring oracle is a plain +backtracking search over colour assignments of ORIGINAL coordinates, not the authors' constructions. Groups: + + COL (O2)/(E2)/(T5) chi_D = max ceil(|U^X_i|/a_i) against the oracle: random bipartite systems with arbitrary + capacities, random read-two NONbipartite systems with even capacities, the E4 triangle (12 shared + coordinates 4-colourable, all 15 need 5), and the excluded doubled triangle with capacity one (chi = 6 > 4). + OBS (O4)/(T6) O_K(D) = union of active full-block containments, by brute force over all subsets, with an inactive + demand-one block; chi_D(X) = K+1; duplicate and strict-superset generator removal keeps a cover. + HAZ (O8)-(O9), (E3), (T11) in exponentiated exact form on random rational product measures: two-sided + Cauchy-Schwarz, read-q product inequality for arbitrary events, integer-weighted loads; the overlap + example 5/8 > 9/16; the max-instead-of-sum counterexample. + TRANS (O5)/(T8) decreasing events are affine in each p_v with nonnegative coefficients; separate concavity + chord bound checked in 60-digit decimal arithmetic (not exact). + TAIL (O6)-(O7), (E5), (T12)-(T16): rational e bounds, s < 1/2, Markov chains, q_5 > 25/512, the exp(7/3) + certificate, 512/25 > (87/32)^3, the q_9 polynomial identity, both (T15) margins, rigorous enclosures of + rho_bip and rho_9 inside (O12)/(T2), the uniform even tail with equality only at a=2, K=4, capacity one + giving q_5 > q_9, and reviewer remark R1: every capacity a >= 2 (odd included) has tail < q_9, where + a = 3 needs a direct tail because Markov's bound 125/8192 exceeds q_9. + +Not a proof of the continuum inequalities: separate concavity, the relative-entropy chain rule and König's +theorem are argued in REVIEW.md. +""" +import argparse +import decimal +import itertools +import json +import random +import sys +from fractions import Fraction as F +from math import comb, factorial + +MUTANTS = ("odd-nonbipartite", "charge-inactive", "q-one", "max-load", "interval-swap", "tail-a3", + "drop-superset-cover") + +# ---------------------------------------------------------------------------------------------------------- +# Colouring +# ---------------------------------------------------------------------------------------------------------- + + +def formula(U, blocks, caps): + return max([0] + [-(-len(U & B) // a) for B, a in zip(blocks, caps)]) + + +def chi_oracle(U, blocks, caps): + """Least k such that U splits into k sets each meeting every block X_i in <= a_i coordinates.""" + U = sorted(U) + if not U: + return 0 + memb = {v: [i for i, B in enumerate(blocks) if v in B] for v in U} + U.sort(key=lambda v: -len(memb[v])) + lower = max(-(-sum(1 for v in U if i in memb[v]) // a) for i, a in enumerate(caps)) # counting bound + for k in range(max(1, lower), len(U) + 1): + load = [[0] * len(blocks) for _ in range(k)] + + def bt(idx, used): + if idx == len(U): + return True + v = U[idx] + for c in range(min(used + 1, k)): + if all(load[c][i] < caps[i] for i in memb[v]): + for i in memb[v]: + load[c][i] += 1 + if bt(idx + 1, max(used, c + 1)): + return True + for i in memb[v]: + load[c][i] -= 1 + return False + + if bt(0, 0): + return k + raise AssertionError("unreachable") + + +def random_bipartite(rng): + n = rng.randrange(5, 10) + nl, nr = rng.randrange(1, 4), rng.randrange(1, 4) + L = [set() for _ in range(nl)] + R = [set() for _ in range(nr)] + for v in range(n): + side = rng.randrange(3) + if side in (0, 2): + L[rng.randrange(nl)].add(v) + if side in (1, 2): + R[rng.randrange(nr)].add(v) + blocks = [B for B in L + R if B] + caps = [rng.randrange(1, 4) for _ in blocks] + return n, blocks, caps + + +def random_read_two(rng, cyc): + """Blocks are the vertices of an odd cycle; coordinates are cycle edges (shared) or private.""" + blocks = [set() for _ in range(cyc)] + v = 0 + for i in range(cyc): + for _ in range(rng.randrange(1, 3)): + blocks[i].add(v) + blocks[(i + 1) % cyc].add(v) + v += 1 + for _ in range(rng.randrange(0, 2)): + blocks[i].add(v) + v += 1 + return v, blocks + + +def check_col(mut): + rng = random.Random(118) + out = {} + ok_bip, ok_even = True, True + for _ in range(120): + n, blocks, caps = random_bipartite(rng) + for _ in range(6): + U = {x for x in range(n) if rng.random() < 0.7} + ok_bip &= chi_oracle(U, blocks, caps) == formula(U, blocks, caps) + for _ in range(80): + n, blocks = random_read_two(rng, rng.choice((3, 5))) + caps = [1 if mut == "odd-nonbipartite" else rng.choice((2, 4)) for _ in blocks] + for _ in range(4): + U = {x for x in range(n) if rng.random() < 0.8} + ok_even &= chi_oracle(U, blocks, caps) == formula(U, blocks, caps) + out["bipartite_arbitrary_capacity_formula_equals_oracle"] = ok_bip + out["read_two_nonbipartite_even_capacity_formula_equals_oracle"] = ok_even + # E4 triangle: capacity 2, four shared coordinates per side, one private per block. + blocks = [set(), set(), set()] + v = 0 + for i in range(3): + for _ in range(4): + blocks[i].add(v) + blocks[(i + 1) % 3].add(v) + v += 1 + shared = set(range(v)) + for i in range(3): + blocks[i].add(v) + v += 1 + full = set(range(v)) + caps = [2, 2, 2] + out["E4_triangle_shared_4_full_5"] = (all(len(B) == 9 for B in blocks) and chi_oracle(shared, blocks, caps) == 4 + and chi_oracle(full, blocks, caps) == 5) + # Excluded doubled triangle, capacity one (PROOF.md section 8). + blocks = [{0, 1, 4, 5, 6}, {0, 1, 2, 3, 7}, {2, 3, 4, 5, 8}] + U = {0, 1, 2, 3, 4, 5} + out["doubled_triangle_capacity_one_chi_6_formula_4"] = (chi_oracle(U, blocks, [1, 1, 1]) == 6 + and formula(U, blocks, [1, 1, 1]) == 4 + and not any(B <= U for B in blocks)) + return out + + +def check_obs(mut): + out = {} + # Bipartite: X0 (a=1, d=4, active), X1={4,5} (a=1, d=1, inactive, overlaps both), X2 (a=1, d=4, active). + blocks = [set(range(0, 5)), {4, 5}, set(range(5, 10))] + caps, d = [1, 1, 1], [4, 1, 4] + K = max(d) + X = set(range(10)) + active = [B for B, di in zip(blocks, d) if di == K] + charged = blocks if mut == "charge-inactive" else active + ok = all(len(B) == a * di + 1 for B, a, di in zip(blocks, caps, d)) + for bits in range(1 << 10): + U = {v for v in range(10) if bits >> v & 1} + obstruct = chi_oracle(U, blocks, caps) > K + ok &= obstruct == any(B <= U for B in active) + if mut == "charge-inactive": + ok &= obstruct == any(B <= U for B in charged) + out["O4_exact_obstruction_equals_active_full_blocks"] = ok + out["chi_whole_ground_K_plus_1"] = chi_oracle(X, blocks, caps) == K + 1 + out["inactive_full_block_not_obstruction"] = chi_oracle(blocks[1], blocks, caps) == 2 <= K + # Duplicate removal (X0 = X1, read-two, bipartite) and strict-superset removal (X0 inside X1, a = 1 and 2). + ok = True + for blocks, caps, keep, drop in (([set(range(5)), set(range(5)), set(range(5, 10))], [1, 1, 1], [0, 2], [1, 2]), + ([set(range(5)), set(range(9))], [1, 2], [0], [1])): + ok &= all(len(B) == a * 4 + 1 for B, a in zip(blocks, caps)) + n = len(set().union(*blocks)) + retained = [blocks[i] for i in (drop if mut == "drop-superset-cover" and len(blocks) == 2 else keep)] + for bits in range(1 << n): + U = {v for v in range(n) if bits >> v & 1} + ok &= (chi_oracle(U, blocks, caps) > 4) == any(B <= U for B in retained) + out["duplicate_and_superset_removal_keeps_cover"] = ok + return out + + +# ---------------------------------------------------------------------------------------------------------- +# Product-measure hazards +# ---------------------------------------------------------------------------------------------------------- + + +def configs(n): + return [tuple(bits >> v & 1 for v in range(n)) for bits in range(1 << n)] + + +def measure(p, event, n): + tot = F(0) + for x in configs(n): + if event(x): + w = F(1) + for v in range(n): + w *= p[v] if x[v] else 1 - p[v] + tot += w + return tot + + +def check_haz(mut): + rng = random.Random(1181) + out = {} + # Overlap destroys independence; Cauchy-Schwarz survives. + p = [F(1, 2)] * 3 + a1 = measure(p, lambda x: x[0] + x[1] <= 1, 3) + a2 = measure(p, lambda x: x[1] + x[2] <= 1, 3) + dd = measure(p, lambda x: x[0] + x[1] <= 1 and x[1] + x[2] <= 1, 3) + out["overlap_5_8_exceeds_9_16_and_CS"] = a1 == a2 == F(3, 4) and dd == F(5, 8) > a1 * a2 and dd ** 2 <= a1 * a2 + ok_cs, ok_rq, ok_w = True, True, True + for trial in range(150): + n = rng.randrange(4, 7) + p = [F(rng.randrange(0, 11), 10) for _ in range(n)] + # Bipartite capacity system: two disjoint left blocks, two disjoint right blocks. + perm = list(range(n)) + rng.shuffle(perm) + cut = rng.randrange(1, n) + L = [set(perm[:cut]), set(perm[cut:])] + rng.shuffle(perm) + cut = rng.randrange(1, n) + R = [set(perm[:cut]), set(perm[cut:])] + blocks = L + R + caps = [rng.randrange(0, 3) for _ in blocks] + ev = [lambda x, B=B, a=a: sum(x[v] for v in B) <= a for B, a in zip(blocks, caps)] + mus = [measure(p, e, n) for e in ev] + muL = measure(p, lambda x: ev[0](x) and ev[1](x), n) + muR = measure(p, lambda x: ev[2](x) and ev[3](x), n) + muD = measure(p, lambda x: all(e(x) for e in ev), n) + ok_cs &= muL == mus[0] * mus[1] and muR == mus[2] * mus[3] and muD ** 2 <= muL * muR + ok_cs &= muD ** 2 <= mus[0] * mus[1] * mus[2] * mus[3] + # Read-q with ARBITRARY events on triangle incidence (q = 2): Prod mu(A_i) >= mu(D)^q. + S = [(0, 1), (1, 2), (2, 0)] + ([(3, 0)] if n > 3 else []) + q = max(sum(1 for s in S if v in s) for v in range(n)) + tables = [{xy: rng.random() < 0.75 for xy in itertools.product((0, 1), repeat=2)} for _ in S] + evs = [lambda x, s=s, t=t: t[(x[s[0]], x[s[1]])] for s, t in zip(S, tables)] + muA = [measure(p, e, n) for e in evs] + muD = measure(p, lambda x: all(e(x) for e in evs), n) + qq = 1 if mut == "q-one" else q + prod = F(1) + for m in muA: + prod *= m + ok_rq &= prod >= muD ** qq + # Integer-weighted loads (T11): Prod mu(A_i)^{n_i} >= mu(D)^{max_v sum_{i ni v} n_i}. + wts = [rng.randrange(0, 4) for _ in S] + if mut == "max-load": + load = max(max([w for s, w in zip(S, wts) if v in s], default=0) for v in range(n)) + else: + load = max(sum(w for s, w in zip(S, wts) if v in s) for v in range(n)) + prod = F(1) + for m, w in zip(muA, wts): + prod *= m ** w + ok_w &= prod >= muD ** load + # Max-instead-of-sum counterexample: two identical events on one fair coordinate. + mA = measure([F(1, 2)], lambda x: x[0] == 0, 1) + load = 1 if mut == "max-load" else 2 + ok_w &= mA * mA >= mA ** load + out["two_sided_cauchy_schwarz_bipartite"] = ok_cs + out["read_q_product_inequality_arbitrary_events"] = ok_rq + out["weighted_load_sum_not_max"] = ok_w + return out + + +def check_trans(mut): + rng = random.Random(1182) + out = {} + ok_aff = True + for _ in range(120): + n = rng.randrange(2, 6) + gens = [frozenset(v for v in range(n) if rng.random() < 0.5) for _ in range(3)] + # decreasing event: the configuration contains no nonempty generator + down = lambda x, gens=gens: not any(g and all(x[v] for v in g) for g in gens) + p = [F(rng.randrange(0, 11), 10) for _ in range(n)] + j = rng.randrange(n) + vals = [] + for pj in (F(0), F(1, 3), F(1)): + pp = list(p) + pp[j] = pj + vals.append(measure(pp, down, n)) + P0, P1 = vals[0], vals[2] # coordinate j forced absent / present + ok_aff &= P0 >= P1 >= 0 and vals[1] == P1 + (P0 - P1) * (1 - F(1, 3)) + out["decreasing_event_affine_nonneg_coefficients"] = ok_aff + # Separate-concavity chord bound F(t) >= H prod t, 60-digit decimal (numerical, not exact). + ctx = decimal.Context(prec=60) + D = decimal.Decimal + ok = True + for _ in range(60): + n = rng.randrange(2, 5) + a = rng.randrange(0, n) + t = [D(rng.randrange(1, 101)) / D(100) for _ in range(n)] + pt = [1 - ctx.exp(-x) for x in t] + p1 = 1 - ctx.exp(D(-1)) + + def mu(pv): + tot = D(0) + for x in configs(n): + if sum(x) <= a: + w = D(1) + for v in range(n): + w *= pv[v] if x[v] else 1 - pv[v] + tot += w + return tot + + Ft = -ctx.ln(mu(pt)) + H = -ctx.ln(mu([p1] * n)) + prod = D(1) + for x in t: + prod *= x + ok &= Ft >= H * prod - D(10) ** -50 + out["separate_concavity_chord_decimal60"] = ok + return out + + +# ---------------------------------------------------------------------------------------------------------- +# Reference tails and certificates +# ---------------------------------------------------------------------------------------------------------- + + +def e_bounds(N): + s = sum(F(1, factorial(j)) for j in range(N + 1)) + return s, s + F(1, factorial(N) * N) + + +def round_out(x, down): + den = 10 ** 45 + num = (x.numerator * den) // x.denominator + return F(num if down else num + 1, den) + + +def log_enclosure(x, m=60): + """Rigorous [lo, hi] for log x, rational x >= 1, via x = 2^j y and the atanh series with remainder.""" + assert x >= 1 + j = 0 + while x >= 2: + x /= 2 + j += 1 + + def atanh2(y): + t = (y - 1) / (y + 1) + s = 2 * sum(t ** (2 * k + 1) / (2 * k + 1) for k in range(m)) + return s, s + 2 * t ** (2 * m + 1) / ((2 * m + 1) * (1 - t * t)) + + l2lo, l2hi = atanh2(F(2)) + ylo, yhi = atanh2(x) + return j * l2lo + ylo, j * l2hi + yhi + + +def binom_le(n, p, a): + return sum(comb(n, i) * p ** i * (1 - p) ** (n - i) for i in range(a + 1)) + + +def check_tail(mut): + out = {} + l, u = F(1957, 720), F(87, 32) + eu6 = l + F(1, factorial(7)) * F(8, 7) + out["e_bounds_series"] = (l == sum(F(1, factorial(j)) for j in range(7)) and eu6 == F(31967, 11760) + and F(8, 3) < l < eu6 < u < F(11, 4)) + el, eh = e_bounds(40) + out["e_bounds_consistent_with_tight"] = l < el < eh < F(31967, 11760) + s_at = lambda e: (e + 4) / (5 * e) + out["s_below_half_from_e_above_8_3"] = s_at(F(8, 3)) == F(1, 2) and s_at(eh) < F(1, 2) + out["markov_chain_a_ge_2_and_a_ge_4"] = (all(F(1, 2) * F(5, 16) ** a <= F(25, 512) for a in range(2, 60)) + and all(F(1, 2) * F(5, 16) ** a <= F(625, 131072) + for a in range(4, 60, 2)) + and all(5 ** a * F(1, 2) ** (4 * a + 1) == F(1, 2) * F(5, 16) ** a + for a in range(1, 30))) + q5lo = F(28, 3) * F(4, 11) ** 5 + out["q5_above_25_512_margin"] = q5lo - F(25, 512) == F(2601239, 247374336) > 0 + out["exp_7_3_certificate"] = (sum(F(7, 3) ** j / factorial(j) for j in range(7)) - F(307, 32) + == F(129055, 209952) and 5 * u - 4 == F(307, 32)) + out["512_25_exceeds_87_32_cubed"] = F(512, 25) - u ** 3 == F(314641, 819200) + # q_9 identity as a polynomial identity in e (y = 1/e): Bin(9, 1-y) <= 2. + ok = True + for e in (F(5, 2), F(11, 4), F(271, 100), F(3)): + y = 1 / e + lhs = binom_le(9, 1 - y, 2) + ok &= lhs == (36 * e * e - 63 * e + 28) / e ** 9 == y ** 9 * (1 + 9 * (e - 1) + 36 * (e - 1) ** 2) + out["q9_polynomial_identity"] = ok + Pz = lambda z: 36 * z * z - 63 * z + 28 + lo9, hi9 = Pz(l) / u ** 9, Pz(u) / l ** 9 + if mut == "interval-swap": + hi9 = Pz(l) / u ** 9 + tlo, thi = Pz(el) / eh ** 9, Pz(eh) / el ** 9 + out["T15_margins_exact"] = (lo9 - F(625, 131072) == F(87187623163627321174969, 8421039761612032386662400) + and F(1, 64) - Pz(u) / l ** 9 + == F(12311490319341451572976881157, 26946192308072632700222520394048)) + out["T15_interval_directions"] = (72 * l - 63 > 0 and lo9 <= tlo and thi <= hi9 and lo9 < hi9 + and F(625, 131072) < lo9 and hi9 < F(1, 64)) + out["log2_above_2_3"] = F(11, 4) ** 2 < 8 + # Rigorous enclosures of rho_bip and rho_9 lie inside the published ones. + x_lo, x_hi = round_out(5 * el - 4, True), round_out(5 * eh - 4, False) + lg_lo, _ = log_enclosure(x_lo) + _, lg_hi = log_enclosure(x_hi) + rb = (2 / (5 - lg_lo), 2 / (5 - lg_hi)) + P_lo, P_hi = round_out(Pz(el), True), round_out(Pz(eh), False) + lq_lo, _ = log_enclosure(P_lo) + _, lq_hi = log_enclosure(P_hi) + r9 = (2 / (9 - lq_lo), 2 / (9 - lq_hi)) + out["rho_bip_inside_O12"] = (F("0.73015826409534942932") < rb[0] <= rb[1] < F("0.73015826409534942934") + and rb[1] < F(3, 4)) + out["rho_9_inside_T2"] = (F("0.47734798895766998533") < r9[0] <= r9[1] < F("0.47734798895766998534") + and r9[1] < F(1, 2)) + # Uniform even tail (T13): rigorous upper bound on P(Bin(aK+1, p*) <= a) via p* > 1 - 1/el. + p_lo, p_hi = 1 - 1 / el, 1 - 1 / eh + q9_lo = binom_le(9, p_hi, 2) + ok_even = True + for a in range(2, 11, 2): + for K in range(4, 9): + if (a, K) == (2, 4): + continue + ok_even &= binom_le(a * K + 1, p_lo, a) < q9_lo + # Capacity one is NOT covered by q_9 (it gives q_5), which is why rho_9 excludes it. + q5_lo = binom_le(5, p_hi, 1) + q9_hi = binom_le(9, p_lo, 2) + out["uniform_even_tail_max_only_at_a2_K4"] = ok_even + out["capacity_one_tail_q5_exceeds_q9"] = q5_lo > q9_hi + # Reviewer remark R1: every capacity a >= 2, odd included, has reference tail < q_9 for K >= 4. For a = 3 + # Markov's bound (1/2)(5/16)^3 = 125/8192 EXCEEDS q_9, so a direct tail (monotone in n, n >= 13) is needed. + markov_a3 = F(1, 2) * F(5, 16) ** 3 + direct_a3 = markov_a3 if mut == "tail-a3" else binom_le(13, p_lo, 3) + out["R1_a3_markov_insufficient_direct_tail_below_q9"] = markov_a3 > q9_hi and direct_a3 < q9_lo + out["R1_a3_monotone_in_trials"] = all(binom_le(n + 1, p_lo, 3) <= binom_le(n, p_lo, 3) for n in range(13, 40)) + out["R1_odd_a_ge_5_markov_below_q9"] = all(F(1, 2) * F(5, 16) ** a < q9_lo for a in range(5, 61, 2)) + # Five-trial reference: q_5 = e^-5 (5e-4) as a polynomial identity. + ok = True + for e in (F(5, 2), F(11, 4), F(3)): + ok &= binom_le(5, 1 - 1 / e, 1) == (5 * e - 4) / e ** 5 + out["q5_polynomial_identity"] = ok + # a = 1 branch: monotone in n. + out["a1_monotone_in_trials"] = all(binom_le(n + 1, p_lo, 1) <= binom_le(n, p_lo, 1) for n in range(5, 30)) + return out + + +def flatten(d): + for v in d.values(): + if isinstance(v, dict): + yield from flatten(v) + else: + yield v + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + mut = ap.parse_args().mutant + checks = {"COL_colouring": check_col(mut), "OBS_obstruction_cover": check_obs(mut), + "HAZ_product_hazards": check_haz(mut), "TRANS_local_transfer": check_trans(mut), + "TAIL_reference_tails": check_tail(mut)} + passed = all(flatten(checks)) + print(json.dumps({"checks": checks, "passed": passed, "scientific_effect": "NONE", + "scope": "exact identities, brute-force colouring oracle and exact product-measure " + "inequalities on finite instances; one 60-digit decimal check; the continuum " + "arguments are in REVIEW.md"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/reviews/remote_height_claude_20260928/RESULTS.json b/reviews/remote_height_claude_20260928/RESULTS.json new file mode 100644 index 000000000..914ccba4c --- /dev/null +++ b/reviews/remote_height_claude_20260928/RESULTS.json @@ -0,0 +1,53 @@ +{ + "checks": { + "BAR_r2_barrier": { + "exceeds_r3": true, + "mean_exactly_flat": true, + "q_equals_r5": true, + "singleton_tv_r2_over_2_1_minus_r2": true, + "valid_law_r_le_half": true + }, + "CONG_congruence": { + "F_j_H_equals_r_F_j_K": true, + "det_H_equals_r_det_K": true, + "inertia_preserved": true + }, + "FDET_filtered_determinant": { + "filtered_det_lipschitz_all_pairs": true + }, + "LIP_window_variation": { + "double_integral_abs_diff_one_third": true, + "mean_deviation_le_L_over_3": true + }, + "MIX_singleton_mixture": { + "a_le_q": true, + "bonferroni_and_multiple": true, + "configuration_tv_equals_epsilon": true, + "epsilon_le_q_over_2m_minus_q": true, + "height_marginal_bound": true, + "mixture_tv_le_a_over_m": true, + "own_marginal_factor_two": true, + "p1_ge_m_minus_q": true, + "selectors_within_epsilon": true + }, + "MOM_moments": { + "mean_error_power_r5": true, + "tv_controls_bounded_moments": true, + "variance_error_power_r8": true, + "variance_perturbation_3_delta": true + }, + "REG_regression_direction": { + "U_r_reexpression_gives_same_g": true, + "V_g_equals_e_h_exact": true, + "column_bound_r_over_2_sup_D3": true, + "contact_limit_second_order": true, + "g_x_one_and_grad_g_x_zero": true, + "original_endpoint_values_and_gradients_vanish": true, + "pathwise_F_h_minus_F_h2_is_dh_times_g_and_targets_realized": true, + "zero_average_identity_both_endpoints": true + } + }, + "passed": true, + "scientific_effect": "NONE", + "scope": "exact identities and a finite-rank Gaussian regression model only; uniform covariance floors, conditional moments and Kac-Rice are argued in REVIEW.md" +} diff --git a/reviews/remote_height_claude_20260928/REVIEW.md b/reviews/remote_height_claude_20260928/REVIEW.md new file mode 100644 index 000000000..1cc9afe98 --- /dev/null +++ b/reviews/remote_height_claude_20260928/REVIEW.md @@ -0,0 +1,228 @@ +# Nonauthor analytic review: remote within-window height decoupling (Math-#120) + +Scientific effect: **NONE**. This file does not change `lemma_closed`, prizes, premises, `STATUS`, +`PROOF_INDEX`, `GRAPH`, the candidate registry or any author source. It records verdicts. Integration is a +separate act. + +## Object + +| Field | Value | +|---|---| +| Object | OA-REMOTE-HEIGHT-DECOUPLING-20260928-v1 (OpenAI / ChatGPT) | +| Branch / head | `chatgpt/remote-height-decoupling-20260928` / `f3e16585338e4c4dc878df43f9117b1b3ed5a479` ([Math-#120](https://github.com/d6g8k5htny-coder/Math-/pull/120)) | +| `PROOF.md` | Git blob `4d7af587db20515955585732d8150d912c89c0e4`, 13747 B, SHA256 `67249f0311342beab7833cb60c3239d9888df96befda4fbae3ec29a66f8cd78e` | +| Consumed, already on main | [RM] `frontiers/remote_window_20260924/PROOF.md` (blob `b383bfcc…`): §§2–5, (2), (5), (8), (11), (12). [RC] `frontiers/remote_collision_20260928/PROOF.md` (blob `7b48a88e…`): Corollary D. Both blobs match main at `63857fe`. | +| Request | [Owner comment 5878357612](https://github.com/d6g8k5htny-coder/Math-/pull/120#issuecomment-5878357612), "especially (H7)–(H15)" | +| Prior review | OpenAI same-provider, source-exposed review [5344808206](https://github.com/d6g8k5htny-coder/Math-/pull/120#pullrequestreview-5344808206): no blocker. This record is the requested different-provider review. | + +## Provenance + +| Field | Value | +|---|---| +| Reviewer | Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3` | +| Relation | Different provider from the OpenAI author. Same GitHub account as every lane, so no organizational independence is claimed. | +| Exposure | I read `PROOF.md` in full, its README, RECONNAISSANCE, SOURCE_MAP and `check.py`, RM §§1–6, and the OpenAI review above before writing this record. **I am the author of [RC]** ([Math-#110](https://github.com/d6g8k5htny-coder/Math-/pull/110)), whose Corollary D supplies `q_r <= C r^5 |E|`. I consumed RM there. So the probability slice (H18)–(H20) is not independent of my own earlier work. The analytic slice (H7)–(H15) consumes only RM. | +| Author code | Replayed from a `git archive` of `f3e1658`: `verify.py` passes all sources, 12 tests per mode, 5 mutants rejected per mode, and identical output pairs. | +| Independent checks | `height_exact_check.py` is my own exact-rational suite. It shares no code with the author's `check.py` and tests different objects, notably an exact finite-rank Gaussian regression model for (H7)–(H10). It does not replace the Gaussian arguments below. | + +## Verdicts + +| Interface | Verdict | +|---|---| +| (H7) exact pathwise identity `F_h - F_h' = (h - h') g` | **ACCEPT** | +| (H8) uniform `C^q` bound on `g` | **ACCEPT**, with note N2 | +| (H9) `V_r g = e_h`, so the ORIGINAL endpoint values and gradients of `g` vanish | **ACCEPT** | +| (H10) vector zero-average column bound `(r/2)‖D^3 g‖` | **ACCEPT** | +| (H11) Lipschitz endpoint and witness blocks, with no `1/r` loss | **ACCEPT**, and it is deterministic (N1) | +| (H12) `W_r/r^2 = F_d(K_M) F_(d-1)(K_S)` by positive congruence | **ACCEPT** | +| (H13) = RM (8) filtered-determinant Lipschitz bound | **ACCEPT** | +| (H14) product difference and moments; (H15) uniform `L` | **ACCEPT**. `Z_r` is independent of the witness height (§3). | +| (H16)–(H17) marked mean measure, variation `<= (d+1) L l^2 |E|/3` | **ACCEPT** | +| **(H1)** `O(r^3)` own-marginal factorization of the normalized mean | **ACCEPT** | +| (H18)–(H19) mixture, `a <= q`; **(H2)** with the factor two; **(H3)** | **ACCEPT** | +| **(H4)** physical mean `O(r^5)`, variance `O(r^8)` | **ACCEPT** | +| (H20), configuration-level `TV = ε`, measurable and randomized selectors | **ACCEPT** | +| §7 contact-profile compatibility; (H21) abstract `r^2` barrier | **ACCEPT**. It is correctly not claimed as Gaussian sharpness. | + +No defect was found. Notes N1–N6 strengthen or delimit the text without changing it. + +--- + +## §1 — (H7)–(H9): the regression direction and the original pins + +The regression realization is affine in the target. So `F_h - F_h' = Cov(F(·),V_r) Σ_r^{-1}(a_h - a_h')`, and +`a_h - a_h' = (h - h') e_h`. That is (H7), pathwise and exact. It is one coupling, not an independence statement. + +Applying the observation functionals to the deterministic function `g(z) = Cov(F(z),V_r) Σ_r^{-1} e_h` gives +`V_r[g] = Cov(V_r,V_r) Σ_r^{-1} e_h = e_h`. Differentiation commutes with covariance for this smooth field. So +`U_r[g] = 0`, `∇g(x) = 0` and `g(x) = 1`. For `r > 0`, `U_r` is an invertible linear re-expression of +`(f(M), ∇f(M), f(S), ∇f(S))`, with determinant `12 r^{-(d+3)}` in RM §2. Hence all `2(d+1)` original observations +of `g` vanish. That is (H9). + +The owner's first falsification target therefore holds. The zero is a statement about the original values and +gradients, not a contact substitute. + +**Exact check (finite-rank Gaussian model).** Take `F = Σ ξ_m φ_m` over all monomials of degree `<= 5` in the plane, +with independent `ξ_m ~ N(0, 1/(a!b!))`. At `x = (3/5, 2/7)` and `r ∈ {1/3, 1/7, 1/19}`, the direction `g` is computed +exactly. The suite confirms: + +- `V_raw[g] = e_h`, including all six original pins. +- `g` is identical whether the pins are written raw or through RM's `U_r` rows (including the `12/r^3` row). +- For a rational `ξ`, `F_h1 - F_h2 = (h1 - h2) g` coefficientwise, and each `F_h` realizes every original target. + +The `no-endpoint-pins` and `gradient-target` mutants fail these checks. + +**N2 (what (H8) needs).** Cauchy–Schwarz bounds `|∂_z^α Cov(F(z),V_i)|` by `(Var ∂^α F(z) · Var V_i)^{1/2}`. So the +input is uniformly bounded **variances** of the divided-difference rows, not bounded raw coefficients: the fourth +row carries `12/r^3`. RM §2 supplies this through `U_r -> U_0` at second order in `L^2`. `Σ_r^{-1}` is uniformly +bounded on `O(d) × D_ρ` by compactness. The model is consistent with this: the coefficient sup-norm of `g_r - g_0` +is 1.50, 0.091 and 0.0057 at `r = 1/4, 1/16, 1/64`, a ratio of about 16 per factor 4 despite the `r^{-3}` +coefficient. Three observed ratios are consistent with `O(r^2)` but do not by themselves prove that asymptotic. The +proof is RM's analytic argument, which this observation does not replace. + +## §2 — (H10)–(H12): no `1/r` loss in the endpoint columns + +The gradient pins on `g` give `∫_0^r D^2 g(M + t u) u dt = ∇g(S) - ∇g(M) = 0`. Integrating by parts: + +- `D^2 g(M) u = -(1/r) ∫_0^r (r - t) D^3 g(M + t u)[u,u] dt` +- `D^2 g(S) u = (1/r) ∫_0^r t D^3 g(M + t u)[u,u] dt` + +Both are vector identities, so no common Rolle point is needed, and each gives the bound `(r/2) ‖D^3 g‖_∞`. That is +(H10). + +The exact check verifies both identities, for the `xx` and `xz` entries, and the bound at both endpoints. The +`no-endpoint-pins` mutant breaks the identities **and** the bound. This shows the homogeneous gradient pins are what +remove the `1/r`. + +With `α_i = f_uu(i)/r` and `β_i = ∇_⊥ f_u(i)/r`, the `h`-differences are `(h - h') g_uu(i)/r` and +`(h - h') ∇_⊥ g_u(i)/r`, each at most `(1/2)‖D^3 g‖ |h - h'|`. `A_i` and `H_x` change by `(h - h')` times bounded +second derivatives of `g`. That is (H11). The owner's second target holds: the column changes are +`O(r |h - h'|)` before the division by `r`. + +**N1 (deterministic Lipschitz).** `g` is deterministic, so every difference in (H11) is a deterministic number +bounded by a deterministic `C|h - h'|`, for every `ω`. That is stronger than the text needs. Moments enter only +through the `max(‖·‖)^{d-1}` factors in (H14). + +(H12): `H_i = D_r K_i D_r` with `D_r = diag(√r, I_{d-1})`. Sylvester's law preserves inertia, and +`det H_i = r det K_i`. So `F_j(H_i) = r F_j(K_i)` for every `j`, including the singular cases. The exact check covers +150 random rational instances in each of `d = 2, 3`, with the index computed exactly by Descartes' rule on the real-rooted +characteristic polynomial. The `unscaled-beta` mutant (no `√r` on `β`) fails. + +## §3 — (H13)–(H15): filtered determinants, moments, and the normalizer + +(H13) is RM (8), and the proof there is correct. If `X` has index `j` and `Y` does not, the segment from `X` to `Y` +contains a singular matrix `Z`. Then `|F_j(X) - F_j(Y)| = |det X - det Z|`, and `‖X - Z‖ <= ‖X - Y‖`, +`‖Z‖ <= max(‖X‖,‖Y‖)`. The determinant bound `|det X - det Z| <= n max^{n-1} ‖X - Z‖` uses `‖adj‖ <= ‖·‖^{n-1}`. + +The exact check tests the implied Frobenius form on 300 random pairs and six forced index flips across a singular +matrix, with `ε` down to `10^-6`. The `indicator-only` mutant (the bare index indicator) fails on the flips. This +confirms that the Lipschitz quantity is the filtered determinant, as the text says. + +(H14): write `T_h = F_d(K_M(h)) F_{d-1}(K_S(h)) F_j(H_x(h))` and apply +`|abc - a'b'c'| <= |a - a'||bc| + |a'||b - b'||c| + |a'b'||c - c'|`. Each difference is at most +`d max(‖·‖)^{d-1} C|h - h'|`. RM (5) gives uniform moments of all the matrices over the extra height pin, and Hölder +then gives `E|T_h - T_h'| <= C|h - h'|`. `E T_h` is the conditional expectation in (H5), because `F_h` has exactly the +conditional law given `Y_x = (0,h)`. + +**Normalizer (owner's third target).** `Z_r = E_{Q_r} W_r` is an endpoint-only functional. It does not involve +`Y_x`, so it is independent of `h`, and RM (11) makes `r^2/Z_r` uniformly bounded. The density +`p_{Y_x|U_r=v_r}(0,h)` is Gaussian with uniformly positive covariance and bounded mean, so it and its `h`-derivative +are bounded. The product rule gives (H15) with `L` uniform over `x ∈ D_ρ`, marks, frames and small `r`. No +derivative of an indicator, and no differentiation under an unbounded expectation, is used. + +**N3 (why the rate improves).** `R_{r,j}(x,·)` is `Θ(1)`, and it varies by `O(|h - h'|) = O(r^3)` across the window. +So the within-window density is flat to **relative** `O(r^3)`. The contact comparison in RM gives only `O(r)`, because +the finite-`r` spatial and index drift is common to all heights. The new proof avoids that drift by comparing at the +same `r`. + +## §4 — (H16)–(H17) and (H1) + +RM's height disintegration gives the density in `t` on Borel subwindows, so (H16) holds as an equality of finite +marked measures. By Jensen, + +`∫_0^1 |R(b - lθ) - R̄| dθ <= L l ∫∫ |θ - t| = L l/3`. + +The exact check confirms `∫∫ |θ - t| = 1/3`. It also checks the mean deviation `<= L/3` on 300 random piecewise-linear +Lipschitz profiles; the affine extremal case gives `L/4`, and the `lip-constant` mutant (`L/6`) fails. + +The comparison measure `μ^Y ⊗ λ` has the same mass `m_r`. So + +`TV <= (d+1) L l^2 |E| / (6 m_r)`, + +and the RM lower bound `m_r >= c r^3 |E|` gives `O(r^3)`, with `|E|` cancelling. That is (H1). + +## §5 — (H18)–(H20), (H2)–(H4), selectors + +`a = E[N; N >= 2] <= E[N(N-1)] = q`, because `N <= N(N-1)` for `N >= 2`. The mixture identity gives +`TV(S, μ/m) = (a/m) TV(S, η/a) <= a/m`. The factor two in (H2) comes from two separate costs: the mixture, and the +change of marginal from `π_r` to `π_{r,1}`. (H3) needs only one of them. (H4) follows because `0 <= θ <= 1`, so TV +controls `E θ` and `E θ^2` and `|Var θ - 1/12| <= 3δ`. With `l = k r^3`, the errors are `l · r^2 = O(r^5)` and +`l^2 · r^2 = O(r^8)`. + +(H20): `1{N >= 1} >= N - N(N-1)/2` and `1{N >= 2} <= N(N-1)/2`, so `ε <= q/(2m - q)`. The nonempty configuration law +is `(1 - ε)`·singletons + `ε`·multiples, and the two parts have disjoint supports, so its TV to the embedded `S_r` is +exactly `ε`. A deterministic or randomized selector agrees with `S_r` on `{N = 1}`, so its law is within `ε`. + +All of these were checked on 300 random exact configuration laws with 8 marks and up to 3 points, plus one extremal +law with an equality case: the singleton at one mark and the pair on two others. That law gives equality in both +`TV(S, μ/m) = a/m` and `ε = q/(2m - q)`, so neither bound can be tightened in general. The mutants +`a-as-probability` (using `P(N >= 2)` in place of `a`) and `eps-over-2m` fail on it. Both a min-mark selector and the +uniform randomized selector satisfy the selector bounds. + +## §6 — §7 compatibility and the (H21) barrier + +`TV(S_r, π_E ⊗ λ) <= O(r^2) + TV(π_{r,1}, π_E) = O(r)`. The given premises only establish `O(r)` here. No lower +bound or optimal Gaussian profile rate is claimed. There is no conflict with (H1)–(H3). + +The (H21) example was rebuilt exactly at `r = 1/2, 1/3, 1/10, 1/50`: + +- The mean is exactly `m × Unif{A,B} × Unif(0,1)`. +- `q = a = r^5`. +- The singleton height TV is `r^2/(2(1 - r^2))`, which is at most `a/m`. +- The law is valid for `r <= 1/2`, and the TV exceeds `r^3` for `r <= 1/10`. + +Within each height half the densities are constant, so bin-level TV equals the continuous TV. The example is +abstract. It shows that the two moment premises cannot give `O(r^3)`, and the text correctly does not claim a +Gaussian lower bound. + +**N4 (consistency with #116).** On the whole torus, #116's LOCAL (L3) gives `P(N >= 2 | N >= 1) >= c_0`; see my +review in [Math-#123](https://github.com/d6g8k5htny-coder/Math-/pull/123). Here `ε = O(r^2)` only on `D_ρ`. The +two statements are consistent: the fixed-`ρ` restriction is exactly what separates them, and #120 claims nothing +global. + +**N5 (dimension).** RM and RC Corollary D both hold for every fixed `d >= 2`, so #120's `d >= 2` scope is +supported. Constants depend on `d, L, ρ, B, K`. + +**N6 (candidate C5).** #120 does not consume #116's `HEIGHT_MARKS.md`. It proves a different, own-marginal target. +Nothing here reviews C5. + +## Checks run + +``` +python3 -B -S verify.py # author packet at f3e1658 (git archive): PASS, 12 tests, 5 mutants per mode +python3 -B -S height_exact_check.py # rc 0, stdout == RESULTS.json +python3 -B -O -S height_exact_check.py # rc 0, byte-identical +python3 -B -S height_exact_check.py --mutant M # rc 1 for each of the nine mutants: + no-endpoint-pins gradient-target unscaled-beta indicator-only lip-constant + eps-over-2m a-as-probability p2-r6 var-l +``` + +Python standard library only. The workflow `.github/workflows/remote-height-review.yml` verifies the packet tree +against `SOURCE_FILES.json`, replays both modes and requires every mutant to be rejected. + +## Not established here + +- RM's own premises: the covariance floor, the moments (5) and the Kac–Rice formula (12). They are consumed as + written, with RM's existing review status. +- Any `ρ -> 0`, global, `k -> 0`, unbounded-mark or random-domain statement. The text excludes all of these. +- Numerical `C`, `r_*`, or an optimal Gaussian rate. +- Organizational independence: all lanes share one GitHub account, and I wrote RC. + +## Revision history + +- **v1**, reviewing head `f3e1658`: initial packet. +- **v2**, responding to [owner comment 5879827321](https://github.com/d6g8k5htny-coder/Math-/pull/123#issuecomment-5879827321). + Wording only; no verdict, check or source changes. + - §6 no longer infers from an `O(r)` upper bound that the contact-profile rate "cannot be better". The given + premises establish only `O(r)`, and no lower bound is claimed. + - N2 now presents the three finite-rank ratios as consistent with `O(r^2)`, not as a proof of it. diff --git a/reviews/remote_height_claude_20260928/SOURCE_FILES.json b/reviews/remote_height_claude_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..1443b3dab --- /dev/null +++ b/reviews/remote_height_claude_20260928/SOURCE_FILES.json @@ -0,0 +1,33 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#120", + "head": "f3e16585338e4c4dc878df43f9117b1b3ed5a479", + "path": "frontiers/remote_height_decoupling_20260928/PROOF.md", + "git_blob": "4d7af587db20515955585732d8150d912c89c0e4", + "bytes": 13747, + "sha256": "67249f0311342beab7833cb60c3239d9888df96befda4fbae3ec29a66f8cd78e" + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 15257, + "sha256": "ebd045805855817821815d70acc811fe4c4b65a9db4a9f605fc2fdf611445489", + "git_blob": "1cc9afe98ba48bac5699f76021d339476b061e5e" + }, + { + "path": "height_exact_check.py", + "bytes": 21277, + "sha256": "52e24dd08961589baee06f4777b3fafdb53f7d1f61865201ba5dcd97c897e0c4", + "git_blob": "01ac919b2bbf7fcd6c9f276a6294478c5f5ce698" + }, + { + "path": "RESULTS.json", + "bytes": 1786, + "sha256": "a758f43296ce43c727667201846cc7458834d8686da05b4fed4a6e70774d6608", + "git_blob": "914ccba4c12b304457449f5786878bd962345f69" + } + ] +} diff --git a/reviews/remote_height_claude_20260928/height_exact_check.py b/reviews/remote_height_claude_20260928/height_exact_check.py new file mode 100644 index 000000000..01ac919b2 --- /dev/null +++ b/reviews/remote_height_claude_20260928/height_exact_check.py @@ -0,0 +1,495 @@ +"""Independent exact checks for the nonauthor review of Math-#120 +(frontiers/remote_height_decoupling_20260928/PROOF.md, remote within-window height decoupling). + +Python standard library only; exact rational arithmetic. Written after reading the author's check.py, but it +shares no code with it and tests different objects. Groups: + + REG (H7)-(H10) in an exact finite-rank Gaussian model on the plane (monomial basis of degree <= 5 with + positive coefficient variances). The regression direction g = Cov(F, V) Sigma^-1 e_h is computed + exactly. Checks: V[g] = e_h, hence the ORIGINAL endpoint values and gradients of g vanish; g is the same + whether the pins are written raw or through RM's U_r transform; the pathwise identity + F_h - F_h' = (h - h') g; the vector zero-average identity behind (H10) at both endpoints; the bound + |D^2 g(i) u| <= (r/2) sup |D^3 g|; and second-order convergence of g to its contact limit. + CONG (H12) positive congruence: det H = r det K and equal inertia, so F_j(H) = r F_j(K), for d = 2, 3. + FDET (H13) = RM (8) for the filtered determinant on random and index-changing pairs (Frobenius form, which + the operator-norm statement implies). + LIP (H17) integral of |theta - t| is 1/3; mean deviation of Lipschitz densities is at most L/3. + MIX (H18)-(H20) singleton/mean mixture, a <= q, Bonferroni, epsilon, own-marginal factor two, + configuration-level TV = epsilon, and deterministic and randomized selectors, on random exact laws. + BAR (H21) the abstract r^2 barrier: exactly flat mean, q = r^5, singleton TV = r^2/(2(1-r^2)). + MOM (H4) TV controls bounded moments; physical mean/variance power ledger. + +Not a continuum or Gaussian proof: uniform covariance floors, conditional moments and Kac-Rice are argued in +REVIEW.md. +""" +import argparse +import json +import random +import sys +from fractions import Fraction as F +from math import comb, factorial + +MUTANTS = ("no-endpoint-pins", "gradient-target", "unscaled-beta", "indicator-only", "lip-constant", + "eps-over-2m", "a-as-probability", "p2-r6", "var-l") + +# ---------------------------------------------------------------------------------------------------------- +# Exact linear algebra and polynomials +# ---------------------------------------------------------------------------------------------------------- + + +def solve(A, b): + n = len(A) + M = [list(row) + [b[i]] for i, row in enumerate(A)] + for col in range(n): + piv = next(i for i in range(col, n) if M[i][col] != 0) + M[col], M[piv] = M[piv], M[col] + pv = M[col][col] + M[col] = [x / pv for x in M[col]] + for i in range(n): + if i != col and M[i][col] != 0: + fac = M[i][col] + M[i] = [x - fac * y for x, y in zip(M[i], M[col])] + return [M[i][n] for i in range(n)] + + +def det(A): + n = len(A) + if n == 1: + return A[0][0] + return sum((-1) ** j * A[0][j] * det([row[:j] + row[j + 1:] for row in A[1:]]) for j in range(n)) + + +def charpoly(A): + """Faddeev-LeVerrier: coefficients c[0..n] of det(t I - A), c[n] = 1.""" + n = len(A) + c = [F(0)] * (n + 1) + c[n] = F(1) + Mk = [[F(0)] * n for _ in range(n)] + for k in range(1, n + 1): + AM = [[sum(A[i][l] * Mk[l][j] for l in range(n)) for j in range(n)] for i in range(n)] + Mk = [[AM[i][j] + (c[n - k + 1] if i == j else 0) for j in range(n)] for i in range(n)] + AMk = [[sum(A[i][l] * Mk[l][j] for l in range(n)) for j in range(n)] for i in range(n)] + c[n - k] = -sum(AMk[i][i] for i in range(n)) / k + return c + + +def inertia(A): + """(negatives, zeros) for a symmetric rational matrix: Descartes' rule is exact for real-rooted polynomials.""" + c = charpoly(A) + z = 0 + while c[z] == 0: + z += 1 + q = [c[i] * (-1) ** i for i in range(z, len(c))] # coefficients of p(-t)/t^z + signs = [x > 0 for x in q if x != 0] + return sum(1 for u, v in zip(signs, signs[1:]) if u != v), z + + +def Fj(A, j, mut=None): + neg, z = inertia(A) + if z or neg != j: + return F(0) + return F(1) if mut == "indicator-only" else abs(det(A)) + + +def frob2(A): + return sum(x * x for row in A for x in row) + + +DEG = 5 +BASIS = [(a, b) for a in range(DEG + 1) for b in range(DEG + 1 - a)] +WEIGHT = [F(1, factorial(a) * factorial(b)) for a, b in BASIS] # positive coefficient variances + + +def dmono(m, i, j, pt): + a, b = m + if i > a or j > b: + return F(0) + c = (factorial(a) // factorial(a - i)) * (factorial(b) // factorial(b - j)) + return c * pt[0] ** (a - i) * pt[1] ** (b - j) + + +def apply(func, coeffs): + return sum(w * dmono(m, i, j, pt) * coeffs[k] for k, m in enumerate(BASIS) for (w, i, j, pt) in func) + + +def row(func): + return [sum(w * dmono(m, i, j, pt) for (w, i, j, pt) in func) for m in BASIS] + + +def observations(r, x, kind): + O = (F(0), F(0)) + Y = [[(1, 1, 0, x)], [(1, 0, 1, x)], [(1, 0, 0, x)]] + if kind == "Y": + return Y + if kind == "U0": + U0 = [[(1, 0, 0, O)], [(1, 1, 0, O)], [(1, 2, 0, O)], [(1, 3, 0, O)], [(1, 0, 1, O)], [(1, 1, 1, O)]] + return U0 + Y + M, S = (-r / 2, F(0)), (r / 2, F(0)) + raw = [[(1, 0, 0, M)], [(1, 1, 0, M)], [(1, 0, 1, M)], [(1, 0, 0, S)], [(1, 1, 0, S)], [(1, 0, 1, S)]] + U = [[(F(1, 2), 0, 0, M), (F(1, 2), 0, 0, S)], + [(-1 / r, 0, 0, M), (1 / r, 0, 0, S)], + [(-1 / r, 1, 0, M), (1 / r, 1, 0, S)], + [(6 / r ** 2, 1, 0, M), (6 / r ** 2, 1, 0, S), (12 / r ** 3, 0, 0, M), (-12 / r ** 3, 0, 0, S)], + [(F(1, 2), 0, 1, M), (F(1, 2), 0, 1, S)], + [(-1 / r, 0, 1, M), (1 / r, 0, 1, S)]] + return {"raw": raw + Y, "U": U + Y}[kind] + + +def direction(V, e_index): + """Coefficients of g = Cov(F(.), V) Sigma^-1 e and the observation matrix A.""" + A = [row(f) for f in V] + n = len(V) + Sig = [[sum(A[k][i] * WEIGHT[i] * A[l][i] for i in range(len(BASIS))) for l in range(n)] for k in range(n)] + e = [F(0)] * n + e[e_index] = F(1) + y = solve(Sig, e) + return [WEIGHT[i] * sum(A[k][i] * y[k] for k in range(n)) for i in range(len(BASIS))], A, Sig + + +def restrict_axis(coeffs, i, j, r): + """Univariate coefficients in t of (d_x^i d_z^j g)(-r/2 + t, 0).""" + out = [F(0)] * (DEG + 1) + for k, (a, b) in enumerate(BASIS): + if coeffs[k] == 0 or i > a or j != b: + continue + c = coeffs[k] * (factorial(a) // factorial(a - i)) * factorial(b) + p = a - i # (-r/2 + t)^p + for s in range(p + 1): + out[s] += c * comb(p, s) * (-r / 2) ** (p - s) + while len(out) > 1 and out[-1] == 0: + out.pop() + return out + + +def uni_int(p, weight, r): + """integral_0^r weight(t) p(t) dt for weight 'r-t' or 't'.""" + tot = F(0) + for s, c in enumerate(p): + if weight == "t": + tot += c * r ** (s + 2) / (s + 2) + else: + tot += c * (r * r ** (s + 1) / (s + 1) - r ** (s + 2) / (s + 2)) + return tot + + +def uni_eval(p, t): + return sum(c * t ** s for s, c in enumerate(p)) + + +def uni_maxabs(p, r): + assert len(p) <= 3 + pts = [F(0), r] + if len(p) == 3 and p[2] != 0: + v = -p[1] / (2 * p[2]) + if 0 < v < r: + pts.append(v) + return max(abs(uni_eval(p, t)) for t in pts) + + +# ---------------------------------------------------------------------------------------------------------- +# Groups +# ---------------------------------------------------------------------------------------------------------- + + +def check_reg(mut): + out = {} + x = (F(3, 5), F(2, 7)) + nopin = mut == "no-endpoint-pins" + # V ends with (f_x(x), f_z(x), f(x)); the mutant conditions on the witness observations alone. + e_idx = (7 if mut == "gradient-target" else 8) - (6 if nopin else 0) + kind_r, kind_0 = ("Y", "Y") if nopin else ("U", "U0") + ok_ev, ok_pins, ok_one, ok_inv, ok_path, ok_avg, ok_bound = True, True, True, True, True, True, True + rng = random.Random(120) + for r in (F(1, 3), F(1, 7), F(1, 19)): + used = observations(r, x, "Y" if nopin else "raw") + c, A, Sig = direction(used, e_idx) + cU, _, _ = direction(observations(r, x, "U"), 8) + ok_inv &= c == cU + raw = observations(r, x, "raw") + vals = [apply(f, c) for f in raw] + target = [F(0)] * 9 + target[8] = F(1) + ok_ev &= vals == target + ok_pins &= all(v == 0 for v in vals[:6]) + ok_one &= vals[8] == 1 and vals[6] == 0 and vals[7] == 0 + # (H7): pathwise identity with one unconditioned coefficient vector xi; the conditioned copies must + # also realize every ORIGINAL target. + xi = [F(rng.randrange(-40, 41), rng.randrange(1, 9)) for _ in BASIS] + Vxi = [sum(a * z for a, z in zip(Ar, xi)) for Ar in A] + vt = [F(1, 3), F(0), F(0), F(1, 3) - F(2, 5) * r ** 3, F(0), F(0), F(0), F(0)] + + def cond(h): + a_h = (vt[6:] if nopin else vt) + [h] + y = solve(Sig, [ai - vi for ai, vi in zip(a_h, Vxi)]) + return [xi[i] + WEIGHT[i] * sum(A[k][i] * y[k] for k in range(len(A))) for i in range(len(BASIS))] + + h1, h2 = F(1, 3) - F(1, 10) * r ** 3, F(1, 3) - F(3, 10) * r ** 3 + f1, f2 = cond(h1), cond(h2) + ok_path &= all(u - v == (h1 - h2) * gi for u, v, gi in zip(f1, f2, c)) + ok_path &= [apply(f, f1) for f in raw] == vt[:6] + [F(0), F(0), h1] + # (H10): vector zero-average identity at both endpoints, for the u-column (xx and xz entries). + for (i, j) in ((2, 0), (1, 1)): + col = restrict_axis(c, i, j, r) + third = restrict_axis(c, i + 1, j, r) + at_M, at_S = uni_eval(col, F(0)), uni_eval(col, r) + ok_avg &= at_M == -uni_int(third, "r-t", r) / r and at_S == uni_int(third, "t", r) / r + bnd = r / 2 * uni_maxabs(third, r) + ok_bound &= abs(at_M) <= bnd and abs(at_S) <= bnd + out["V_g_equals_e_h_exact"] = ok_ev + out["original_endpoint_values_and_gradients_vanish"] = ok_pins + out["g_x_one_and_grad_g_x_zero"] = ok_one + out["U_r_reexpression_gives_same_g"] = ok_inv + out["pathwise_F_h_minus_F_h2_is_dh_times_g_and_targets_realized"] = ok_path + out["zero_average_identity_both_endpoints"] = ok_avg + out["column_bound_r_over_2_sup_D3"] = ok_bound + # Second-order contact convergence of the direction: ||g_r - g_0|| shrinks by >= 8 per factor 4 in r. + c0, _, _ = direction(observations(None, x, kind_0), e_idx) + ds = [] + for r in (F(1, 4), F(1, 16), F(1, 64)): + cr, _, _ = direction(observations(r, x, kind_r), e_idx) + ds.append(max(abs(u - v) for u, v in zip(cr, c0))) + out["contact_limit_second_order"] = ds[1] * 8 <= ds[0] and ds[2] * 8 <= ds[1] and ds[2] > 0 + return out + + +def check_cong(mut): + rng = random.Random(1201) + ok_det, ok_idx, ok_F = True, True, True + for n in (2, 3): + for _ in range(150): + s = F(rng.randrange(1, 20), 20) + r = s * s + alpha = F(rng.randrange(-9, 10), rng.randrange(1, 4)) + beta = [F(rng.randrange(-9, 10), rng.randrange(1, 4)) for _ in range(n - 1)] + Ab = [[F(0)] * (n - 1) for _ in range(n - 1)] + for i in range(n - 1): + for j in range(i, n - 1): + Ab[i][j] = Ab[j][i] = F(rng.randrange(-9, 10), rng.randrange(1, 4)) + sb = 1 if mut == "unscaled-beta" else s + K = [[alpha] + [sb * b for b in beta]] + [[sb * beta[i]] + Ab[i] for i in range(n - 1)] + H = [[r * alpha] + [r * b for b in beta]] + [[r * beta[i]] + Ab[i] for i in range(n - 1)] + ok_det &= det(H) == r * det(K) + ok_idx &= inertia(H) == inertia(K) + ok_F &= all(Fj(H, j) == r * Fj(K, j) for j in range(n + 1)) + return {"det_H_equals_r_det_K": ok_det, "inertia_preserved": ok_idx, "F_j_H_equals_r_F_j_K": ok_F} + + +def check_fdet(mut): + rng = random.Random(1202) + ok, flips = True, 0 + pairs = [] + for n in (2, 3): + for _ in range(150): + X = [[F(0)] * n for _ in range(n)] + E = [[F(0)] * n for _ in range(n)] + for i in range(n): + for j in range(i, n): + X[i][j] = X[j][i] = F(rng.randrange(-9, 10), rng.randrange(1, 5)) + E[i][j] = E[j][i] = F(rng.randrange(-9, 10), rng.randrange(1, 5)) + t = F(1, rng.choice((1, 10, 1000))) + pairs.append((X, [[X[i][j] + t * E[i][j] for j in range(n)] for i in range(n)])) + for eps in (F(1, 10), F(1, 1000), F(1, 10 ** 6)): # forced index change across a singular matrix + D1 = [[F(1) if i == j else F(0) for j in range(n)] for i in range(n)] + D2 = [list(rw) for rw in D1] + D1[n - 1][n - 1], D2[n - 1][n - 1] = eps, -eps + pairs.append((D1, D2)) + for X, Y in pairs: + n = len(X) + m2 = max(frob2(X), frob2(Y)) + d2 = frob2([[X[i][j] - Y[i][j] for j in range(n)] for i in range(n)]) + flips += inertia(X) != inertia(Y) + for j in range(n + 1): + diff = Fj(X, j, mut) - Fj(Y, j, mut) + ok &= diff * diff <= n * n * m2 ** (n - 1) * d2 + return {"filtered_det_lipschitz_all_pairs": ok and flips >= 6} + + +def check_lip(mut): + out = {} + # integral_0^1 integral_0^1 |theta - t| dt dtheta = integral_0^1 (theta^2/2 + (1-theta)^2/2) dtheta + out["double_integral_abs_diff_one_third"] = F(1, 6) + F(1, 6) == F(1, 3) + const = F(1, 6) if mut == "lip-constant" else F(1, 3) + rng = random.Random(1203) + Lc = F(3) + ok = True + cases = [[Lc] * 8, [-Lc] * 8] + [[F(rng.randrange(-30, 31), 10) for _ in range(8)] for _ in range(300)] + for slopes in cases: + knots = [F(5)] + for sl in slopes: + knots.append(knots[-1] + sl / 8) + mean = sum((knots[i] + knots[i + 1]) / 2 for i in range(8)) / 8 + dev = F(0) + for i in range(8): + u, v = knots[i] - mean, knots[i + 1] - mean # linear on a piece of width 1/8 + if u * v >= 0: + dev += abs(u + v) / 2 / 8 + else: + dev += (u * u + v * v) / (2 * abs(v - u)) / 8 + ok &= dev <= Lc * const + out["mean_deviation_le_L_over_3"] = ok + return out + + +def tv(p, q): + keys = set(p) | set(q) + return sum(abs(p.get(k, F(0)) - q.get(k, F(0))) for k in keys) / 2 + + +def law_stats(law): + m = sum(P * len(c) for c, P in law.items()) + mu, sig = {}, {} + for c, P in law.items(): + for pt in c: + mu[pt] = mu.get(pt, F(0)) + P + if len(c) == 1: + sig[c[0]] = sig.get(c[0], F(0)) + P + a = sum(mu.values()) - sum(sig.values()) + q = sum(P * len(c) * (len(c) - 1) for c, P in law.items()) + alpha = sum(P for c, P in law.items() if len(c) >= 2) + P1 = sum(P for c, P in law.items() if len(c) >= 1) + return m, mu, sig, a, q, alpha, P1 + + +def ymarg(d): + out = {} + for (y, th), v in d.items(): + out[y] = out.get(y, F(0)) + v + return out + + +def times_lambda(d): + return {(y, th): v / 2 for y, v in d.items() for th in (0, 1)} + + +def check_mix(mut): + rng = random.Random(1204) + marks = [(y, th) for y in range(4) for th in (0, 1)] + laws = [] + s, p = F(1, 10), F(1, 20) + laws.append({(): 1 - s - p, ((0, 0),): s, ((1, 0), (2, 1)): p}) # extremal: equality in (H19), (H20) + for _ in range(300): + w = {(): F(rng.randrange(1000, 3000))} + for mk in marks: + w[(mk,)] = F(rng.randrange(0, 60)) + for _ in range(6): + c = tuple(sorted(rng.sample(marks, 2))) + w[c] = w.get(c, F(0)) + rng.randrange(0, 6) + for _ in range(3): + c = tuple(sorted(rng.sample(marks, 3))) + w[c] = w.get(c, F(0)) + rng.randrange(0, 3) + tot = sum(w.values()) + laws.append({c: v / tot for c, v in w.items() if v}) + res = dict.fromkeys(("mixture_tv_le_a_over_m", "a_le_q", "p1_ge_m_minus_q", "bonferroni_and_multiple", + "epsilon_le_q_over_2m_minus_q", "own_marginal_factor_two", "height_marginal_bound", + "configuration_tv_equals_epsilon", "selectors_within_epsilon"), True) + for law in laws: + m, mu, sig, a, q, alpha, P1 = law_stats(law) + p1 = sum(sig.values()) + S = {k: v / p1 for k, v in sig.items()} + mun = {k: v / m for k, v in mu.items()} + abound = alpha if mut == "a-as-probability" else a + res["mixture_tv_le_a_over_m"] &= tv(S, mun) <= abound / m + res["a_le_q"] &= a <= q + res["p1_ge_m_minus_q"] &= p1 == m - a and p1 >= m - q + res["bonferroni_and_multiple"] &= P1 >= m - q / 2 and alpha <= q / 2 + eps = alpha / P1 + ebound = q / (2 * m) if mut == "eps-over-2m" else q / (2 * m - q) + res["epsilon_le_q_over_2m_minus_q"] &= 2 * m > q and eps <= ebound + base = tv(mun, times_lambda(ymarg(mun))) + pi1 = ymarg(S) + res["own_marginal_factor_two"] &= (tv(pi1, ymarg(mun)) <= tv(S, mun) + and tv(S, times_lambda(pi1)) <= 2 * a / m + base) + thS = {th: sum(v for (y, t), v in S.items() if t == th) for th in (0, 1)} + res["height_marginal_bound"] &= tv(thS, {0: F(1, 2), 1: F(1, 2)}) <= a / m + base + cond = {c: P / P1 for c, P in law.items() if c} + emb = {(k,): v for k, v in S.items()} + res["configuration_tv_equals_epsilon"] &= tv(cond, emb) == eps + det_sel, rnd_sel = {}, {} + for c, P in cond.items(): + k = min(c) + det_sel[k] = det_sel.get(k, F(0)) + P + for pt in c: + rnd_sel[pt] = rnd_sel.get(pt, F(0)) + P / len(c) + for sel in (det_sel, rnd_sel): + res["selectors_within_epsilon"] &= (tv(sel, S) <= eps and + tv(sel, times_lambda(ymarg(sel))) <= 2 * eps + tv(S, times_lambda(pi1))) + return res + + +def check_bar(mut): + ok_flat, ok_q, ok_tv, ok_nonneg, ok_beats = True, True, True, True, True + for r in (F(1, 2), F(1, 3), F(1, 10), F(1, 50)): + m = r ** 3 + p2 = r ** 6 / 2 if mut == "p2-r6" else r ** 5 / 2 + sig = {("A", 0): m / 4 - p2, ("A", 1): m / 4, ("B", 0): m / 4 - p2, ("B", 1): m / 4} + law = {c: v for c, v in (((k,), v) for k, v in sig.items())} + law[(("A", 0), ("B", 0))] = p2 + law[()] = 1 - sum(sig.values()) - p2 + mm, mu, sg, a, q, alpha, P1 = law_stats(law) + ok_flat &= mm == m and all(v == m / 4 for v in mu.values()) + ok_q &= q == r ** 5 and a == q + p1 = sum(sg.values()) + th = {t: sum(v for (y, tt), v in sg.items() if tt == t) / p1 for t in (0, 1)} + val = tv(th, {0: F(1, 2), 1: F(1, 2)}) + ok_tv &= val == r * r / (2 * (1 - r * r)) and val <= a / m + ok_nonneg &= all(v >= 0 for v in law.values()) + if r <= F(1, 10): + ok_beats &= val > r ** 3 + return {"mean_exactly_flat": ok_flat, "q_equals_r5": ok_q, "singleton_tv_r2_over_2_1_minus_r2": ok_tv, + "valid_law_r_le_half": ok_nonneg, "exceeds_r3": ok_beats} + + +def check_mom(mut): + rng = random.Random(1205) + grid = [F(i, 12) for i in range(13)] + ok = True + for _ in range(300): + P = [F(rng.randrange(0, 20)) for _ in grid] + Q = [F(rng.randrange(0, 20)) for _ in grid] + if not sum(P) or not sum(Q): + continue + P = [v / sum(P) for v in P] + Q = [v / sum(Q) for v in Q] + d = sum(abs(u - v) for u, v in zip(P, Q)) / 2 + for phi in (lambda t: t, lambda t: t * t): + ok &= abs(sum(u * phi(t) for u, t in zip(P, grid)) - sum(v * phi(t) for v, t in zip(Q, grid))) <= d + # Var(theta) perturbation: E theta = 1/2 + d1, E theta^2 = 1/3 + d2, |d_i| <= delta <= 1 => |Var - 1/12| <= 3 delta + ok_var = True + for _ in range(300): + delta = F(rng.randrange(1, 100), 100) + d1 = delta * F(rng.randrange(-100, 101), 100) + d2 = delta * F(rng.randrange(-100, 101), 100) + var = F(1, 3) + d2 - (F(1, 2) + d1) ** 2 + ok_var &= abs(var - F(1, 12)) <= 3 * delta + lpow = 3 + varpow = 1 if mut == "var-l" else 2 + return {"tv_controls_bounded_moments": ok, "variance_perturbation_3_delta": ok_var, + "mean_error_power_r5": lpow + 2 == 5, "variance_error_power_r8": varpow * lpow + 2 == 8} + + +def flatten(d): + for v in d.values(): + if isinstance(v, dict): + yield from flatten(v) + else: + yield v + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + mut = ap.parse_args().mutant + checks = {"REG_regression_direction": check_reg(mut), "CONG_congruence": check_cong(mut), + "FDET_filtered_determinant": check_fdet(mut), "LIP_window_variation": check_lip(mut), + "MIX_singleton_mixture": check_mix(mut), "BAR_r2_barrier": check_bar(mut), + "MOM_moments": check_mom(mut)} + passed = all(flatten(checks)) + print(json.dumps({"checks": checks, "passed": passed, "scientific_effect": "NONE", + "scope": "exact identities and a finite-rank Gaussian regression model only; uniform " + "covariance floors, conditional moments and Kac-Rice are argued in REVIEW.md"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main())