diff --git a/.github/workflows/d5-punctured-pin-continuum-review.yml b/.github/workflows/d5-punctured-pin-continuum-review.yml new file mode 100644 index 000000000..7e7885d04 --- /dev/null +++ b/.github/workflows/d5-punctured-pin-continuum-review.yml @@ -0,0 +1,59 @@ +name: D5 punctured-pin continuum record checks + +'on': + pull_request: + paths: + - 'reviews/d5_punctured_pin_continuum_claude_20260929/**' + - '.github/workflows/d5-punctured-pin-continuum-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/d5_punctured_pin_continuum_claude_20260929').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 / 'pp_continuum_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['wrong-a-floor', 'drop-minor', 'angle-sensitive-axis', 'same-sign-k', 'absolute-remainder'] + 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/sard-g-a2-fixed-frame-review.yml b/.github/workflows/sard-g-a2-fixed-frame-review.yml new file mode 100644 index 000000000..3b194f1ce --- /dev/null +++ b/.github/workflows/sard-g-a2-fixed-frame-review.yml @@ -0,0 +1,59 @@ +name: SARD-G A2 fixed-frame nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/sard_g_a2_fixed_frame_claude_20260929/**' + - '.github/workflows/sard-g-a2-fixed-frame-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/sard_g_a2_fixed_frame_claude_20260929').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 / 'a2ff_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['wrong-slope', 'bounded-quotient', 'nonzero-gradient'] + 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/sard-g-a2-fixed-frame.yml b/.github/workflows/sard-g-a2-fixed-frame.yml new file mode 100644 index 000000000..3f207ebf5 --- /dev/null +++ b/.github/workflows/sard-g-a2-fixed-frame.yml @@ -0,0 +1,30 @@ +name: SARD-G fixed-frame and closure finite controls +'on': + pull_request: + paths: + - 'frontiers/sard_g_a2_parameter_20260929/**' + - '.github/workflows/sard-g-a2-fixed-frame.yml' + push: + branches: [main] + paths: + - 'frontiers/sard_g_a2_parameter_20260929/**' + - '.github/workflows/sard-g-a2-fixed-frame.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + finite-fixed-frame: + 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: Exact successor sources and intended semantic failures in both modes + run: | + set -euo pipefail + python -B -S frontiers/sard_g_a2_parameter_20260929/v2/verify.py --output "${RUNNER_TEMP}/sard-fixed-frame-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}" + git diff --exit-code diff --git a/.github/workflows/sard-g-a2-parameter.yml b/.github/workflows/sard-g-a2-parameter.yml new file mode 100644 index 000000000..05d079a86 --- /dev/null +++ b/.github/workflows/sard-g-a2-parameter.yml @@ -0,0 +1,25 @@ +name: SARD-G A2 finite interface controls +'on': + pull_request: + paths: + - 'frontiers/sard_g_a2_parameter_20260929/**' + - '.github/workflows/sard-g-a2-parameter.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + finite-a2: + 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' + - run: | + set -euo pipefail + python -B -S frontiers/sard_g_a2_parameter_20260929/check.py + python -B -O -S frontiers/sard_g_a2_parameter_20260929/check.py + git diff --exit-code diff --git a/.github/workflows/sard-g-a2-regularity.yml b/.github/workflows/sard-g-a2-regularity.yml new file mode 100644 index 000000000..bb5fe34d8 --- /dev/null +++ b/.github/workflows/sard-g-a2-regularity.yml @@ -0,0 +1,56 @@ +name: SARD-G A2 regularity note checks + +'on': + pull_request: + paths: + - 'frontiers/sard_g_a2_regularity_20260929/**' + - '.github/workflows/sard-g-a2-regularity.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + witness: + 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('frontiers/sard_g_a2_regularity_20260929').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text()) + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest['files']: + path = root / 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 / 'a2_check.py') + expected = (root / 'RESULTS.json').read_bytes() + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=120).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in ['lp-exponent', 'nonlinear-superposition', 'saddle-sign']: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=120).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/sard-g-pinned-transfer.yml b/.github/workflows/sard-g-pinned-transfer.yml new file mode 100644 index 000000000..deb283f56 --- /dev/null +++ b/.github/workflows/sard-g-pinned-transfer.yml @@ -0,0 +1,56 @@ +name: SARD-G pinned transfer note checks + +'on': + pull_request: + paths: + - 'frontiers/sard_g_pinned_transfer_20260929/**' + - '.github/workflows/sard-g-pinned-transfer.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + witness: + 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('frontiers/sard_g_pinned_transfer_20260929').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text()) + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest['files']: + path = root / 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 / 'transfer_check.py') + expected = (root / 'RESULTS.json').read_bytes() + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=120).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in ['no-correction', 'unprojected', 'duplicate-pin']: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=120).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/sard-g-r1r2-review.yml b/.github/workflows/sard-g-r1r2-review.yml new file mode 100644 index 000000000..9d9329fdc --- /dev/null +++ b/.github/workflows/sard-g-r1r2-review.yml @@ -0,0 +1,59 @@ +name: SARD-G R1/R2 second-provider review checks + +'on': + pull_request: + paths: + - 'reviews/sard_g_r1r2_claude_20260929/**' + - '.github/workflows/sard-g-r1r2-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/sard_g_r1r2_claude_20260929').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 / 'r1r2_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['relint-rule', 'whole-prefix', 'no-terminal-slack', 'endpoint-accept', 'sign-flip'] + 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/sard-robust-charts.yml b/.github/workflows/sard-robust-charts.yml new file mode 100644 index 000000000..2ec278e32 --- /dev/null +++ b/.github/workflows/sard-robust-charts.yml @@ -0,0 +1,31 @@ +name: SARD robust-chart exact interface controls + +'on': + pull_request: + paths: + - 'frontiers/sard_g_robust_charts_20260929/**' + - '.github/workflows/sard-robust-charts.yml' + push: + branches: [main] + paths: + - 'frontiers/sard_g_robust_charts_20260929/**' + - '.github/workflows/sard-robust-charts.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + robust-chart-controls: + 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: Exact packet and both-mode geometric negatives + run: | + set -euo pipefail + python -B -S frontiers/sard_g_robust_charts_20260929/verify.py --output "${RUNNER_TEMP}/sard-robust-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}" + git diff --exit-code diff --git a/frontiers/sard_g_a2_parameter_20260929/PROOF.md b/frontiers/sard_g_a2_parameter_20260929/PROOF.md new file mode 100644 index 000000000..36bbc0c30 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/PROOF.md @@ -0,0 +1,119 @@ +# SARD-G A2 parameter-regularity interface + +Object: OA-SARD-A2-PARAMETER-20260929-v1. +Author: OpenAI / ChatGPT. +Disposition: AUTHOR-SIDE DOWNSTREAM CANDIDATE; nonauthor analytic review required. +Scientific effect: NONE. + +## 1. Exact interface + +Let X=C^2(T_L^2) and V_f=grad f, viewed as a C^1 vector field. Fix f0 and a +nondegenerate index-one critical point p0. After shrinking an X-neighborhood U +of f0 and a coordinate ball B about p0, the following are the A2-T/A2-D claims +consumed by Math-#135. + +**A2.1 tracked saddle.** There is a unique map p:U->B with V_f(p(f))=0. It is +C^1 as a map from the Banach space X to R^2. Its derivative is +Dp(f)[h]=-H_f(p(f))^{-1} grad h(p(f)). + +**A2.2 local branch germs.** After choosing one stable/unstable eigendirection +and its sign at f0, there are fixed compact graph-parameter intervals and maps +Gamma_f^sigma on them whose images are the four labelled local invariant +half-branches. The map f -> Gamma_f^sigma is continuous U->C^1, and C^1 after +possibly shrinking U. The graph parameter, not physical flow time at p(f), is +used at the stationary endpoint. + +**A2.3 local-section launch.** If a fixed finite section is transverse to the +chosen germ at an interior point, its first robust closed-section hit, under the +R1 hypotheses of #135, depends continuously on f; under A2.2 C^1 dependence it +is C^1 by the scalar implicit-function theorem. + +**A2.4 regular finite flow.** Let z(f) be such a C^1 launch point and suppose a +compact finite trajectory segment stays in a coordinate region on which +|V_f|>=eta>0. For every fixed finite time horizon before leaving that region, +Phi_f^t(z(f)) is C^1 jointly in (f,t). Its field derivative u=D_f Phi_f^t(z)[h] +satisfies the variational equation + u'=H_f(Phi_f^t)u + grad h(Phi_f^t), +with the corresponding initial derivative. Consequently any transverse robust +first hit along this finite segment is C^1 in f. + +These statements are local. They do not prove A3-A4, Gaussian genericity, +global connection absence, or any C103 estimate. + +## 2. Why C2 is the right field topology + +The linear map f -> V_f=grad f is bounded C^2->C^1. Evaluation +(f,x)->V_f(x) is C^1 from X x T^2 to R^2: its field derivative is grad h(x) +and its spatial derivative is H_f(x), continuous because f is C^2. Therefore +the Banach implicit-function theorem proves A2.1 directly. + +For finite regular flow, write the integral equation + x(t)=z + integral_0^t V_f(x(s)) ds. +On a compact coordinate region, V_f and D_x V_f are uniformly bounded and +continuous in f in the C^1 norm. Standard contraction on short time slabs gives +existence and continuous dependence. Differentiate the fixed-point equation in +the Banach parameter f. The derivative is the unique solution of the displayed +linear variational equation. Concatenating finitely many slabs proves A2.4 on a +fixed finite horizon. No derivative of H_f is used; C^2 field regularity is +therefore sufficient for this finite-flow part. + +## 3. Local invariant graph by a parameter-dependent contraction + +Translate p(f) to zero and use a continuously chosen orthonormal eigenframe of +the symmetric Hessian H_f(p(f)); the simple positive/negative eigenvalues remain +separated after shrinking U. In coordinates (x,y), write + V_f(x,y)=(lambda_f x, -mu_f y)+N_f(x,y), +where lambda_f,mu_f>=lambda_*>0 and N_f(0)=DN_f(0)=0. The map +f -> (lambda_f,mu_f,N_f) is C^1 into the natural C^1 coefficient space: the +eigenvalues/eigenprojections of a simple symmetric 2x2 matrix are C^1, and the +coordinate change and p(f) are C^1. + +Choose a small radius so sup ||DN_f|| is uniformly below a fixed fraction of +lambda_*. The usual graph transform on C^1 graphs y=g(x), g(0)=g'(0)=0, is then +a uniform contraction on a closed C^1 ball. Importantly, its contraction +constant is <1 uniformly in f. The transform is C^1 in (f,g): it is assembled +from V_f, finite local flow, coordinate projections and inverses whose +derivatives stay uniformly nonzero on this small ball. + +The fixed point g_f therefore depends C^1 on f. A direct proof avoids importing +a differentiable fixed-point theorem: from g_f=T(f,g_f), + [g_{f+h}-g_f]/||h|| +is Cauchy because the difference quotient equals the parameter difference +quotient of T plus a contraction applied to the graph difference quotient. +Taking the limit gives + Dg_f[h]=(I-D_g T(f,g_f))^{-1} D_f T(f,g_f)[h], +where the inverse is the convergent Neumann series since ||D_gT||<1. +Continuity of these derivatives follows from continuity of DT and the same +uniform contraction bound. The unstable graph is obtained by applying the same +argument to reversed time. Restricting x to positive or negative compact +subintervals gives the labelled half-branches and proves A2.2. + +This argument uses C^1 graph transforms, not a claim that an arbitrary C^1 +vector field has C^2 invariant manifolds. The output required downstream is +only a C^1 arc with C^1 dependence on the C^2 field parameter. + +## 4. Hitting maps + +Let Gamma(f,s) be any local germ or regular-flow arc already proved C^1 in +(f,s), and let a finite section be rho=0 with d rho(Gamma_s) nonzero at the +first robust hit. The R1 geometry in #135 supplies an open neighborhood on +which that zero remains the first closed contact. The Banach scalar IFT gives +a C^1 hit parameter tau(f), with + D tau(f)[h]= -D_f(rho o Gamma)(f,tau)[h] + / partial_s(rho o Gamma)(f,tau). +Composition gives the C^1 hit point. This proves exactly the differential part +of A2-D once R1 supplies the robust first-contact predicate. + +## 5. Scope and review target + +The only non-elementary local ingredient above is the uniform C^1 graph +transform. A reviewer should check that its chosen graph space and transform +really are C^1 in the Banach parameter when f is only C^2, and that no hidden +third derivative of f is used. The finite-flow argument needs only H_f +continuous; the local invariant graph uses the C^1 vector field V_f and its +C^1 parameter dependence. + +No literature priority claim is made. Consensus search was attempted on +2026-09-29 and returned the monthly quota error; no result is fabricated from +that call. This note is intended to discharge the precise imported A2-T/A2-D +interface after independent review, not to promote SARD-G by itself. diff --git a/frontiers/sard_g_a2_parameter_20260929/README.md b/frontiers/sard_g_a2_parameter_20260929/README.md new file mode 100644 index 000000000..c53bde904 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/README.md @@ -0,0 +1,21 @@ +# SARD-G A2: corrected successor and explicit predecessor withdrawal + +**The original PROOF.md is a noncontrolling, invalid predecessor at its Section 3 +and C1-into-C1 claim. Do not consume it as A2 discharge.** Its exact original bytes +are preserved for audit, as are its four illustrative finite tests. + +The replacement is [v2/README.md](v2/README.md). It proves the necessary joint C1 +evaluation/continuous-C1-arc interface using a fixed-frame C0 trajectory contraction, +not a differentiable moving eigenframe. The explicit counterexample and author +correction are in [v2/AUTHOR_CORRECTION.md](v2/AUTHOR_CORRECTION.md). + +The new companion supplies localized scalar-potential nonvanishing, a full-support +Fourier argument, mesh genericity, and a qualitative unconditioned planar no-saddle- +connection composition. All are new author-side claims requiring nonauthor review. +No C103 regional estimate, conditioned-field theorem, RN/JETMOD, 3D or registry +advancement is implied by publication or finite checking. + + python -B -S v2/verify.py --output /path/to/new-output + +The new manifest and finite tests are confined to v2 and cannot launder the old +invalid argument into a passing mathematical verdict. Scientific effect NONE. diff --git a/frontiers/sard_g_a2_parameter_20260929/check.py b/frontiers/sard_g_a2_parameter_20260929/check.py new file mode 100644 index 000000000..4fa5db865 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/check.py @@ -0,0 +1,43 @@ +"""Finite illustrations of the A2 parameter formulas; not a stable-manifold proof.""" +import unittest +from fractions import Fraction as F + +def tracked(a,b,c): # grad f=(a*x+b, -c*y), a,c>0 + return (-F(b,a), F(0)) + +def tracked_derivative(a, db): + return (-F(db,a), F(0)) + +def flow_derivative(a,t,x0,h): # x'=a x + eps*h*x? derivative at eps=0 + # for integer t=1 only in exact checker: u(1)=h*x0*e^a is not rational; + # use constant forcing x'=a x + eps*h, t symbolically via coefficients. + return F(h,a) # equilibrium derivative of -eps*h/a, sign handled by equation + +class A2(unittest.TestCase): + def test_implicit_saddle_derivative(self): + a,c=F(3),F(5) + for b in (F(-2),F(0),F(7,4)): + p=tracked(a,b,c) + eps=F(1,1000); db=F(7,3) + dq=((tracked(a,b+eps*db,c)[0]-p[0])/eps,F(0)) + self.assertEqual(dq,tracked_derivative(a,db)) + def test_graph_parameter_at_stationary_point(self): + # unstable branch y=0 is parameterized by x=s, including s=0; + # its derivative in s is nonzero although physical vector field vanishes at s=0. + for s in (F(0),F(1,10),F(-1,10)): + gamma=(s,F(0)); dgamma=(F(1),F(0)) + self.assertEqual(dgamma,(1,0)) + if s==0:self.assertEqual((3*s,-5*gamma[1]),(0,0)) + def test_transverse_hit_formula(self): + # Gamma(eps,s)=(s+eps, s); section rho=x-1. + eps=F(1,1000) + tau0=F(1); tau1=1-eps + self.assertEqual((tau1-tau0)/eps,-1) + def test_variational_forcing_sign(self): + # x'=-a x + eps*h has equilibrium x=eps*h/a. + a,h=F(7),F(3) + eps=F(1,1000) + xeq=eps*h/a + self.assertEqual(xeq/eps,h/a) + +if __name__=="__main__": unittest.main() diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/A2_FIXED_FRAME.md b/frontiers/sard_g_a2_parameter_20260929/v2/A2_FIXED_FRAME.md new file mode 100644 index 000000000..09c45efbd --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/A2_FIXED_FRAME.md @@ -0,0 +1,261 @@ +# A2 at C2: fixed-frame bounded trajectories, not a differentiable C1 graph transform + +Object: OA-SARD-A2-FIXED-FRAME-20260929-v2. +Author: OpenAI / ChatGPT. Status: AUTHOR-SIDE SUCCESSOR; nonauthor analytic review required. +Scientific effect NONE. The original #137 manuscript remains a historical, +noncontrolling predecessor; its moving-eigenframe/C1-into-C1 claim is withdrawn. + +## 1. The exact target and the false stronger claim + +Put X=C^2(T_L^2) with its usual Banach norm, and V_f=grad f. Fix a reference field +f_* in X and a nondegenerate saddle p_*. All assertions are LOCAL on a sufficiently +small X-neighborhood U of f_*. There are four labelled local branch germs, with +fixed compact graph-parameter intervals, for which: + +(T) f -> Gamma_f is continuous into C^1 arcs; +(D) (f,s) -> Gamma_f(s) is jointly Frechet C^1 into the surface; +(B) for fixed s, |D_f Gamma_f(s)[h]| <= C ||h||_{C^1}. + +Finite regular flow, robust local-section launches, and robust central hits have +the same joint differentiability and local derivative bounds. In particular the +scalar mismatch D_chi is Frechet C^1 on every robust chart from [RC-S], with +|D D_chi(f)[h]| <= C_chi,f ||h||_{C^1}; its derivative is continuous in operator +norm on X*. It therefore also supplies Claude's weaker line form A2-G in [CL]. + +(D) DOES NOT assert that f -> Gamma_f is differentiable into the C^1 arc norm. +That extra derivative is not needed by the hitting IFT or the Gaussian slicing. +[RC-S] A2-D is read literally as joint C^1 evaluation; graph axes are fixed with +the atlas neighborhood, not recomputed from a moving Hessian. This specifies the +previously ambiguous graph-coordinate sentence without changing the geometry. + +The original #137 Section 3 incorrectly claimed that H_f(p(f)), its eigenframe, +and its recentered nonlinearity are C^1 in the necessary strong norms for f in C^2. +They need not be. Here is a concrete counterexample in a coordinate ball, with a +fixed smooth cutoff equal to one near zero: + + f_t(x,y)=(x^2-y^2)/2 +(2/3)xy(x^2+y^2)^(1/4) + -t x -(2/3)t|t|^(1/2)y. (F1) + +The homogeneous nonpolynomial term has degree 5/2, is C^2, and its second +derivatives tend to zero at zero. The map t -> f_t is C^1 into C^2. The saddle +p_t=(t,0) has Hessian + + H_{f_t}(p_t)=[[1,sqrt(|t|)],[sqrt(|t|),-1]]. (F2) + +Its positive eigenline has slope + + m(t)=sqrt(|t|)/(1+sqrt(1+|t|)). (F3) + +For 0=1/(3 sqrt(t)), so it is not differentiable at zero. A fixed-x +graph of the local unstable manifold, anchored at p_t, has derivative m(t) at its +anchor. Differentiability into C^1 arcs would imply differentiability of that +slope, which is false. Periodization is harmless because all calculations are +inside the cutoff-one ball. This example refutes the old proof's strong regularity, +not the joint C^1 evaluation target (D). No C^3 assumption will be inserted to +hide the issue. + +## 2. Tracked saddle and fixed coordinates + +The map (f,x) -> grad f(x) is jointly C^1, with + + D[grad f(x)][h,z]=grad h(x)+H_f(x)z. (F4) + +For example its remainder is bounded by +omega_{H_f}(|z|)|z|+||h||_{C^2}|z|. Continuity of the derivative in operator norm +uses uniform continuity of H_f and +sup_{||h||C2<=1}|grad h(x)-grad h(y)|<=C|x-y|. This agrees with [CL] Lemma J. +The Banach IFT therefore gives the unique nearby saddle p(f), with + + Dp(f)[h]=-H_f(p(f))^{-1} grad h(p(f)). (F5) + +We USE the derivative of p, but we do NOT differentiate H_f(p(f)). Its continuity +suffices for the local inverse bound. Choose the origin p_* and an orthonormal +eigenframe of H_{f_*}(p_*) ONCE. In these fixed coordinates + + A=diag(lambda,-mu), lambda,mu>0, + V_f(x)=A x+R_f(x), (F6) + +where R_f=V_f-Ax. The saddle p(f) is not translated out of the vector field. +In particular R_f(0) is usually nonzero and must be retained. + +## 3. A fixed compact cutoff with a uniformly small Lipschitz constant + +Let chi be a fixed smooth cutoff equal to one on the ball B_a and zero outside +B_{2a}, in a coordinate ball contained in the declared endpoint neighborhood. +Set + + N_f(x)=chi(x)(V_f(x)-Ax), (F7) + +and extend by zero to R^2. This need not be a gradient vector field outside B_a; +all local trajectories used below remain in B_a, where it is the original field. +The map f -> N_f is affine and bounded C^2->C^1 on this fixed coordinate region. +The functions N_f and DN_f are globally bounded; DN_f is uniformly continuous +for each fixed f. There is no moving cutoff or moving-coordinate derivative. + +Given epsilon>0, first choose a small a so ||DV_{f_*}-A||<=epsilon on B_{2a}. +Then ||R_{f_*}(x)||<=epsilon|x| there. If ||f-f_*||C2<=delta, + + ||DN_f||_infinity <= C_chi(epsilon+delta/a+delta), (F8) + +by the product rule. Thus by choosing a and THEN delta sufficiently small, +we may arrange ||DN_f||<=ell with ell as small as desired, uniformly on U. +Also ||N_f(0)||<=C delta. All constants below use an adapted max norm on the +fixed stable/unstable factors; projections have norm one. + +Choose beta with 0N_f(x(.)) really IS C^1 into E_0. Its +variation is + + (h,z(.)) -> chi(x(.)) grad h(x(.))+DN_f(x(.))z(.). (F12) + +For the x part, the uniform remainder is at most +omega_{DN_f}(||z||infinity)||z||infinity. The mixed f/x remainder is at most +C||h||C2 ||z||infinity. The parameter derivative is continuous in operator norm +because, uniformly on ||h||C2<=1, chi grad h is Lipschitz; DN_f changes uniformly +under C^2 field changes. A compact fixed cutoff ensures these estimates also +hold for trajectories outside the local ball. Hence T is genuinely C^1 on +U x R x E_0; no spatial derivative of DN_f is differentiated. + +Banach IFT applied to x-T(f,a_0,x), or the differentiable-contraction argument, +now proves (f,a_0)->x_{f,a_0} is jointly Frechet C^1 into E_0. Its derivative z +in direction (h,da_0) is the unique bounded solution + + z=(exp(lambda t)da_0,0) + +K[chi(x(.))grad h(x(.))+DN_f(x(.))z(.)]. (F13) + +In particular + + ||z||infinity <= (|da_0|+C_0 C_chi||h||C1)/(1-theta_0). (F14) + +The inverse I-K DN_f is its norm-convergent Neumann series. This is the correct +fixed-point differentiability argument, in a C^0 trajectory norm, replacing the +unproved C^1-graph-transform assertion. The time interval is infinite but the +paths are bounded and DN_f is uniformly continuous, so no exponentially growing +Nemytskii domain is being differentiated. + +## 5. Localization, convergence to the moved saddle, and full-germ coverage + +The fixed point estimate gives + + ||x_{f,a_0}||infinity + <= (|a_0|+C_0||N_f(0)||)/(1-theta_0). (F15) + +Choose |a_0| and U small enough that this is strictly below a/2. The entire +backward trajectory then stays where chi=1 and is a trajectory of V_f. It is +not an artefact of the cutoff. + +Let p=p(f) and a_p=P_u p. The constant path p is the fixed point of (F11) for +a_0=a_p, since Ap+N_f(p)=0. Subtracting this constant path gives the equation + + y=(exp(lambda t)(a_0-a_p),0)+K[N_f(p+y)-N_f(p)]. (F16) + +For THIS existence comparison only, use E_beta with norm +sup_{t<=0} exp(-beta t)|y(t)|. The elementary two integral estimates give the +bound C_beta in (F9), so (F16) has a unique fixed point in E_beta, satisfying + + ||y||beta <= |a_0-a_p|/(1-theta_beta). (F17) + +This fixed point also belongs to E_0 and solves (F16) there; E_0 uniqueness +identifies it with x_{f,a_0}-p. Thus x(t)->p exponentially as t->-infinity. No +differentiability in E_beta is invoked. In particular we never differentiate +the moving p inside DN_f or an exponentially weighted composition operator. + +Conversely, any backward trajectory of the original V_f that stays in the small +ball is bounded. Variation of constants gives (F10)-(F11): the stable homogeneous +term from a time -T disappears as T->infinity because the trajectory is bounded. +The unstable part uses its value at zero. By uniqueness it is one of our graphs. +This proves that the construction gives the full local unstable germ, not a +selected orbit or an arbitrary continuously chosen curve. Reversing time proves +the stable germ, with the roles of lambda and mu interchanged. + +Define the anchored graph parameterization by + + Gamma_f(s)=x_{f,a_p(f)+s}(0), |s|<=s_*, (F18) + +on a compact interval with strict smallness slack. Its unstable projection is +a_p(f)+s, so partial_s Gamma is nonzero and it is embedded. Gamma_f(0)=p(f). +Formulae (F5),(F13) prove joint C^1 evaluation (D) and the C^1 perturbation bound +(B). Joint continuity of partial_s Gamma, uniform on compact s-intervals, proves +f->Gamma_f is CONTINUOUS into C^1 arcs. We do not differentiate partial_s Gamma +in f. Restrict s to either sign for the two half-branches. Fixed frame plus +fixed sign labels produce the four branches needed by [RC-S]. + +The construction is localized: if h vanishes on the endpoint neighborhood that +contains the cutoff and subsequent local arc, then N_{f+th}=N_f there and all +local branch launches are identical. A germ may be propagated to any declared +nearby local section by a finite flow inside that neighborhood; the same locality +holds. This is the endpoint-support fact needed by the companion proof. + +## 6. Finite flows, robust sections, and mismatch derivatives + +On each compact finite-time region, the integral equation +Phi_f(t,z)=z+integral_0^t V_f(Phi_f(s,z)) ds is a contraction on sufficiently short +time slabs. Its Nemytskii map in the C^0 path norm is C^1 by (F4). The same IFT +argument and concatenation of finitely many slabs give jointly C^1 dependence +in (f,z,t), with continuous derivatives. The field variation satisfies + + w'=H_f(Phi_f)w+grad h(Phi_f), (F19) + +with initial derivative if z=z(f). Gronwall bounds it by C||h||C1. There is no +need for positive speed merely to solve or differentiate this ODE; positive speed +is required on the finite regular arcs used for transverse hits and chart margins. +Physical flow starting exactly at the saddle is stationary; (F18), not that flow, +parameterizes the local germ across its anchor. + +For a fixed section rho=0 and a robust transverse hit at parameter tau, [RC-S] R1 +ensures the nearby zero stays the FIRST contact with the CLOSED section. Joint +C^1 evaluation and the scalar IFT give + + Dtau(f)[h]=-D_f[rho(Gamma(f,tau))][h]/partial_s[rho(Gamma(f,tau))]. (F20) + +The transverse denominator is bounded away from zero on a smaller neighborhood. +This gives the required derivative bounds for launches, central hits, and +D_chi=s(z_u)-s(z_s). Applying it to EVERY local and central section supplies the +literal A2-T and joint A2-D hypotheses of [RC-S], with graph coordinates fixed +once per atlas chart. The same reasoning yields A2-G and its bound for [CL]. + +A2-G alone supports the reduced slicing application, but does not by logical +implication prove an arbitrary stronger Frechet statement. Here joint Frechet +C^1 was proved separately by (F11)-(F14); no Gâteaux/Frechet identification is +being made from the line theorem alone. + +## 7. Interface disposition and remaining use + +This is an author-side full argument for the precise A2 interface. [CL]'s Lemma J, +regularity diagnosis and weaker-use observation are credited. Its center-manifold +citations are not imported as unverified substitutes: the hyperbolic construction +above is displayed in full, including cutoff smallness, forcing, differentiability, +decay and complete local-germ identification. + +No false C^1-into-C^1 conclusion remains in this successor. The companion manuscript +supplies a new A3/A4 route, the generic full-measure argument, and a qualitative +planar no-connection composition. The robust first-contact geometry still has the +exact [RC-S] source/review lineage. A nonauthor review must evaluate these actual +arguments, not infer them from the finite scalar checks or the previously merged +R3/R4 conditional review. No C103 bound, RN/JETMOD, 3D theorem, numerical constant, +scientific-status transition, or claimed historical novelty is included. diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/AUTHOR_CORRECTION.md b/frontiers/sard_g_a2_parameter_20260929/v2/AUTHOR_CORRECTION.md new file mode 100644 index 000000000..1f72865b3 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/AUTHOR_CORRECTION.md @@ -0,0 +1,24 @@ +# Author correction to Math-#137 v1 + +The original PROOF.md at e944ba0b595d790d27d1466cc4f576467890bc3a is NOT an accepted +proof of A2.2 or Section 3. Its claim that a moving Hessian/eigenframe and a +recentered C1 graph transform are C1 in a C2 field parameter is invalid without +additional arguments/regularity. Claude's #138 correctly identified this issue. +The preceding assistant explanation repeated that unsupported claim; it is +withdrawn here, not merely relabelled as needing a routine check. + +The explicit C2 gradient counterexample (F1)-(F3) in A2_FIXED_FRAME.md disproves +the C1-into-C1 strengthening. The tracked-saddle and finite-flow formulas remain +valid. The old four finite illustrations never verified the invalid analytic step. + +This additive v2 preserves all original files in Git history and as predecessor +files in the branch. Its claims are different and narrower: joint C1 evaluation, +not C1 dependence into C1 arcs; continuous C1 arc dependence is proved separately. +The actual fixed-point map on bounded C0 trajectories is displayed and its +Nemytskii differentiability justified. Only a decay comparison uses weighted +spaces; no weighted differentiability is assumed. + +The extension to A3/A4 and genericity is new author-side work. It must receive +its own source-bound analytic review; the merged R3/R4 review cannot discharge +its newly supplied premises retroactively. No original proof or review verdict, +scientific register, lemma flag, prize, RN/JETMOD or C103 status is altered here. diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/NONVANISHING_AND_CLOSURE.md b/frontiers/sard_g_a2_parameter_20260929/v2/NONVANISHING_AND_CLOSURE.md new file mode 100644 index 000000000..7da6a393c --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/NONVANISHING_AND_CLOSURE.md @@ -0,0 +1,291 @@ +# Localized forcing, full Fourier support, and the qualitative planar SARD-G conclusion + +Object: OA-SARD-NONVANISHING-CLOSURE-20260929-v1. +Author: OpenAI / ChatGPT. Status: AUTHOR-SIDE PROOF; nonauthor review required. +Scientific effect NONE. This is not a quantitative or regional C103 certificate. + +## 1. Exact scope and conclusion + +On the fixed flat torus T_L^2, consider the centered variance-one Gaussian field +with covariance + + K_L(x-y)= [sum_{m in Z^2} exp(-|x-y+Lm|^2/2)] + / [sum_{m in Z^2} exp(-|Lm|^2/2)]. (N1) + +All constants and neighborhoods in this manuscript are local/existential for +fixed L. Use ascending gradient flow x'=grad f; reversing its sign exchanges +stable and unstable conventions without changing the no-connection event. + +**Theorem S (qualitative planar no-connection candidate).** Almost surely the +field has finitely many nondegenerate critical points, with distinct critical +values, and no gradient trajectory connects two different index-one saddles. +Precisely, the connection event has outer Gaussian measure zero and is null in +the completed Gaussian probability space. This does not assert in advance that +the uncompleted connection event itself is Borel. + +The proof assembles: the ACTUAL first-closed-contact charts of [RC-S] (not the +old endpoint-admitting predicate); the corrected joint C^1 regularity proved in +A2_FIXED_FRAME.md; the explicit interior perturbation in Sections 2-4 below; +full Fourier support; and the mesh/genericity and countable Gaussian slicing +arguments in Sections 5-7. No A2, A3/A4 or genericity black-box assumption remains +inside this new composition. The source-level R1/R2 geometry is consumed at its +pinned proof, with its separate review status retained. This is an author-side +composition pending review, not a canonical advancement of the old SG source. + +The theorem is unconditioned. It does not apply a full-support proof to a +coalescing pair-conditioned field, and gives no bound uniform under conditioning. +There is no 3D Morse-Smale conclusion, no regional intensity, no RN/JETMOD claim, +no numerical probability of a near-connection, and no new quantitative C103 gate. + +## 2. An interior perturbation cannot be canceled by endpoint variation + +Fix a zero of a robust chart: a genuine saddle connection from p to q, with its +unstable and stable launches in disjoint endpoint neighborhoods. Along its compact +regular arc write gamma(t), 0<=t<=T, with central first section hit at t=c in (0,T). +By uniqueness and strict increase of f, the arc is embedded. Pick t_0 in (0,c), +strictly after the unstable launch. A small coordinate neighborhood O of gamma(t_0) +can be chosen disjoint from both endpoint neighborhoods and from the entire +stable travel half gamma([c,T]); it meets the remaining trajectory only inside +a small time interval J compactly contained in (0,c). + +Why O exists matters. An embedded compact arc is a homeomorphism onto its image. +Remove a small open parameter interval around t_0; its remaining compact image +is disjoint from a smaller compact subarc. Their distance is positive. Choose +O inside that separation, small enough for a local coordinate graph. This rules +out hidden returns through the support of the perturbation. + +Let h in C^2 be supported in O. The original vector field and every endpoint local +germ are unchanged near their entire defining endpoint neighborhoods. The fixed +cutoff construction in A2_FIXED_FRAME.md, followed by local finite flow, makes +both launch points EXACTLY unchanged for f+epsilon h. The stable travel half and +its central hit are also unchanged, since the field is unchanged on a neighborhood +of that half. The unstable variation w therefore satisfies + + w'=H_f(gamma(t))w+grad h(gamma(t)), w(0)=0, 0<=t<=c. (N2) + +Let Sigma have unit normal n and unit tangent tau, and V_c=grad f(gamma(c)). +Transversality means n.V_c!=0. Correction for the moving hit time projects the +fixed-time variation by + + Pi=I-V_c n^T/(n.V_c). (N3) + +The mismatch coordinate is the signed tangent coordinate, so its derivative is + + L_f(h)=tau^T Pi w(c). (N4) + +In particular endpoint-supported derivative terms have not been ignored; they +vanish for THIS specially supported perturbation by exact localization. +For general h the joint C^1 regularity gives a bounded linear derivative L_f on +X with |L_f(h)|<=C||h||C1. Only the supported perturbation is needed to prove it +is nonzero. No formula claiming endpoint variation is a finite list of two-jets +is asserted. + +## 3. The covector calculation and a concrete potential perturbation + +Let Phi(t,s) be the fundamental matrix of w'=H_f(gamma(t))w. Define + + b_c=Pi^T tau, b(t)=Phi(c,t)^T b_c. (N5) + +Pi fixes the tangent tau, so b_c.tau=1 and b_c!=0. Also b_c.V_c=0 because Pi V_c=0. +Invertibility of Phi gives b(t)!=0. The adjoint identity is + + b'=-H_f(gamma(t))^T b, b(t).grad f(gamma(t))=0. (N6) + +The last equality follows by differentiating the pairing; the vector grad f +along the orbit solves V'=H_f V. Duhamel now gives + + L_f(h)=integral_0^c b(t).grad h(gamma(t)) dt. (N7) + +It remains to choose h as a SCALAR POTENTIAL, not an arbitrary vector forcing. +In a fixed local Euclidean coordinate rotation, the regular C^2 trajectory is +a C^2 graph y=g(x) on O, with x(t) strictly monotone. Since b is perpendicular +to its tangent, on a smaller interval it has the form + + b(t)=a(t)(-g'(x(t)),1), + +where a is continuous, nonzero, and of constant sign. Choose a nonnegative C^2 +function phi supported strictly inside that x interval, not identically zero, +and a smooth transverse cutoff zeta equal to one near zero. Set + + h(x,y)=sign(a) phi(x)(y-g(x)) zeta(y-g(x)). (N8) + +The rectangle and cutoffs are small enough that h is supported in O; extend it +by zero globally. It is C^2. Along the orbit its gradient is +sign(a) phi(x)(-g'(x),1), so + + b(t).grad h(gamma(t))=|a(t)| phi(x(t))(1+g'(x(t))^2)>=0, + +with a strictly positive integral. Thus L_f(h)>0. This explicitly proves +nonvanishing at every robust connection using only C^2 regularity. If a smooth +h is desired, approximate this compactly supported C^2 function in C^2 inside +O by smooth functions; continuity of L_f preserves strict positivity. + +The construction is field-dependent only as an EXISTENCE witness for L_f!=0. +It is not selected measurably and is not itself used as a random Gaussian shift +direction. Countably many deterministic Fourier directions are chosen next. + +## 4. From a local bump to a deterministic Cameron-Martin direction + +Poisson summation gives Fourier weights + + a_n=[2pi/(L^2 Z_L)] exp(-2pi^2 |n|^2/L^2)>0, + Z_L=sum_m exp(-|Lm|^2/2), sum_n a_n=1. (N9) + +Every real trigonometric polynomial therefore belongs to the Cameron-Martin +space H: its RKHS norm is a FINITE sum of squared Fourier coefficients divided +by positive a_n (with the corresponding real-mode convention). Such polynomials +are dense in C^2. One direct proof uses periodic smoothing followed by Fourier +truncation of the smoothed function, or product Fejer means applied also to each +of the continuous derivatives of orders <=2. + +Since L_f is continuous on C^2 and is nonzero on (N8), it cannot vanish on all +trigonometric polynomials. By linearity it is nonzero on at least one individual +real Fourier mode. These modes all lie in H. This proves the A3/A4 nonvanishing +interface WITHOUT differentiating an RKHS kernel or representing every endpoint +variation by distributions. Positivity of EVERY Fourier weight is essential; +a band-limited or otherwise restricted spectrum is not covered by this argument. + +It also verifies compatibility with [RC-S] R3: a nonzero continuous L_f|H is +nonzero on its countable evaluation-image family. Thus one may use its already +written Gaussian decomposition. Section 7 instead gives a simpler equivalent +Fourier-coordinate decomposition for this particular periodic model. + +## 5. Smooth sample paths and finite-jet covariance floors + +Choose one representative n in each pair {n,-n}, n!=0. An exact real realization is + + f(x)=sqrt(a_0)Z_0+sum_{n+}sqrt(2a_n) + [Z_n^c cos(2pi n.x/L)+Z_n^s sin(2pi n.x/L)], (N10) + +with independent standard real Gaussians. For every integer k, + + sum_n sqrt(a_n)(1+|n|)^k E|Z_n| < infinity. + +Tonelli gives almost-sure absolute uniform convergence of all derivative series +through order k; a countable intersection in k gives smooth paths. Their C^k +norms also have finite fixed moments by the corresponding sum/Minkowski bound. +This realization has covariance (N1); its C^2-valued law is the Gaussian law used +in [RC-S]. No finite Fourier truncation is substituted for the exact field. + +Any finite set of distinct derivative functionals at one point is linearly +independent as distributions when symmetric duplicates are removed. The same +holds for gradients at two distinct points together with their value difference: +use test functions supported separately near the two points to isolate each +coefficient. If a linear combination had zero variance, positivity of all a_n +would force it to vanish on every Fourier mode. It would then vanish as a +finite-order distribution, by Fourier approximation of smooth tests, contrary +to independence. Hence its covariance is positive definite. + +In particular (grad f,H_f) at one point is a nondegenerate five-dimensional +Gaussian vector. Also + + (grad f(x),grad f(y),f(x)-f(y)) (N11) + +is nondegenerate for x!=y. Covariance varies continuously with the points, so +on dist(x,y)>=epsilon its smallest eigenvalue has a positive minimum. Gaussian +densities are therefore uniformly bounded on that compact separated set. These +floors are qualitative for each fixed separation; no uniform lower floor as +x->y is claimed or needed here. + +## 6. Two elementary mesh arguments establish the full-measure generic set + +This supplies the genericity input explicitly, not through an unverified claim +that every field along a Gaussian shift line is generic. + +### 6.1 Morse critical points + +Localize to ||f||C3<=M. If grad f(x)=0 and det H_f(x)=0, at a mesh point x_delta +within C delta one has |grad f(x_delta)|<=C_M delta, +||H_f(x_delta)||<=C_M, and |det H_f(x_delta)|<=C_M delta. There are O(delta^-2) +mesh points. For a symmetric matrix [[a,b],[b,c]] in a bounded box, the volume of + + |ac-b^2|<=epsilon (N12) + +is O_M(sqrt(epsilon)). Indeed split |a|<=sqrt(epsilon), which has volume +O_M(sqrt(epsilon)), from |a|>sqrt(epsilon), where at each fixed a,b the permitted +c interval has length at most 2epsilon/|a|<=2sqrt(epsilon). This rough bound is +sufficient even near the double-zero matrix. + +The joint five-variable density bound from Section 5 gives probability +O_M(delta^2 sqrt(delta)) per mesh point. The union bound gives O_M(sqrt(delta)), +which tends to zero along any sequence of refining meshes. The bad event is +contained in every such mesh union, so it has probability zero on ||f||C3<=M. +Take a countable union over M. Nondegenerate zeros of grad f are isolated; +compactness then makes their number finite. + +### 6.2 Distinct critical values + +Fix separation epsilon>0 and localize to ||f||C2<=M. If two separated critical +points have equal values, (N11) at a nearby mesh pair has norm <=C_M delta. +For small delta the pair remains separated by epsilon/2. There are O(delta^-4) +mesh pairs. The five-dimensional Gaussian density bound gives probability +O_{M,epsilon}(delta^5) for each, and hence O_{M,epsilon}(delta) for the union. +Let delta->0, then take the countable union over M and separations epsilon=1/n. +Every distinct pair has some positive separation, so almost surely all critical +values are distinct. + +The relevant events can be formulated by minima of continuous functions on compact +sets at fixed norm/separation bounds; alternatively the mesh unions supply Borel +null supersets directly. This is enough for the completed-measure conclusion. +There is no reliance on a sampled gradient minimum as a certified continuum bound. + +## 7. Countable Fourier slicing closes the qualitative connection event + +Use the robust charts of [RC-S] with fixed-frame branch parameterizations from +A2_FIXED_FRAME.md. The chart domains are open in C^2, form a countable family, +and cover every nondegenerate connection. Their mismatches D_chi are jointly +constructed and Frechet C^1. At every connection zero their derivative is +nonzero on some deterministic real Fourier mode by Sections 2-4. + +For a mode let h_j be its function in the expansion (N10), INCLUDING its standard- +Gaussian scale sqrt(a_0) or sqrt(2a_n). Its Fourier coefficient xi_j is standard +normal, and the residual g_j=f-xi_j h_j is independent of xi_j. One can check +this from the independent series, or by vanishing cross-covariances and the +Gaussian characteristic functional. Subtracting one smooth mode leaves a +C^2-valued residual. All modes are countably indexed. The constant mode has +zero mismatch derivative, but at least one nonconstant mode is nonzero. + +For fixed chi,j let + + B_chi,j={f in U_chi: D_chi(f)=0, D D_chi(f)[h_j]!=0}. (N13) + +This is Borel because U_chi is open and both scalar maps are continuous. For +EVERY fixed residual g, the validity set I_g={t:g+t h_j in U_chi} is open. The +function t->D_chi(g+t h_j) is C^1 there. Each zero counted in (N13) has nonzero +derivative, hence is isolated among all zeros on its validity interval. The +regular zeros are countable: each has a rational-endpoint interval containing +no other zero. Accumulation at singular zeros or interval boundaries is allowed. + +Independence and Tonelli therefore give mu(B_chi,j)=0, since the scalar Gaussian +charges no countable set. The union over chi,j is a Borel null set containing all +nondegenerate connections. Section 6 supplies a full-measure set of Morse fields +with distinct critical values. The connection event is thus outer-null and null +in the completion. A self-connection is excluded separately by strict increase +of f along every nonconstant gradient trajectory. This proves Theorem S as a +qualitative source-level composition. + +An equivalent ending applies [RC-S] R3/R4 after supplying A2-D and A3/A4 from this +packet and genericity from Section 6. We wrote the mode argument to show that the +concrete periodic theorem does not need any norm-separable Banach dual, abstract +measurable chart selector, or assertion about all shifted fields being Morse. + +## 8. What this resolves mathematically, and what it does not authorize + +The packet supplies explicit source arguments for local parameter regularity, +nonzero Cameron-Martin variation, the full-measure generic set, and their actual +composition with the robust first-contact predicate. It avoids proving the false +strong C1-into-C1 statement and does not attempt to repair it by enlarging the +field norm to C3, changing the Gaussian law, or allowing an endpoint hit. + +The original SG/BR/RI and conditional [RC-S] reviews remain historical evidence. +A nonauthor review of A2, of the localized-forcing/Fourier argument, and of this +assembly is still needed before any canonical downstream status fold. In particular +Theorem S is not a new regional Kac-Rice estimate, does not prove a deterministic +normalizer floor on a numerical interval, and does not settle conditioned SARD-G, +RN/JETMOD, P0.1 or any 3D claim. Such consumers must expose the exact measure and +object they use rather than treating an unconditioned null set as universally null. + +The methods are classical contraction, variation of constants, Fourier support, +mesh bounds and Gaussian slicing. No historical-priority or exhaustive novelty +claim is made. Finite tests check selected exact identities and logical exclusions; +they are not proofs of the infinite-dimensional or measure-theoretic statements. diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/README.md b/frontiers/sard_g_a2_parameter_20260929/v2/README.md new file mode 100644 index 000000000..82404a159 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/README.md @@ -0,0 +1,33 @@ +# Targeted SARD-G completion candidate + +**Author-side successor; nonauthor analytic review required. Scientific effect NONE.** + +[A2_FIXED_FRAME.md](A2_FIXED_FRAME.md) replaces the invalid moving-eigenframe and +C1-into-C1 assertions of #137 v1. It proves only what the downstream proof uses: +joint Frechet C1 evaluation, continuous C1 arc dependence and local derivative +bounds. It uses fixed-origin/splitting bounded trajectories; a separate weighted +argument proves decay but is not differentiated. + +[NONVANISHING_AND_CLOSURE.md](NONVANISHING_AND_CLOSURE.md) supplies an explicit +interior scalar-potential perturbation, a Fourier-density route to a nonzero +Cameron-Martin derivative, elementary full-measure genericity, and an assembly +with #135's actual robust charts. Its qualitative planar no-saddle-connection +statement is not a conditional-field or regional C103 estimate. + +[AUTHOR_CORRECTION.md](AUTHOR_CORRECTION.md) records exactly what was wrong and +what is preserved. Original #137 proof bytes are not rewritten or accepted. + +Run from this directory: + + python -B -S verify.py --output /path/to/new-output + python -B -O -S verify.py --output /path/to/other-output + +Both entry modes check the full flat packet and execute 18 tests plus 9 intended +semantic negatives in each Python mode. Outputs and source identities must agree. +The tests are finite exact illustrations, not invariant-manifold, support, or +measure-theoretic proofs. All implementation uses the Python standard library. + +The only imported source-level geometry is the pinned robust-chart manuscript +in SOURCE_MAP.json. Claude's A2 note is credited and reviewed separately; its +classical references are not silently used to validate our corrected contraction. +Old AMEND, C103, RN/JETMOD, 3D and registry statuses remain unchanged by publication. diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/RECONNAISSANCE.md b/frontiers/sard_g_a2_parameter_20260929/v2/RECONNAISSANCE.md new file mode 100644 index 000000000..da64e07c2 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/RECONNAISSANCE.md @@ -0,0 +1,29 @@ +# Dependency-focused reconnaissance, 29 September 2026 + +Consensus was called for C1 parameter-dependent hyperbolic invariant manifolds, +Lyapunov-Perron bounded trajectories and Gaussian transversality. It returned +its 30-search monthly quota error, reset October 1. No paper result was returned. + +Direct primary-source record inspected: +A. Vanderbauwhede and S. A. van Gils, Center manifolds and contractions on a scale +of Banach spaces, Journal of Functional Analysis 72(2),209-224 (1987), +DOI 10.1016/0022-1236(87)90086-3. +https://www.sciencedirect.com/science/article/pii/0022123687900863 + +Read scope: publisher abstract and metadata. It explicitly discusses differentiability +only after embeddings on a scale of spaces for a center-manifold construction. +That abstract does NOT verify the precise C2 parameter claim in #137, and this +packet does not import a theorem from it. Our hyperbolic bounded-trajectory proof +is written out, rather than citing a center-manifold theorem by name. + +Further targeted searches for Gaussian Morse-Smale potentials and parameter +stable manifolds returned adjacent results, not a directly verified theorem for +this precise periodic field. This is not a complete novelty audit or evidence +of historical priority. Contraction, Lyapunov-Perron, variation of constants, +Fourier approximation, mesh arguments and Gaussian slicing are classical. + +The source-level mathematics actually read includes #135's full robust predicate, +#137's erroneous predecessor, and #138's full regularity note. The last supplies +an important diagnosis and a weaker line-slicing interface, but its citation-only +invariant-manifold statements are not substituted for the new proof. The author +and dependency exposure are recorded in SOURCE_MAP.json. diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/RESULTS.json b/frontiers/sard_g_a2_parameter_20260929/v2/RESULTS.json new file mode 100644 index 000000000..70ce5a3f3 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/RESULTS.json @@ -0,0 +1,8 @@ +{ + "tests_per_mode": 18, + "semantic_mutants_per_mode": 9, + "identical_output_pairs": 10, + "all_intended_failures": true, + "scientific_effect": "NONE", + "continuum_verified_by_code": false +} diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/SOURCE_FILES.json b/frontiers/sard_g_a2_parameter_20260929/v2/SOURCE_FILES.json new file mode 100644 index 000000000..9fbf77d30 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/SOURCE_FILES.json @@ -0,0 +1,66 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "files": [ + { + "path": "A2_FIXED_FRAME.md", + "bytes": 13253, + "sha256": "d14f0d18213de9031ecc336f6b5b4bd804ae954b84b58c3c2e1a18e94976633d", + "git_blob": "09c45efbde38f81bc152e30ba4b4a51a37c9272b" + }, + { + "path": "AUTHOR_CORRECTION.md", + "bytes": 1514, + "sha256": "1e4f0ca0bb11a44a41331bebedb703b9a4031223e2ee86852c97dd356bbfe921", + "git_blob": "1f72865b30d5366c969be533f7521f01157ae1b8" + }, + { + "path": "NONVANISHING_AND_CLOSURE.md", + "bytes": 15901, + "sha256": "fce5e5ee33cbe49d59077de03a21ed8e6bb2cd77d800e33e67a05f830e43315e", + "git_blob": "7da6a393cabc08063e68587b6e4007c39baba38f" + }, + { + "path": "README.md", + "bytes": 1826, + "sha256": "1c86fcd42ec572fc1a391dc6c8bec106f19b18409cd04877c1847a7335f8759e", + "git_blob": "82404a159b4ed2690963cff7e84c47e2b2d434d0" + }, + { + "path": "RECONNAISSANCE.md", + "bytes": 1760, + "sha256": "5f4d4cba2606369fb2e39f579c4a424283bd029ae32a39e67ebeb064838dbff2", + "git_blob": "da64e07c2701aa2e8251c989b11afb09149d4b3c" + }, + { + "path": "RESULTS.json", + "bytes": 196, + "sha256": "e4502640063f3278dbd287d1ba2b1f83a4300cc2d2fd97f267570a7ec0ad880c", + "git_blob": "70ce5a3f3892304051912347e0c85136f8f6ccdf" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 1625, + "sha256": "b9f8194065a6a69395b9003db95ba8f655e7ee16a6d146157b848274175537fb", + "git_blob": "87bb332962a0db8ce46af33f40af4b8d7b8c15d9" + }, + { + "path": "a2.py", + "bytes": 4152, + "sha256": "119294e4d3ef9277bb6152bbbaafde498b998c39f917f48be4cd314ea6711f6a", + "git_blob": "c089a020cc1d56117e9626741a39a9da4b6731f2" + }, + { + "path": "test_a2.py", + "bytes": 5337, + "sha256": "a9272681bbb962888f02e7140fc8b75ddc765180f30a541e1e143aeea4e50dc8", + "git_blob": "f66c75b64c0eae940afd91f1492c5eaa60d17e4a" + }, + { + "path": "verify.py", + "bytes": 4773, + "sha256": "1fe9616dcd6f8d8787c03f592b5f8905ea6353d753c645373dbe9a4849306d08", + "git_blob": "d84a41f9f6c74090cfa2eb03a604e6da98b48cb9" + } + ] +} diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/SOURCE_MAP.json b/frontiers/sard_g_a2_parameter_20260929/v2/SOURCE_MAP.json new file mode 100644 index 000000000..87bb33296 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/SOURCE_MAP.json @@ -0,0 +1,40 @@ +{ + "scientific_effect": "NONE", + "upstream_replayed_by_packet": false, + "inputs": [ + { + "id": "RC-S", + "repository": "d6g8k5htny-coder/Math-", + "commit": "ee94b06368c29bceca80662698b4b4d6ee81ec91", + "path": "frontiers/sard_g_robust_charts_20260929/PROOF.md", + "git_blob": "7e2237063a8dd0120e9d5bd15a3caaa32e8495fa", + "bytes": 25022, + "sha256": "b91b9f792c6322204a0f2a573b2ca76d5c951e49ddd7caa6ffd1abed0aa79e79", + "use": "Actual first-closed-contact R1/R2 charts and optional R3/R4 slicing; geometric source not overwritten." + }, + { + "id": "CL", + "repository": "d6g8k5htny-coder/Math-", + "commit": "2726594c83ac35b0371362674a1e4e4f52fd3840", + "path": "frontiers/sard_g_a2_regularity_20260929/PROOF.md", + "git_blob": "b27a36e3d337fd0c2bcecdeae6bf013b56883b0f", + "use": "Attribution and cross-check of Lemma J, loss diagnosis and weaker A2-G; cited stable-manifold theorems not imported." + }, + { + "id": "PREDECESSOR", + "repository": "d6g8k5htny-coder/Math-", + "commit": "e944ba0b595d790d27d1466cc4f576467890bc3a", + "path": "frontiers/sard_g_a2_parameter_20260929/PROOF.md", + "use": "INVALID Section3/C1-into-C1 predecessor explicitly withdrawn; no proof dependency." + } + ], + "new_author_claims": [ + "fixed-frame joint Frechet C1 germs", + "localized scalar-potential nonvanishing", + "Fourier-support Cameron-Martin separation", + "Morse/distinct-values mesh proof", + "qualitative unconditioned planar no-connection composition" + ], + "nonauthor_review_required": true, + "no_status_fold": true +} diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/a2.py b/frontiers/sard_g_a2_parameter_20260929/v2/a2.py new file mode 100644 index 000000000..c089a020c --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/a2.py @@ -0,0 +1,115 @@ +"""Exact finite controls for a fixed-frame Lyapunov--Perron proof. + +No numerical trajectory sampling and no Gaussian continuum acceptance. +""" +from fractions import Fraction as F +from math import comb + +MUTANT=None + +def _positive(*values): + if any(F(x)<=0 for x in values): + raise ValueError('positive spectral/radius data required') + +def lp_constants(lam,mu,ell,beta): + lam,mu,ell,beta=map(F,(lam,mu,ell,beta)) + _positive(lam,mu,ell,beta) + if beta>=lam: + raise ValueError('unstable weight must be below lambda') + cu=1/(lam+beta) if MUTANT=='wrong-unstable-weight' else 1/(lam-beta) + cs=1/(mu-beta) if MUTANT=='wrong-stable-weight' else 1/(mu+beta) + return ell*(1/lam+1/mu),ell*(cu+cs) + +def anchor_equilibrium(lam,mu,bu,bs): + """Bounded constant path of x'=lambda*x+bu, y'=-mu*y+bs.""" + lam,mu,bu,bs=map(F,(lam,mu,bu,bs));_positive(lam,mu) + if MUTANT=='drop-constant-forcing': + return F(0),F(0) + px=bu/lam if MUTANT=='reverse-unstable-integral' else -bu/lam + return px,bs/mu + +def unstable_polynomial(lam,mu,rho,c): + """Triangular ILLUSTRATION x'=lambda*x+c, y'=-mu*y+rho*x^2. + +Returns px and coefficients of y(s)=y0+y1*s+y2*s^2, s=x-px. +This illustrative vector field need not be a gradient and is labelled as such. +""" + lam,mu,rho,c=map(F,(lam,mu,rho,c));_positive(lam,mu) + px=anchor_equilibrium(lam,mu,c,0)[0] + return px,rho*px*px/mu,2*rho*px/(mu+lam),rho/(mu+2*lam) + +def fixed_anchor_derivative(lam,mu,rho,c,a): + lam,mu,rho,c,a=map(F,(lam,mu,rho,c,a));_positive(lam,mu) + p=-c/lam;s=a-p + dp=-1/lam + return dp*(2*rho*p/mu+2*rho*(a-2*p)/(mu+lam)-2*rho*s/(mu+2*lam)) + +def matrix_inverse2(A): + a,b=A[0];c,d=A[1];det=a*d-b*c + if not det:raise ValueError('singular matrix') + return [[d/det,-b/det],[-c/det,a/det]] + +def mm(A,B): + return [[sum((x*y for x,y in zip(row,col)),F(0)) for col in zip(*B)] for row in A] + +def dot(a,b):return sum((x*y for x,y in zip(a,b)),F(0)) + +def projection(v,n): + v=list(map(F,v));n=list(map(F,n));den=dot(v,n) + if den==0:raise ValueError('transverse normal denominator required') + if MUTANT=='omit-hit-time-projection': + return [[F(1),F(0)],[F(0),F(1)]] + return [[F(int(i==j))-v[i]*n[j]/den for j in range(2)] for i in range(2)] + +def adjoint_hit(v,n,tau): + P=projection(v,n) + return [sum(F(tau[i])*P[i][j] for i in range(2)) for j in range(2)] + +def eigenline_quotient_bounds(n): + """At t=n^-4: k=sqrt(t)=n^-2, 1=2 required') + t=F(1,n**4);k=F(1,n**2) + if MUTANT=='pretend-Lipschitz-eigenline': + return F(0),F(1) + return k/(t*(2+t/2)),k/(2*t) + +def beta_polynomial_integral(n): + """Integral_0^1 x^n (1-x)^n dx by finite rational expansion.""" + if type(n) is not int or n<0:raise ValueError('integer n>=0 required') + return sum((F((-1)**j*comb(n,j),n+j+1) for j in range(n+1)),F(0)) + +def density_mesh_powers(): + """Probabilistic dimension ledger, not a continuum probability calculation.""" + morse=F(2)+F(1,2)-2 + distinct=F(5)-4 + if MUTANT=='omit-height-difference':distinct=F(4)-4 + if MUTANT=='ignore-singular-slab':morse=F(2)-2 + return morse,distinct + +def gaussian_residual_covariances(weights,ell): + weights=list(map(F,weights));ell=list(map(F,ell)) + v=sum(w*l*l for w,l in zip(weights,ell)) + if v<=0:raise ValueError('positive variance required') + q=[w*l for w,l in zip(weights,ell)] + scale=F(1) if MUTANT=='wrong-residual-scale' else 1/v + # xi=ell(f), g=f-(Qell/v)*xi: unnormalised exact equivalent. + return [a-a*scale*v for a in q] + +def matrix_rank(rows): + A=[list(map(F,row)) for row in rows] + if not A:return 0 + r=0 + for j in range(len(A[0])): + pivot=next((i for i in range(r,len(A)) if A[i][j]),None) + if pivot is None:continue + A[r],A[pivot]=A[pivot],A[r] + for i in range(r+1,len(A)): + if A[i][j]: + q=A[i][j]/A[r][j] + A[i]=[a-q*b for a,b in zip(A[i],A[r])] + r+=1 + if r==len(A):break + return r diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/test_a2.py b/frontiers/sard_g_a2_parameter_20260929/v2/test_a2.py new file mode 100644 index 000000000..f66c75b64 --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/test_a2.py @@ -0,0 +1,103 @@ +"""Exact finite falsification controls; not invariant-manifold or Gaussian proofs.""" +import unittest +from fractions import Fraction as F +import a2 as m + +class Checks(unittest.TestCase): + def test_contraction_denominators(self): + self.assertEqual(m.lp_constants(2,3,F(1,10),1),(F(1,12),F(1,8))) + def test_constant_forcing_retained(self): + self.assertEqual(m.anchor_equilibrium(2,3,1,2),(F(-1,2),F(2,3))) + self.assertEqual(m.unstable_polynomial(2,3,F(1,5),1),(F(-1,2),F(1,60),F(-1,25),F(1,35))) + def test_constant_path_solves_original_vector_field(self): + for bu in (F(-1,3),F(0),F(2,5)): + p=m.anchor_equilibrium(3,5,bu,F(7,11)) + self.assertEqual(3*p[0]+bu,0) + self.assertEqual(-5*p[1]+F(7,11),0) + def test_weight_validation(self): + with self.assertRaises(ValueError):m.lp_constants(2,3,F(1,10),2) + with self.assertRaises(ValueError):m.lp_constants(0,3,F(1,10),1) + def test_nonlinear_germ_exact_invariance(self): + # Triangular (not necessarily gradient) model; chain rule in s=x-p. + for lam,mu,rho,c in ((2,3,F(1,5),1),(3,2,F(1,7),F(-1,3))): + p,y0,y1,y2=m.unstable_polynomial(lam,mu,rho,c) + for s in (F(-1,9),F(0),F(1,11)): + y=y0+y1*s+y2*s*s + self.assertEqual(lam*s*(y1+2*y2*s),-mu*y+rho*(p+s)**2) + def test_fixed_anchor_parameter_derivative(self): + # Graph is a quadratic polynomial in c; centered difference is EXACT. + for c in (F(0),F(1,5),F(-2,7)): + lam,mu,rho,a=F(2),F(3),F(1,5),F(1,17) + def value(cc): + p,y0,y1,y2=m.unstable_polynomial(lam,mu,rho,cc);s=a-p + return y0+y1*s+y2*s*s + eps=F(1,1000) + self.assertEqual((value(c+eps)-value(c-eps))/(2*eps),m.fixed_anchor_derivative(lam,mu,rho,c,a)) + def test_neumann_inverse_equation(self): + B=[[F(1,8),F(1,16)],[F(1,24),F(1,12)]] + Iminus=[[F(int(i==j))-B[i][j] for j in range(2)] for i in range(2)] + inv=m.matrix_inverse2(Iminus) + self.assertEqual(m.mm(Iminus,inv),[[1,0],[0,1]]) + self.assertLess(max(sum(abs(x) for x in row) for row in B),F(1,4)) + def test_projection_annihilates_time_direction(self): + v=[F(2),F(3)];n=[F(1),F(0)];tau=[F(0),F(1)] + cov=m.adjoint_hit(v,n,tau) + self.assertEqual(m.dot(cov,v),0) + self.assertEqual(m.dot(cov,tau),1) + self.assertEqual(cov,[F(-3,2),F(1)]) + def test_projection_requires_transversality(self): + with self.assertRaises(ValueError):m.projection([0,1],[1,0]) + def test_scalar_potential_transverse_forcing(self): + # Straight regular segment: h(x,y)=x^3(1-x)^3*y near y=0. + self.assertEqual(m.beta_polynomial_integral(3),F(1,140)) + for a,gprime,phi in ((F(2),F(3,2),F(1,5)),(F(-3),F(-1,2),F(2,7))): + sign=1 if a>0 else -1 + cov=[-a*gprime,a];grad=[-sign*phi*gprime,sign*phi] + self.assertEqual(m.dot(cov,grad),abs(a)*phi*(1+gprime*gprime)) + self.assertGreater(m.dot(cov,grad),0) + def test_eigenline_derivative_loss_counterexample(self): + previous=F(0) + for n in (2,4,8,16,32): + lo,hi=m.eigenline_quotient_bounds(n) + self.assertGreater(lo,F(n*n,3)) + self.assertLess(lo,hi) + self.assertGreater(lo,previous) + previous=lo + def test_cusp_saddle_hessian(self): + for n in (2,4,8,16): + t=F(1,n**4);k=F(1,n**2) + self.assertEqual(k*k,t) + det=-1-k*k + self.assertEqual(det,-1-t) + self.assertLess(det,0) + # (1+t/2)^2>1+t gives the rational square-root enclosure. + self.assertGreater((1+t/2)**2,1+t) + def test_stationary_point_graph_parameter(self): + # Coordinate derivative stays nonzero at the saddle even though flow speed is zero. + for s in (F(0),F(1,10)): + dxds=1 + self.assertNotEqual(dxds,0) + if not s:self.assertEqual(3*s,0) + def test_morse_mesh_exponent(self): + self.assertEqual(m.density_mesh_powers()[0],F(1,2)) + self.assertGreater(m.density_mesh_powers()[0],0) + def test_distinct_value_mesh_exponent(self): + self.assertEqual(m.density_mesh_powers()[1],1) + self.assertGreater(m.density_mesh_powers()[1],0) + def test_two_point_derivative_functionals(self): + # Columns x,x^2,x^3,y,xy; rows grad at (0,0),(1,0), f(1,0)-f(0,0). + rows=[[1,0,0,0,0],[0,0,0,1,0],[1,2,3,0,0],[0,0,0,1,1],[1,1,1,0,0]] + self.assertEqual(m.matrix_rank(rows),5) + self.assertEqual(m.matrix_rank(rows[:-1]),4) + self.assertEqual(m.matrix_rank(rows[:-1]+[rows[0]]),4) + def test_gaussian_residual_independence_identity(self): + self.assertEqual(m.gaussian_residual_covariances([1,F(1,2),F(1,3)],[1,2,3]),[0,0,0]) + with self.assertRaises(ValueError):m.gaussian_residual_covariances([1,0],[0,1]) + def test_localization_second_derivative_vanishes_at_edge(self): + # x^3(1-x)^3 has value, first and second derivatives zero at both endpoints. + coeff=[0,0,0,1,-3,3,-1] + for order in (0,1,2): + for x in (0,1):self.assertEqual(sum(c*x**i for i,c in enumerate(coeff)),0) + coeff=[i*c for i,c in enumerate(coeff)][1:] + +if __name__=='__main__':unittest.main() diff --git a/frontiers/sard_g_a2_parameter_20260929/v2/verify.py b/frontiers/sard_g_a2_parameter_20260929/v2/verify.py new file mode 100644 index 000000000..d84a41f9f --- /dev/null +++ b/frontiers/sard_g_a2_parameter_20260929/v2/verify.py @@ -0,0 +1,96 @@ +"""Exact packet membership and finite controls; no continuum proof claim.""" +import argparse +import hashlib +import io +import json +from pathlib import Path +import subprocess +import sys +import unittest + +ROOT=Path(__file__).resolve().parent +MUTANTS={ + 'wrong-unstable-weight':'test_contraction_denominators', + 'wrong-stable-weight':'test_contraction_denominators', + 'drop-constant-forcing':'test_constant_forcing_retained', + 'reverse-unstable-integral':'test_constant_path_solves_original_vector_field', + 'omit-hit-time-projection':'test_projection_annihilates_time_direction', + 'pretend-Lipschitz-eigenline':'test_eigenline_derivative_loss_counterexample', + 'omit-height-difference':'test_distinct_value_mesh_exponent', + 'ignore-singular-slab':'test_morse_mesh_exponent', + 'wrong-residual-scale':'test_gaussian_residual_independence_identity', +} + +def need(ok,message): + if not ok:raise ValueError(message) + +def decode(text): + def unique(items): + out={} + for k,v in items: + need(k not in out,'duplicate JSON key: '+k);out[k]=v + return out + return json.loads(text,object_pairs_hook=unique) + +def identity(p): + need(p.is_file() and not p.is_symlink(),'regular source required: '+p.name) + b=p.read_bytes() + return {'bytes':len(b),'sha256':hashlib.sha256(b).hexdigest(), + 'git_blob':hashlib.sha1(f'blob {len(b)}\0'.encode()+b).hexdigest()} + +def sources(): + identity(ROOT/'SOURCE_FILES.json') + entries=decode((ROOT/'SOURCE_FILES.json').read_text())['files'] + names=[e['path'] for e in entries] + need(len(names)==len(set(names)) and all(Path(n).name==n and n!='SOURCE_FILES.json' for n in names), + 'unique flat paths required') + need(sorted(p.name for p in ROOT.iterdir())==sorted(names+['SOURCE_FILES.json']), + 'source membership differs') + for e in entries: + need(identity(ROOT/e['path'])=={k:e[k] for k in ['bytes','sha256','git_blob']},'source identity differs: '+e['path']) + return {p.name:identity(p) for p in sorted(ROOT.iterdir())} + +def child(mutant): + import a2, test_a2 + a2.MUTANT=mutant + res=unittest.TextTestRunner(stream=io.StringIO()).run(unittest.defaultTestLoader.loadTestsFromModule(test_a2)) + data={'tests':res.testsRun,'passed':res.wasSuccessful(), + 'failures':sorted(t.id().rsplit('.',1)[-1] for t,_ in res.failures), + 'errors':sorted(t.id().rsplit('.',1)[-1] for t,_ in res.errors)} + print(json.dumps(data,sort_keys=True)) + return 0 if res.wasSuccessful() else 1 + +def replay(path): + path=path.resolve() + need(not path.exists() and not path.is_relative_to(ROOT),'new output outside packet required') + before=sources();path.mkdir(parents=True) + cases={} + for case in ['baseline',*MUTANTS]: + outputs=[] + for mode,flags in [('normal',[]),('optimized',['-O'])]: + cmd=[sys.executable,'-B',*flags,'-S',str(ROOT/'verify.py'),'--child'] + if case!='baseline':cmd+=['--mutant',case] + run=subprocess.run(cmd,capture_output=True,timeout=30) + (path/(case+'_'+mode+'.stdout')).write_bytes(run.stdout) + (path/(case+'_'+mode+'.stderr')).write_bytes(run.stderr) + record=decode(run.stdout.decode()) + need(not run.stderr and not record['errors'],'execution error, not intended failure: '+case) + need(record['tests']==18,'incorrect test count') + if case=='baseline':need(run.returncode==0 and record['passed'] and not record['failures'],'baseline failed') + else:need(run.returncode==1 and not record['passed'] and MUTANTS[case] in record['failures'],'semantic mutant escaped: '+case) + outputs.append(run.stdout) + need(outputs[0]==outputs[1],'normal/optimized mismatch: '+case) + cases[case]=decode(outputs[0].decode()) + summary={'tests_per_mode':18,'semantic_mutants_per_mode':9,'identical_output_pairs':10, + 'all_intended_failures':True,'scientific_effect':'NONE','continuum_verified_by_code':False} + need(summary==decode((ROOT/'RESULTS.json').read_text()),'stored summary differs') + need(before==sources(),'source changed during execution') + (path/'REPORT.json').write_text(json.dumps({**summary,'cases':cases,'sources':before,'sources_unchanged':True},indent=2,sort_keys=True)+'\n') + print(json.dumps(summary,sort_keys=True));return 0 + +if __name__=='__main__': + p=argparse.ArgumentParser(description=__doc__);g=p.add_mutually_exclusive_group(required=True) + g.add_argument('--child',action='store_true');g.add_argument('--output',type=Path) + p.add_argument('--mutant',choices=MUTANTS);o=p.parse_args() + need(o.child or o.mutant is None,'mutant requires child mode') + raise SystemExit(child(o.mutant) if o.child else replay(o.output)) diff --git a/frontiers/sard_g_a2_regularity_20260929/PROOF.md b/frontiers/sard_g_a2_regularity_20260929/PROOF.md new file mode 100644 index 000000000..8ea2c3537 --- /dev/null +++ b/frontiers/sard_g_a2_regularity_20260929/PROOF.md @@ -0,0 +1,185 @@ +# SARD-G premise A2: where the regularity actually sits, and the weakest form the slicing needs + +Object: CL-SARD-A2-REGULARITY-20260929-v2. +Author: Anthropic Claude (Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3`). +Disposition: AUTHOR-SIDE SOURCE NOTE; nonauthor review required. +Scientific effect: NONE. No register, graph, lemma flag, prize or source changes. C103 is not moved. + +## 1. Contract + +The robust-chart successor [RC-S] (Math-#135, `frontiers/sard_g_robust_charts_20260929/PROOF.md`, blob `7e223706…`) +imports two premises from SG (main `a1fc9581`), which lists "A2 parameter-dependent local invariant-manifold and +first-crossing regularity" but proves neither. The published A1–A6 reviews issue no A2 verdict. + +- **A2-T.** The local branch germs and the finite regular flow arcs depend continuously on `f ∈ X = C²(T_L²)` in the + `C¹` arc topology. +- **A2-D.** The same objects are `C¹` in the field parameter and the arc parameter. + +[RC-S] §2 warns that any regularity loss "at the C2-field/C1-vector-field interface must be resolved in A2's own +review". This note makes three claims. + +- **(J)** `F(x, f) = ∇f(x)` is jointly Fréchet-`C¹` on `T² × X`. A loss of one derivative appears only if one asks + for `f ↦ γ_f` to be Fréchet `C¹` *into `C¹` arcs*. No step of [RC-S] asks for that. +- **(G)** Every use of A2-D in [RC-S] (R1a, R2's `C¹` mismatch, R3d, R4) needs only the weaker line form A2-G of §4, + and A2-G follows from classical one-parameter theory. +- **(T)** A2-T follows from classical continuous-dependence theory. + +§5 checks each use of A2-G against [RC-S]. The full Fréchet A2-D is recorded in §6 as cited theory, not proved here. +A3–A4 are not addressed. + +## 2. Lemma J: the vector field is jointly `C¹` in position and field + +Use the flat structure of `T_L² = ℝ²/(Lℤ)²`, so `∇` and `D²` are global. Define `F: T² × X → ℝ²` by +`F(x, f) = ∇f(x)`. + +**Lemma J.** `F` is Fréchet `C¹`, with + + DF(x, f)[ξ, h] = D²f(x) ξ + ∇h(x). (J1) + +For all `x, y ∈ T²` and `f, g ∈ X`: + + |D²f(x) − D²g(y)| ≤ ‖f − g‖_{C²} + ω_{D²g}(|x − y|), (J2) + sup_{‖h‖_{C²} ≤ 1} |∇h(x) − ∇h(y)| ≤ |x − y|, (J3) + +where `ω` is a modulus of continuity. + +*Proof.* `F` is linear in `f` and `C¹` in `x` for fixed `f`. The remainder + + F(x+ξ, f+h) − F(x, f) − D²f(x)ξ − ∇h(x) + = [∇f(x+ξ) − ∇f(x) − D²f(x)ξ] + [∇h(x+ξ) − ∇h(x)] + +is `o(|ξ|) + ‖h‖_{C²}|ξ| = o(|ξ| + ‖h‖)`. Continuity of `(x, f) ↦ DF(x, f)` in operator norm is exactly (J2) for +the `ξ`-part and (J3) for the `h`-part. (J3) is the mean-value inequality with `‖D²h‖_∞ ≤ ‖h‖_{C²}`. ∎ + +**Where a derivative is lost.** Consider `X → C¹(T²; ℝ²)`, `f ↦ ∇f(· + p(f))`, the field recentred at a moving +saddle `p(f)`. It is not differentiable in general for `f ∈ C² ∖ C³`: its derivative in `p` would be +`D²f(· + p) ∈ C¹`, which requires `D³f`. Proofs that recentre and then apply a Banach fixed-point argument in `C¹` +function spaces therefore lose a derivative. A second, easily missed loss occurs at a moving saddle. The unstable eigenline `e_u(f)` of `D²f(p(f))` is only +*continuous* in `f`: its derivative in direction `h` would involve `D²h(p) + D³f(p)[Dp(f)h]`, which needs `D³f`. So a +germ written as a graph over the MOVING eigenline need not be `C¹` in `f`, even though the geometric germ is. The +remedy is to use a graph coordinate over a FIXED direction, chosen once per atlas neighbourhood (§4). Transversality +keeps the germ a graph there, and the geometric first hit on a fixed section is independent of the parameterization. + +The arguments of [RC-S] never recentre in `C¹` function spaces. They differentiate point +functionals `(s, f) ↦ γ_f(s)` and hitting times through the scalar implicit-function theorem (R1a), which needs only +(J1)–(J3) and their consequences below. + +## 3. A2-T from continuous dependence + +Let `f_0 ∈ U_χ^rob` and let `p_0` be a tracked hyperbolic saddle. +- **Saddles.** By (J1) and the implicit-function theorem, `p(f)` is `C¹` near `f_0`, with + `Dp(f)[h] = −D²f(p)^{-1}∇h(p)`. +- **Local germs.** For `C¹` vector fields, the local stable and unstable manifolds of a hyperbolic equilibrium are + `C¹` embedded curves that depend continuously on the vector field in the `C¹` topology (stable manifold theorem with + continuous dependence; e.g. Palis–de Melo, *Geometric Theory of Dynamical Systems*, Ch. 2 §6; Hirsch–Pugh–Shub). + Since `f ↦ ∇f ∈ C¹` is bounded linear, the four labelled germs, written as graphs over the continuing eigenlines, + depend continuously on `f ∈ X` in the `C¹` arc topology. +- **Regular arcs.** On compact time intervals, solutions of `ẋ = ∇f(x)` and their first spatial derivatives depend + continuously on the vector field in `C¹` (Gronwall). + +Hence A2-T holds on the chart domains. This is the only premise R2's openness uses. + +## 4. A2-G: the line form, from one-parameter theory + +**A2-G.** For every `f ∈ U_χ^rob` and `h ∈ X`: +1. `t ↦ D_χ(f + th)` is `C¹` on the open set `{t: f + th ∈ U_χ^rob}`, with derivative at `t = 0` equal to `L_f(h)`. +2. `h ↦ L_f(h)` is linear, with `|L_f(h)| ≤ C_f ‖h‖_{C¹}`. +3. For each fixed `h`, `f ↦ L_f(h)` is continuous on `U_χ^rob`. + +The same holds for the launch points, the hit parameters and the hit points. + +*Proof.* Fix `f, h` and set `V_t(x) = ∇f(x) + t∇h(x)`. By Lemma J, `(x, t) ↦ V_t(x)` is `C¹`, and it is affine in +`t` with `∂_t V_t = ∇h ∈ C¹`. This is a one-parameter `C¹` family of planar vector fields, so classical +finite-parameter theory applies. +- The saddle `p(t)` is `C¹` by the implicit-function theorem. +- The local unstable and stable manifolds are `C¹` in `(a, t)` as graphs `w̃(a, t)` over a FIXED direction (the + eigenline at `t = 0`), not over the moving eigenline (see §2). + Suspend with `ṫ = 0`. The curve `{(p(t), t)}` is a normally hyperbolic curve of equilibria, and its local + unstable (stable) manifold is `C¹` (Fenichel; Hirsch–Pugh–Shub). Alternatively, cite the parameter-dependent + stable manifold theorem for `C¹` families. +- The flow is `C¹` in `(time, x, t)`, by classical dependence on parameters. +- Hitting times and points are `C¹`, by R1a. + +This proves part 1 at `t = 0`, and at every point of the open set by applying the same argument at `f + t_0 h`. + +**Linearity and the bound (part 2).** The `t`-derivative is obtained by linearizing at `t = 0`. The perturbation +enters the variational equations only through the forcing `∇h`, evaluated along the saddle, the germs and the arcs. +- The saddle moves by `−D²f(p)^{-1}∇h(p)`. +- The germ variation is the unique solution of the linearized invariance equation that stays bounded in backward + time. It has the Lyapunov–Perron form `∫_{−∞}^0 (dichotomy kernel)·∇h(γ(σ)) dσ`. On the compact germ domain it is + bounded by `C_f ‖∇h‖_{C⁰}`. +- The flow and hitting variations are Duhamel integrals of `∇h` along compact arcs, divided by the positive transverse + margin in R1a. + +All of these are linear in `h` and bounded by `C_f ‖h‖_{C¹}`. + +**Continuity in `f` (part 3).** The data of these linear formulas depend continuously on `f ∈ X`: +- the orbit, `D²f` along it, and the eigenprojections, by §3; +- the exponential dichotomy on the germ domain, which is robust under `C¹`-small perturbations of the coefficient + `D²f(γ(σ))`; +- the transverse margin, which is bounded below on the chart. + +Dominated convergence in the convergent dichotomy integrals then gives continuity of `f ↦ L_f(h)`. ∎ + +`a2_check.py` gives an exact polynomial instance of the Lyapunov–Perron variation. +- For `V_t(x, y) = (x, −y + x² + t x³)` the unstable manifold is exactly `y = x²/3 + t x³/4`. +- Its `t`-derivative `x³/4` equals the backward integral `∫_{−∞}^0 e^{σ}(x e^{σ})³ dσ`. +- Two perturbations superpose linearly: `t_1 x³ + t_2 x⁴` gives `t_1 x³/4 + t_2 x⁴/5`. +- The saddle-displacement formula holds for `V_t = (x − t, −y + x²)`. + +## 5. Each use in [RC-S] needs only A2-T and A2-G + +| Use in [RC-S] | What is needed | Supplied by | +|---|---|---| +| R2 openness of `U_χ^rob` | continuity of germs, arcs and hits | A2-T (§3) with R1 | +| R1a hit derivative | `C¹` dependence of `(s, f) ↦ γ_f(s)` along the direction used | A2-G part 1 | +| R4: `B_{χ,ℓ}` Borel | `D_χ` continuous; `f ↦ ∂_{h_ℓ} D_χ(f)` continuous | A2-T; A2-G part 3 | +| R4: `F_g(t) = D_χ(g + t h_ℓ)` is `C¹` with `F_g' = L_{g+th_ℓ}(h_ℓ)` | line `C¹` with continuous derivative | A2-G parts 1 and 3 | +| R3d: some `h_ℓ` with nonzero derivative | `L_f|_H` linear, continuous, nonzero | A2-G part 2 (since `‖h‖_{C¹} ≤ C‖h‖_H`), with A3–A4 read for `L_f` | + +The A3–A4 premise is phrased in [RC-S] for "the derivative of the mismatch". Its original route computes that +derivative as a curve contribution plus endpoint-supported terms applied to `h`, which is exactly `L_f(h)`. Reading +it for the line derivative `L_f` therefore changes nothing in that route. Its nonvanishing is not addressed here. + +**Note for [RC-S] P2.** P2's "graph coordinate" should be read as a fixed-frame coordinate chosen with the atlas +neighbourhood. If it meant the moving eigen-coordinate, the germ parameterization could fail to be `C¹` in `f`. +R1a would then apply to a different, fixed-frame parameterization of the same geometric germ, with the same hit +point. No conclusion changes, but the wording should say which coordinate is meant. + +## 6. The full Fréchet A2-D (cited theory, not proved here) + +By Lemma J, the planar vector-field family `(x, f) ↦ ∇f(x)` is jointly `C¹` with a Banach parameter. +- Flows of `C¹` vector fields with a `C¹` Banach parameter are `C¹` in `(time, x, parameter)` (Dieudonné, + *Foundations of Modern Analysis*, the chapter on differential equations). +- Local unstable manifolds depend `C¹` on Banach parameters by the Lyapunov–Perron method on a scale of exponentially + weighted spaces (Vanderbauwhede–van Gils, 1987). The loss of exponent in the Nemytskii operator is handled there by + the two-weight argument. + +With (J1)–(J3) these give A2-D as stated in [RC-S]. This note does not reprove those theorems. The reduction of §5 +means that [RC-S]'s conclusions need only §§3–4. + +## 7. Reading rule + +This note licenses exactly the following. +1. **Lemma J**, as proved in §2. +2. **A2-T and A2-G**, as consequences of the classical theorems named in §§3–4, under those theorems' stated + hypotheses. The citation-based steps await nonauthor verification against primary sources. +3. **A reduced application of [RC-S].** R1a, R2's `C¹` mismatch, R3d (with A3–A4 read for the line derivative + `L_f`) and R4 are to be read with **A2-G in place of A2-D**, as tabulated in §5. + +It does **not** license the literal Fréchet sentence A2-D ("C1 in the field parameter" on `X`). That stronger +assertion stays an import of [RC-S], and §6 only cites it. A consumer that needs Fréchet differentiability of +`D_χ` on `X`, rather than its line derivatives, cannot use this note for it. + +## 8. Scope + +- Proved here: Lemma J; the reduction of §5. +- Classical theorems with explicit hypotheses: A2-T and A2-G. +- Cited only: the full A2-D. +- Not addressed: A3–A4, finite-jet nondegeneracy, `μ(Ω_gen) = 1`, the R1/R2 geometry (Harper's slice) and C103. +- The finite companion checks exact polynomial identities only. + +## Revisions + +- **v2** ([5891507824](https://github.com/d6g8k5htny-coder/Math-/pull/138#issuecomment-5891507824)): adds the §7 reading + rule, which separates the reduced A2-G application from the unproved literal Fréchet A2-D. No other change. diff --git a/frontiers/sard_g_a2_regularity_20260929/RESULTS.json b/frontiers/sard_g_a2_regularity_20260929/RESULTS.json new file mode 100644 index 000000000..44f7705d1 --- /dev/null +++ b/frontiers/sard_g_a2_regularity_20260929/RESULTS.json @@ -0,0 +1,10 @@ +{ + "checks": { + "graph_invariant_and_linear_in_perturbation": true, + "saddle_displacement_formula": true, + "variation_equals_backward_integral": true + }, + "object": "CL-SARD-A2-REGULARITY-20260929-v1", + "passed": true, + "scope": "exact polynomial identities only; not the invariant-manifold theorems" +} diff --git a/frontiers/sard_g_a2_regularity_20260929/SOURCE_FILES.json b/frontiers/sard_g_a2_regularity_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..8b2c9bb21 --- /dev/null +++ b/frontiers/sard_g_a2_regularity_20260929/SOURCE_FILES.json @@ -0,0 +1,42 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "disposition": "AUTHOR_SIDE_SOURCE_NOTE", + "consumes": [ + { + "id": "RC-S", + "repository": "d6g8k5htny-coder/Math-", + "pr": 135, + "head": "ee94b06368c29bceca80662698b4b4d6ee81ec91", + "path": "frontiers/sard_g_robust_charts_20260929/PROOF.md", + "git_blob": "7e2237063a8dd0120e9d5bd15a3caaa32e8495fa" + }, + { + "id": "SG", + "repository": "d6g8k5htny-coder/main", + "commit": "a1fc9581291b6f81c76c903c96a13955b51f8d54", + "path": "research/q0/sard_g/SARD_G_EXECUTION_REPAIR_20260925.md", + "git_blob": "8f86e0c9ef91fde473e2344a3e461c31f63f8529" + } + ], + "files": [ + { + "path": "PROOF.md", + "bytes": 11882, + "sha256": "6eae144117e67ea9bcc990c2a681acee7179ad5f3794449a85577c71d934aac9", + "git_blob": "8ea2c35375085905986a144c44b522a0b397cee7" + }, + { + "path": "RESULTS.json", + "bytes": 317, + "sha256": "4f4f3edac6daa6d0331c451e36e441c0b83eceb70cf643345ba72c3bb652a34c", + "git_blob": "44f7705d1447d2da3e3e2579a3dadea20451262e" + }, + { + "path": "a2_check.py", + "bytes": 3562, + "sha256": "78f092d25339dace5011bd266b36736cd07a26506c65d98c31bb85ecc6221c05", + "git_blob": "73a56609dc9d2228a0962687af2948b0a98a11bf" + } + ] +} diff --git a/frontiers/sard_g_a2_regularity_20260929/a2_check.py b/frontiers/sard_g_a2_regularity_20260929/a2_check.py new file mode 100644 index 000000000..73a56609d --- /dev/null +++ b/frontiers/sard_g_a2_regularity_20260929/a2_check.py @@ -0,0 +1,91 @@ +"""Exact polynomial companion for CL-SARD-A2-REGULARITY-20260929-v1 (PROOF.md). Standard library, exact rationals. + +INVARIANCE for V_t(x,y) = (x, -y + x^2 + t1 x^3 + t2 x^4) the graph y = x^2/3 + t1 x^3/4 + t2 x^4/5 is invariant + (coefficientwise polynomial identity), so the unstable-manifold graph is C1 in (x, t) and LINEAR in the + perturbation coefficients. +LYAPUNOV the t1-derivative x^3/4 equals the bounded backward solution z(0) = int_{-inf}^0 e^{s} (x e^{s})^3 ds, + i.e. x^3 * 1/(3+1); the t2-derivative x^4/5 likewise with 1/(4+1). +SADDLE V_t = (x - t, -y + x^2): p(t) = (t, t^2) and dp/dt = -DV(p)^{-1} d_tV = (1, 2t) exactly. +Mutants (each must fail): lp-exponent, nonlinear-superposition, saddle-sign. +""" +import argparse +import json +import sys +from fractions import Fraction as F + +MUTANTS = ("lp-exponent", "nonlinear-superposition", "saddle-sign") +MUT = None + + +def poly_mul(a, b): + out = {} + for i, x in a.items(): + for j, y in b.items(): + out[i + j] = out.get(i + j, F(0)) + x * y + return {k: v for k, v in out.items() if v != 0} + + +def poly_add(*ps): + out = {} + for p in ps: + for k, v in p.items(): + out[k] = out.get(k, F(0)) + v + return {k: v for k, v in out.items() if v != 0} + + +def deriv(p): + return {k - 1: k * v for k, v in p.items() if k > 0} + + +def check_invariance(): + ok = True + for t1 in (F(0), F(1), F(-3, 2)): + for t2 in (F(0), F(2, 5), F(-1)): + c4 = t2 / 5 if MUT != "nonlinear-superposition" else t2 / 5 + t1 * t2 + w = {2: F(1, 3), 3: t1 / 4, 4: c4} # y = w(x) + xdot = {1: F(1)} # xdot = x + lhs = poly_mul(deriv(w), xdot) # d/dt w(x(t)) = w'(x) xdot + rhs = poly_add({k: -v for k, v in w.items()}, {2: F(1), 3: t1, 4: t2}) # ydot on the graph + ok &= lhs == rhs + return {"graph_invariant_and_linear_in_perturbation": ok} + + +def check_lyapunov(): + # z' = -z + x(s)^n with x(s) = x e^{s}: bounded backward solution z(0) = x^n int_{-inf}^0 e^{(n+1)s} ds = x^n/(n+1) + ok = True + for n, coeff in ((3, F(1, 4)), (4, F(1, 5))): + integral = F(1, n + (0 if MUT == "lp-exponent" else 1)) + ok &= integral == coeff + return {"variation_equals_backward_integral": ok} + + +def check_saddle(): + ok = True + for t in (F(0), F(1, 3), F(-2)): + p = (t, t * t) + ok &= p[0] - t == 0 and -p[1] + p[0] ** 2 == 0 # V_t(p) = 0 + DV = [[F(1), F(0)], [2 * p[0], F(-1)]] + det = DV[0][0] * DV[1][1] - DV[0][1] * DV[1][0] + inv = [[DV[1][1] / det, -DV[0][1] / det], [-DV[1][0] / det, DV[0][0] / det]] + dtV = (F(-1), F(0)) + sign = 1 if MUT == "saddle-sign" else -1 + dp = tuple(sign * (inv[i][0] * dtV[0] + inv[i][1] * dtV[1]) for i in range(2)) + ok &= dp == (F(1), 2 * t) + return {"saddle_displacement_formula": ok} + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = {**check_invariance(), **check_lyapunov(), **check_saddle()} + passed = all(checks.values()) + print(json.dumps({"object": "CL-SARD-A2-REGULARITY-20260929-v1", "checks": checks, "passed": passed, + "scope": "exact polynomial identities only; not the invariant-manifold theorems"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/frontiers/sard_g_pinned_transfer_20260929/PROOF.md b/frontiers/sard_g_pinned_transfer_20260929/PROOF.md new file mode 100644 index 000000000..314e38c6f --- /dev/null +++ b/frontiers/sard_g_pinned_transfer_20260929/PROOF.md @@ -0,0 +1,144 @@ +# SARD-G for pinned and tilted laws: the measure-dependent steps and their transfer + +Object: CL-SARD-PINNED-TRANSFER-20260929-v1. +Author: Anthropic Claude (Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3`). +Disposition: AUTHOR-SIDE SOURCE NOTE; nonauthor review required. +Version: v2 (admissible-law scope for Corollary R0, per OpenAI review 5353818348; Theorem P unchanged). +Scientific effect: NONE. No register, graph, lemma flag, prize or source changes. R0 and C103 are not moved. + +## 1. Why this is needed + +In the q0 program, R0 is the Gaussian-Sard/Morse–Smale condition *for the conditioned flow*: the pinned law `Q_r` +and its tilt `Q_r^W` (q0 ledger, "MS-Sard / R0: a.s. Morse–Smale for the conditioned flow"). The SARD-G chain is +written for the unconditioned law `μ` of the periodized field on `X = C²(T_L²)`, which is the "full-Gaussian C103 +corollary": +- SG (main `a1fc9581`); +- the robust-chart successor [RC-S] (Math-#135, blob `7e223706…`); +- the A2 note [A2] (Math-#138); +- the forthcoming A3/A4 proof. + +The pinned laws are singular with respect to `μ`: they live on the null set `{U_r = v_r}`. The conclusion therefore +does not transfer by absolute continuity. This note identifies exactly which steps of the chain depend on the measure, +and proves that each of them holds for the pinned and tilted laws. + +## 2. Which steps depend on the measure + +Go through [RC-S] §§3–8 and [A2]. +- **Deterministic statements about a fixed field or chart:** + - R1 (first contact); + - the chart predicate P1–P4, openness (R2) and coverage (R2b); + - A2-T and A2-G, including the bound `|L_f(h)| ≤ C_f‖h‖_{C¹}`; + - the countability of regular zeros on a line (R4). +- **Steps that use the measure `μ`:** + - **(M1)** R3: density of covariance images in the Cameron–Martin space, and the independent residual. + - **(M2)** A3–A4: the line derivative `L_f` is nonzero *on the Cameron–Martin space*. + - **(M3)** the full-measure generic set `Ω_gen` (Morse, distinct critical values). + - **(M4)** the Tonelli step of R4, which uses the independent standard-normal coordinate. + +## 3. The localized form of A3–A4 + +**(L).** Let `f ∈ Ω_gen` lie in some `U_χ^rob` with `D_χ(f) = 0`. For every finite set `P` of critical points of `f`, +there is `φ ∈ C^∞(T²)` vanishing on a neighbourhood of `P` with `L_f(φ) ≠ 0`. + +The announced A3/A4 proof (Math-#138 comment 5891507824) uses a `C²` bump transverse to an interior point of the +unstable half-arc, away from the endpoint neighbourhoods and the stable half-arc. Such a bump already satisfies (L). +The half-arc consists of regular points, so it has positive distance from every critical point, and the bump's support +can be shrunk to avoid any finite critical set `P`. This note uses (L) as its A3–A4 input and does not prove it. + +## 4. Theorem P (pinned Gaussian laws) + +**Setting.** +- Let `P ⊂ T²` be finite, and let `J_P h = (h(p), ∇h(p))_{p∈P}`, which is `3|P|` functionals. +- Let `f̃` be the centered Gaussian field obtained from the periodized field by regression on `J_P`, that is, + conditioning on `J_P = 0`. +- Let `m ∈ C³(T²)` be deterministic with `∇m(p) = 0` for `p ∈ P`. +- Put `Q = Law(m + f̃)`. Then `Q`-a.s. every point of `P` is a critical point. + +**Theorem P.** Assume the deterministic imports of §2, and (L). Assume also `Q(Ω_gen) = 1`, where `Ω_gen` means Morse +with distinct critical values. Then the saddle–saddle connection event is `Q`-null in the completed space. + +*Proof.* + +**(M1).** The covariance operator of `f̃` is `Q̃ℓ = Π_P Qℓ`, where `Π_P` is the `H`-orthogonal projection onto +`H_P = {h ∈ H : J_P h = 0}`. The Cameron–Martin space of `f̃` is `H_P` with the `H` inner product. For `h ∈ H_P`, +`⟨h, Q̃ℓ_n⟩_H = ⟨h, Qℓ_n⟩_H = h(x_n)`. So `h ⊥ Q̃ℓ_n` for all `n` forces `h = 0` on the dense set `S`, hence `h = 0`. +The images `Q̃ℓ` of rational combinations of point evaluations are therefore dense in `H_P`. The normalization, the +standard-normal coordinate `ξ_ℓ = ℓ(f̃)/√v_ℓ` and the independent residual `g_ℓ = m + f̃ − ξ_ℓ h_ℓ` are exactly as +in R3, now with `f̃`. The deterministic mean sits in the residual. + +**(M2).** Take `φ` from (L), with `P` the pin set, which consists of critical points `Q`-a.s. Trigonometric polynomials +lie in `H` (every Fourier weight is positive) and are dense in `C²`, by Fejér means of the smooth `φ`, so choose +trigonometric polynomials `τ_n → φ` in `C²`. The functionals `J_P` are linearly independent on trigonometric +polynomials (distinct-site jets), so choose trigonometric polynomials `ψ_i` dual to them. Then +`h_n = τ_n − Σ_i (J_P τ_n)_i ψ_i ∈ H_P` and `h_n → φ` in `C²`, because `J_P τ_n → J_P φ = 0`. By A2-G part 2, +`L_f` is continuous in `C¹`, so `L_f(h_n) → L_f(φ) ≠ 0`. Thus `L_f|_{H_P} ≠ 0`, and by (M1) some `h_ℓ` has +`L_f(h_ℓ) ≠ 0`. This is (R3d) for `Q`. + +**(M4).** R4 goes through verbatim. `B_{χ,ℓ}` is Borel by A2-T and A2-G part 3. On each open validity interval the +regular zeros are countable. Independence of `ξ_ℓ` and `g_ℓ` together with Tonelli gives `Q(B_{χ,ℓ}) = 0`. + +**(M3)** is assumed. The covering (R2b) is deterministic. A countable union of null sets is null, so +`Q*(Connection) ≤ Q*(Connection ∩ Ω_gen) + Q(Ω_gen^c) = 0`. ∎ + +With `P = ∅` and `m = 0`, Theorem P is the full-Gaussian statement, so the theorem also re-derives that case under +the same imports. + +## 5. Genericity for the laws used by R0 + +Fix an **admissible** law: distinct pin sites `M ≠ S` on `T²` and gap `k > 0`, within the validity regime of the +parent (its local cylinder and pin covariance, `0 < r ≤ r_0` below the torus injectivity scale), or a separately +proved extension. For example `r = L`, `u = e_1` identifies `M` and `S` on the torus, and then unequal pinned values +are impossible; such parameters are excluded. For each admissible law, `Q_r` is `Law(m_r + f̃)` with `P = {M, S}`. +The pins are values and gradients, so `J_P` is exactly the pin frame `U_r` up to an invertible map. `m_r` is the +regression mean, which has `∇m_r = 0` at `M` and `S`. + +D1 parent §8, `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (sha `9350ad6e…`), accepted +within the D1 reconciliation of Math-#126, proves exactly `Q_r(Ω_gen) = 1`, and then `Q_r^W(Ω_gen) = 1` because +`0 < Z_r < ∞`. Its ingredients are: +- an overdetermined-zero lemma, applied to `(∇f(x), Hf(x)v)` away from the pins and to + `(∇f(x), ∇f(y), f(x) − f(y))` on compact separated sets; +- pinned Hessian densities; +- ties to the pinned heights, which are distinct since `kr³ > 0`. + +The same argument with no pins gives `μ(Ω_gen) = 1`. The pinned and tie cases then simply do not occur. So (M3) +is **discharged** for `μ` and for each admissible `Q_r` and `Q_r^W` by an already-accepted source. + +**Corollary R0.** Assume the imports named in §7. Then for each fixed admissible law as above, `Q_r` and `Q_r^W` are +almost surely Morse–Smale. The `Q_r^W` case follows by absolute continuity with density `W_r/Z_r` *with respect to +`Q_r`*, and so only after Theorem P for `Q_r` itself: `Q_r^W` is not absolutely continuous with respect to the +unconditioned law. + +The statement is per fixed law. It gives no common almost-sure set for uncountably many targets, and no uniform +quantitative constants as `r → 0`. No regional or numerical estimate follows. + +For planar gradient flows, Morse–Smale means Morse together with no saddle–saddle connection. Gradient flows have no +periodic orbits, and every other stable/unstable intersection is transverse by dimension. + +## 6. Finite companion + +`transfer_check.py` works in exact rationals on a trigonometric circle model, with value-and-derivative pins at two +Pythagorean points. It checks four things: +1. The pin functionals have full rank on trigonometric polynomials. +2. The corrected approximant satisfies `J_P h = 0` exactly, and its correction is linear in `J_P τ`. +3. Projected covariance images `Π_P Qℓ` lie in `H_P` and reproduce `ℓ` on `H_P`. +4. Enough projected point evaluations span `H_P`. + +Mutants that skip the correction, fail to project or duplicate a pin are rejected. + +## 7. Scope and reading rule + +**Proved here:** +- the classification of §2; +- Theorem P from its stated imports; +- the discharge of (M3) by D1 parent §8. + +**Imports, not reviewed or proved here:** +- R1/R2 (A1; xAI/Harper's slice); +- A2-T and A2-G ([A2], Math-#138), or #137's alternative route; +- (L), the A3–A4 proof announced by OpenAI. + +The literal Fréchet A2-D is neither needed nor claimed. + +No R0 or C103 register change follows until those imports have their own nonauthor verdicts. No novelty claim is +made: parametric transversality for random fields is a known genre, and a planned prior-art search could not run +because the search quota was exhausted. diff --git a/frontiers/sard_g_pinned_transfer_20260929/RESULTS.json b/frontiers/sard_g_pinned_transfer_20260929/RESULTS.json new file mode 100644 index 000000000..5bc72a5f2 --- /dev/null +++ b/frontiers/sard_g_pinned_transfer_20260929/RESULTS.json @@ -0,0 +1,12 @@ +{ + "checks": { + "corrected_approximant_satisfies_pins": true, + "pin_functionals_independent": true, + "projected_images_lie_in_H_P": true, + "projected_point_evaluations_span_H_P": true, + "reproducing_identity_on_H_P": true + }, + "object": "CL-SARD-PINNED-TRANSFER-20260929-v1", + "passed": true, + "scope": "exact finite-dimensional illustrations only" +} diff --git a/frontiers/sard_g_pinned_transfer_20260929/SOURCE_FILES.json b/frontiers/sard_g_pinned_transfer_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..4729e3d9d --- /dev/null +++ b/frontiers/sard_g_pinned_transfer_20260929/SOURCE_FILES.json @@ -0,0 +1,45 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "disposition": "AUTHOR_SIDE_SOURCE_NOTE", + "consumes": [ + { + "id": "RC-S", + "pr": "d6g8k5htny-coder/Math-#135", + "head": "ee94b06368c29bceca80662698b4b4d6ee81ec91", + "path": "frontiers/sard_g_robust_charts_20260929/PROOF.md", + "git_blob": "7e2237063a8dd0120e9d5bd15a3caaa32e8495fa" + }, + { + "id": "A2", + "pr": "d6g8k5htny-coder/Math-#138", + "path": "frontiers/sard_g_a2_regularity_20260929/PROOF.md", + "git_blob": "8ea2c353" + }, + { + "id": "D1-parent-section-8", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7" + } + ], + "files": [ + { + "path": "PROOF.md", + "bytes": 8912, + "sha256": "6cef00efb0e4e3b0cc3a85a0f43468a22b7d2dba1525cd8489d45dfd375667bd", + "git_blob": "314e38c6f5f2bd78da79e423f30a341a3d45e22c" + }, + { + "path": "RESULTS.json", + "bytes": 371, + "sha256": "592698af30550052fc9a6e853473a6e7f502ad775966b0a87fb9a83ccdbbf60c", + "git_blob": "5bc72a5f299261d1220ab74855ab7e9a20a79504" + }, + { + "path": "transfer_check.py", + "bytes": 5695, + "sha256": "62ec8f0cf6bf18eedd7b33068f9077f6ed2719b4dbd5a0a2ee1a1197b3aeabff", + "git_blob": "2a468a1f1400045a058713bb9ccb03f51c9b7aa6" + } + ] +} diff --git a/frontiers/sard_g_pinned_transfer_20260929/transfer_check.py b/frontiers/sard_g_pinned_transfer_20260929/transfer_check.py new file mode 100644 index 000000000..2a468a1f1 --- /dev/null +++ b/frontiers/sard_g_pinned_transfer_20260929/transfer_check.py @@ -0,0 +1,147 @@ +"""Exact companion for CL-SARD-PINNED-TRANSFER-20260929-v1 (PROOF.md). Standard library, exact rationals. + +Circle trigonometric model, modes 0..K with positive rational weights (covariance Sigma = diag(w) in coefficient +coordinates, H inner product _H = a^T Sigma^-1 b). Pins: value and derivative at x_a = theta and x_b = 2 theta, +cos theta = 3/5 (all trigonometric values rational). + RANK the four pin functionals are independent on trigonometric polynomials. + CORRECTION h = tau - sum_i (J tau)_i psi_i with dual psi_i satisfies J h = 0 exactly; the correction is linear in J tau. + PROJECTION Pi_P(Sigma l) lies in H_P (J annihilates it) and _H = l(h) for h in H_P. + SPAN projected point-evaluation images at further Pythagorean points span H_P (dimension 2K+1-4). +Mutants (each must fail): no-correction, unprojected, duplicate-pin. +""" +import argparse +import json +import sys +from fractions import Fraction as F + +MUTANTS = ("no-correction", "unprojected", "duplicate-pin") +MUT = None +K = 3 +N = 2 * K + 1 +W = [F(1)] + [F(1, 2 ** k) for k in range(1, K + 1) for _ in (0, 1)] + + +def angle_pow(m): + c, s = F(1), F(0) + for _ in range(m): + c, s = c * F(3, 5) - s * F(4, 5), s * F(3, 5) + c * F(4, 5) + return c, s + + +def eval_rows(m): + """value and derivative functionals at x = m*theta in coefficient coordinates.""" + c1, s1 = angle_pow(m) + cs, ss = [F(1)], [F(0)] + for _ in range(K): + cs.append(cs[-1] * c1 - ss[-1] * s1) + ss.append(ss[-1] * c1 + cs[-2] * s1) + val, der = [F(1)], [F(0)] + for k in range(1, K + 1): + val += [cs[k], ss[k]] + der += [-k * ss[k], k * cs[k]] + return val, der + + +def matmul(A, B): + return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))] + + +def transpose(A): + return [list(r) for r in zip(*A)] + + +def inverse(A): + n = len(A) + M = [list(A[i]) + [F(int(i == j)) for j in range(n)] for i in range(n)] + for c in range(n): + p = next(i for i in range(c, n) if M[i][c] != 0) + M[c], M[p] = M[p], M[c] + piv = M[c][c] + M[c] = [x / piv for x in M[c]] + for i in range(n): + if i != c and M[i][c] != 0: + f = M[i][c] + M[i] = [x - f * y for x, y in zip(M[i], M[c])] + return [r[n:] for r in M] + + +def rank(rows): + M = [list(r) for r in rows] + rk = 0 + for col in range(len(M[0])): + p = next((i for i in range(rk, len(M)) if M[i][col] != 0), None) + if p is None: + continue + M[rk], M[p] = M[p], M[rk] + for i in range(len(M)): + if i != rk and M[i][col] != 0: + f = M[i][col] / M[rk][col] + M[i] = [x - f * y for x, y in zip(M[i], M[rk])] + rk += 1 + return rk + + +def check(): + out = {} + va, da = eval_rows(1) + vb, db = eval_rows(2) if MUT != "duplicate-pin" else eval_rows(1) + J = [va, da, vb, db] + out["pin_functionals_independent"] = rank(J) == 4 + if not out["pin_functionals_independent"]: + return out + Jt = transpose(J) + # dual trigonometric polynomials psi = J^T (J J^T)^-1 (columns) + Psi = matmul(Jt, inverse(matmul(J, Jt))) + ok = True + for tau in ([F(j + 1, 7) for j in range(N)], [F((-1) ** j * (j + 2), 3) for j in range(N)]): + Jtau = [sum(r[i] * tau[i] for i in range(N)) for r in J] + corr = [sum(Psi[i][c] * Jtau[c] for c in range(4)) for i in range(N)] + h = tau if MUT == "no-correction" else [t - c for t, c in zip(tau, corr)] + ok &= all(sum(r[i] * h[i] for i in range(N)) == 0 for r in J) + # linearity of the correction in J tau + corr2 = [sum(Psi[i][c] * 2 * Jtau[c] for c in range(4)) for i in range(N)] + ok &= all(c2 == 2 * c for c, c2 in zip(corr, corr2)) + out["corrected_approximant_satisfies_pins"] = ok + # projection Pi_P k = k - Sigma J^T (J Sigma J^T)^-1 J k + S = [[W[i] if i == j else F(0) for j in range(N)] for i in range(N)] + G = inverse(matmul(matmul(J, S), Jt)) + SJt = matmul(S, Jt) + + def proj(k): + Jk = [sum(r[i] * k[i] for i in range(N)) for r in J] + coeff = [sum(G[a][b] * Jk[b] for b in range(4)) for a in range(4)] + return [k[i] - sum(SJt[i][a] * coeff[a] for a in range(4)) for i in range(N)] + + ok_in = ok_rep = True + hP = [F(0)] * N + # an element of H_P: correct a generic vector + tau = [F(j * j + 1, 5) for j in range(N)] + Jtau = [sum(r[i] * tau[i] for i in range(N)) for r in J] + hP = [t - sum(Psi[i][c] * Jtau[c] for c in range(4)) for i, t in enumerate(tau)] + for m in (3, 4, 5): + l, _ = eval_rows(m) + Sl = [W[i] * l[i] for i in range(N)] + k = Sl if MUT == "unprojected" else proj(Sl) + ok_in &= all(sum(r[i] * k[i] for i in range(N)) == 0 for r in J) + ok_rep &= sum(hP[i] * k[i] / W[i] for i in range(N)) == sum(l[i] * hP[i] for i in range(N)) + out["projected_images_lie_in_H_P"] = ok_in + out["reproducing_identity_on_H_P"] = ok_rep + imgs = [proj([W[i] * eval_rows(m)[0][i] for i in range(N)]) for m in range(3, 3 + N)] + out["projected_point_evaluations_span_H_P"] = rank(imgs) == N - 4 + return out + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = check() + passed = all(checks.values()) and len(checks) == 5 + print(json.dumps({"object": "CL-SARD-PINNED-TRANSFER-20260929-v1", "checks": checks, "passed": passed, + "scope": "exact finite-dimensional illustrations only"}, indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/frontiers/sard_g_robust_charts_20260929/PROOF.md b/frontiers/sard_g_robust_charts_20260929/PROOF.md new file mode 100644 index 000000000..7e2237063 --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/PROOF.md @@ -0,0 +1,422 @@ +# SARD-G robust charts: a source-level A1/A5/A6 successor + +Object: OA-SARD-ROBUST-CHARTS-20260929-v1. +Author: OpenAI / ChatGPT, 29 September 2026. +Disposition: AUTHOR-SIDE INTERFACE REPAIR; source-bound nonauthor review required. +Scientific effect NONE. The original manuscript, AMEND reviews, STATUS, graph, +lemma flags and prizes are unchanged. This note is not a C103 regional certificate. + +## 1. The downstream defect and the precise replacement contract + +The strict-gradient successor SG, at main commit a1fc9581, correctly excludes +hidden critical points and equality at the gradient margin. Its Conditions 2–3 +still allow an endpoint hit of a finite closed section. The boundary review BR +shows that such a field can belong to a purported chart while arbitrarily close +fields do not. Thus A1's openness assertion fails for that written predicate and +A6 cannot apply its open-interval slicing to it. Harper's standalone RI note +identifies the missing geometric conditions but explicitly does not amend SG. + +This is an explicit alternative chart definition and its associated slicing +proof, not another suggestion to amend the predicate later. It replaces SG +Section 3's chart/first-hit definition, Section 6's countable-direction choice, +and Sections 7–8's application to those charts. It does not rewrite SG Sections +4–5 or claim a new verification of their endpoint-support and RKHS-injectivity +arguments. All source identities are in SOURCE_MAP.json. + +The repaired claims are: + +**R1 (robust first contact).** A finite arc whose FIRST CONTACT with the CLOSED +section is transverse, in its relative interior, after launch and before its +terminal parameter, with positive compact open-tube clearance, has a continuous +first-hit map under C1 arc perturbations. If the parameter-to-arc map is C1, +its hit parameter and hit point are C1 as well. + +**R2 (chart contract, A1).** Under the local-branch continuity premise A2-T below, +the actual chart sets U_chi^rob defined in Section 4 are open in C2, have a +countable index set, and cover every nondegenerate saddle connection by a zero +of their mismatch. If the branch maps satisfy A2-D, that mismatch is C1. + +**R3 (Gaussian directions, A5).** For the C2-valued centered Gaussian field, +rational finite combinations of point evaluations at a fixed countable dense +set supply covariance images dense in its Cameron–Martin space. Normalizing +these gives a countable separating family of Gaussian slicing directions with +an independent residual. Norm separability of the Banach dual is neither used +nor asserted. + +**R4 (conditional application, A6).** If A2-D and the original A3–A4 directional +nonvanishing implication hold on the new charts, the charted connection event +is contained in a Borel Gaussian null set. With a separately justified full- +measure generic set this yields the completed-measure almost-sure conclusion. +No statement that every point of a Gaussian shift line is Morse is required. + +R1 and R3 are proved here. R2 explicitly uses A2-T; the C1 part and R4 explicitly +use A2-D. The statement is not an independent proof of invariant-manifold +parameter regularity, A3–A4, finite-jet nondegeneracy or any regional Kac–Rice +estimate. In particular an accepted R1 does not, by itself, promote C103. + +## 2. Functional setting and the unaltered premises + +Let X=C2(T_L^2) with its separable Banach norm. Let mu be the centered Gaussian +law of the same smooth periodized field, Q:X* -> X its covariance operator, +and H its Cameron–Martin Hilbert space, continuously embedded in X. The smooth +sample-path and Gaussian moment assumptions of SG ensure that Q is defined by +Bochner integration and the reproducing identity below applies. This note uses +no special isotropic rotation of a conditioned field. + +For each pair of rational nested endpoint boxes and continuation neighborhoods, +retain SG's exact critical-point predicate: the CLOSED outer box contains exactly +one critical point, it lies in the interior continuation neighborhood, its index +is one and its spectral gap is greater than a specified positive rational margin. +The gradient minimum on the compact continuation complement is STRICTLY greater +than its specified positive rational threshold eta. The two outer boxes are +compactly disjoint. Equality is not accepted. + +**A2-T, explicit imported topological premise.** Around every field with these +hyperbolic tracked saddles there are open field neighborhoods on which the four +local stable/unstable branch germs have fixed-label embedded C1 parameterizations +on compact intervals, continuously depending on the field in the C1 arc topology. +They represent the full germs near the saddle, not arbitrary selected orbit +pieces. They stay inside their declared endpoint neighborhoods. The regular flow +arcs launched from them depend continuously in C1 on the field on their declared +finite time intervals. Ordinary gradient time may be used; an equivalent +normalized flow is used only on regions with a positive gradient lower bound. + +**A2-D, additional differential premise.** On those neighborhoods the local +parameterizations and finite regular flow maps are C1 in the field parameter and +the arc parameter, so the implicit-function derivative for transverse hitting +is defined on X. A2-T alone is not a differentiability theorem. Any regularity +loss at the C2-field/C1-vector-field interface must be resolved in A2's own +review, not hidden inside the first-hit argument. + +**A3–A4, imported nonvanishing premise.** At a chart zero corresponding to a +connection, the derivative of the mismatch is a continuous linear functional +on X whose restriction to H is nonzero. The original route uses a curve +contribution plus endpoint-supported terms and positivity of Fourier weights. +The endpoint neighborhoods remain disjoint from the compact interior test arc +in the new charts, so the SUPPORT hypothesis is unchanged. This note records +that compatibility but does not independently discharge that route. + +The generic full-measure set of nondegenerate critical points and distinct +critical values is another named input. R4 will state precisely where it is +needed, instead of assuming it for an entire one-dimensional shift line. + +## 3. The finite-section first-contact lemma with the missing early-prefix proof + +Work in a local Euclidean chart near a nondegenerate closed segment +Sigma=[a,b]. Its boundary relative to the supporting line is the two-point set +{a,b}, not its ambient topological boundary, which would be the whole segment. +Write n for a unit normal, and s for a signed coordinate along the supporting +line. Let T be an open tube in the surface. Suppose a C1 embedded arc gamma on +[0,H] is defined on a slightly larger parameter neighborhood when required by +local differentiation, and satisfies: + +(F1) gamma(0) is not in Sigma and the FIRST time tau of contact with the CLOSED + Sigma exists, with 00 so [tau-epsilon,tau+epsilon] lies in (0,H), +gamma on that interval stays in one supporting-line chart and in T, its tangential +coordinate lies a positive distance from both endpoints, and its normal derivative +has constant sign with absolute value bounded below. Its signed normal values at +tau-epsilon and tau+epsilon therefore have opposite signs with positive slack. + +The EARLY PREFIX gamma([0,tau-epsilon]) is compact and disjoint from the CLOSED +segment Sigma. Its distance from Sigma is consequently strictly positive. This +is the step that a phrase such as 'all conditions are strict' does not supply: +the whole travelled arc has zero distance to the section at the hit, so it cannot +be used as a separated prefix. Nor may the closed segment be replaced by relint +in this compact-set argument. + +Small C1 perturbations preserve early-prefix separation, endpoint and tube margins, +the normal derivative's sign and lower bound on the terminal interval, and the +opposite signs at its ends. The intermediate-value theorem gives one zero of the +normal coordinate in this interval; strict monotonicity makes it unique. Its +point lies in the relative interior of Sigma. No earlier contact is possible in +the prefix or in the terminal interval before that zero. Thus the continued zero +is still the first CLOSED contact. Later contacts beyond this interval are +irrelevant to this definition. The positive terminal-time slack ensures that the +continued hit is still inside the declared arc domain. + +The zero and hit point are continuous under C1 arc perturbations. If gamma is +Gamma(f,t) with C1 parameter dependence, the scalar implicit-function theorem +applies to n.(Gamma(f,t)-a), and + + d tau_f[h] = - n.(D_f Gamma(f,tau_f)[h]) + / (n.partial_t Gamma(f,tau_f)). (R1a) + +The hit-point derivative follows by the chain rule. This proves R1 and all its +strict-margin variants. The local terminal argument also persists under small +changes of the finite segment endpoints, a fact used for rational approximation +in the coverage proof. Earlier crossings of the SUPPORTING LINE outside Sigma +are allowed; only actual contacts with Sigma are excluded. QED. + +## 4. The actual successor predicate, including every local branch label + +Fix a countable atlas of local-branch field neighborhoods supplied by A2-T. +Here is why it may be fixed countably without assuming a countable norm-dense +subset of X*: for each choice of rational isolating data, its hyperbolic field +locus is an open subspace of the second-countable space X. The local field +neighborhoods of A2-T form an open cover. A countable subcover exists by Lindelof. +Choose one local-branch chart on each selected neighborhood once and for all, +with a fixed compact parameter interval after shrinking if needed. Products of +the two endpoint atlases and the finite branch labels remain countable. + +This is a countable topological atlas, not a computable enumeration of arbitrary +real fields. It is chosen ONCE, not as a measurable 'first chart' depending on a +random realization. Every field is allowed to belong to multiple charts. + +A label chi consists of one such atlas index; SG's rational isolating boxes, +continuation neighborhoods, strict spectral/gradient margins; branch signs; all +local closed rational sections; a central closed rational segment Sigma; a +finite rational polygonal open tube covering the compact regular travel arcs; +finite rational positive parameter/time horizons; and positive rational lower +clearances and speed/normal-angle margins. Keep the endpoint-support neighborhoods +disjoint from the compact interior test subarc as required by A3. + +Define U_chi^rob to be EXACTLY the set of fields satisfying all of the following: + +(P1) The field belongs to the specified local-branch atlas domain and satisfies + the CLOSED-outer-box uniqueness and STRICT spectral/gradient predicate of + Section 2 for each tracked saddle. +(P2) EVERY local branch-label section is met by its specified compact local + germ arc according to (F1)–(F4), with the declared strict margins. The local + arc parameter is a graph coordinate, not physical time from a stationary + saddle. It may start at the saddle, which lies OFF the local section. + There is no positive-flow-speed requirement at that stationary launch. + Its positive-parameter first section hit defines the regular launch point. +(P3) From these regular launch points, the forward unstable and backward stable + flow arcs are defined through their declared finite horizons. EACH meets + the same central CLOSED Sigma by (F1)–(F4), with strict launch/terminal, + endpoint, open-tube, regular-speed and transverse-normal margins. +(P4) Any other section hit used to specify a branch or mismatch is governed by + the SAME conditions. It is not enough to repair only the central section. + Separation of endpoint neighborhoods from the interior test arc is strict. + +Later returns after a first hit are immaterial. No predicate based on 'the first +relative-interior hit while ignoring earlier closed-boundary contacts' is used. +No degenerate field is admitted by overriding an invalid local predicate after +slicing has begun. A degeneracy elsewhere on the torus need not invalidate this +local chart, and the new definition does not say otherwise. + +On U_chi^rob define the mismatch by the ACTUAL robust first-contact points, + + D_chi(f)=s(z_u(f))-s(z_s(f)), (R2a) + +where s is the fixed signed coordinate on central Sigma. This definition is not +a post hoc restriction of the old possibly discontinuous hit map. + +## 5. Openness and C1 regularity of the defined charts + +For P1 the unique saddle continues in a small ball by the nondegenerate-zero +implicit-function theorem. The gradient has a positive minimum on the rest of +the compact outer box outside that ball; small C1 perturbations cannot create a +new zero there. The saddle stays inside its continuation neighborhood and its +index/spectral gap persist under C2 perturbations. On each fixed compact exclusion +set K, |min_K|grad f|-min_K|grad g||<=||grad f-grad g||_infinity, so a STRICT +margin remains strict. No sampled minimum is being substituted for this argument. + +A2-T supplies the local arcs continuously in C1. R1 first continues every local +section hit and hence both regular launch points. Continuous finite-time flow +dependence then supplies both travel arcs. Apply R1 again to the central hits. +Compact travel speed and tube-clearance minima are continuous under uniform arc +and C1 vector-field convergence; their strict bounds persist. There are finitely +many conditions per chart, so a sufficiently small C2 ball preserves all of them. +Therefore U_chi^rob is open. + +Under A2-D the same applications of (R1a), composition, and the chain rule give +C1 launch points, central hit times/points, and D_chi on U_chi^rob. This C1 conclusion +uses A2-D explicitly; the geometric lemma has not proved invariant-manifold +parameter differentiability. Different overlapping charts need not have identical +mismatch functions away from their connection zeros. The slicing argument only +uses each on its own open domain. + +## 6. Countable coverage still includes every genuine connection + +Fix a nondegenerate saddle-to-saddle gradient connection. Choose compactly +separated rational isolating boxes with each saddle the only zero in its outer +box. Choose rational continuation neighborhoods and smaller rational spectral and +gradient thresholds. The required strict minima exist by compactness. + +Choose atlas neighborhoods containing the field for the corresponding local +germs. On each selected branch, choose a small local section through an interior +point of its regular part, transverse to that branch, lying inside the endpoint +neighborhood. Shrink the segment so the earlier compact local germ prefix avoids +its closure; local monotonicity in a graph coordinate then gives first closed +contact in its relative interior. Extend the local parameter interval a little +past the hit. The same construction applies to every label section required. + +The connection's compact regular arc between these launches is embedded: a +repeated point of a nonstationary orbit would be periodic, while f strictly +increases along ascending gradient time. Choose a small central transverse +segment near an interior point. By shrinking it, the two compact earlier travel +prefixes avoid its closure. Their local transverse crossings are of the same +geometric connection, so they hit the central segment at the same point. +Extend both travel arcs a small positive time past that point, away from the +endpoint neighborhoods. An open tubular neighborhood of the compact travelled +arcs has positive clearance, positive regular speed and a central transverse +normal bound. A finite rational polygonal tube may be chosen within it and +around the arcs; a finite coordinate cover handles torus winding. + +All these properties have strict slack. The proof of R1, with segment endpoints +as additional finite-dimensional parameters, shows that close rational segment +endpoints preserve them. Hence the initially chosen local and central sections +can be replaced by rational ones. Rational horizons and smaller positive rational +margins complete a label chi. The field lies in U_chi^rob, and its mismatch is zero. +Thus + + Connection intersect Omega_gen + subset union_chi {f in U_chi^rob:D_chi(f)=0}. (R2b) + +The index set is countable. No realization is asked to select a first chart, +and no measurable-selection or analytic-projection theorem is needed. + +## 7. Countable Gaussian directions without a norm-dense Banach dual + +Let S={x_n} be a fixed countable dense subset of the torus (rational coordinates +after rescaling by L). Let ell_n be point evaluation at x_n, a continuous linear +functional on X, and k_n=Q ell_n in H. For h in H the covariance/RKHS identity is + + _H=ell_n(h)=h(x_n). (R3a) + +If h is orthogonal to every k_n, it vanishes on S. The embedding H -> C2 implies +continuity, so h vanishes everywhere and is the zero vector. Therefore the real +linear span of {k_n} is dense in H. Rational finite linear combinations are also +dense: approximate finitely many real coefficients by rationals in a fixed finite +sum before approximating h by such sums. + +Enumerate all rational finite combinations ell of the ell_n, remove those with +variance v_ell=ell(Qell)=0, and set + + h_ell=Qell/sqrt(v_ell), + xi_ell=ell(f)/sqrt(v_ell), + g_ell=f-xi_ell h_ell. (R3b) + +The h_ell are dense in the unit sphere of H (or merely a countable separating +family would suffice). This construction needs neither X* norm separability nor +a countable dense family in X*. The old dual-density sentence in SG is replaced, +not treated as an extra unproved assumption. + +The scalar xi_ell is standard Gaussian. For any a in X*, + + Cov(a(f),xi_ell)=a(Qell)/sqrt(v_ell)=a(h_ell), + Cov(a(g_ell),xi_ell)=0. (R3c) + +The pair (g_ell,xi_ell) is jointly Gaussian since it is a continuous linear image +of f. The vanishing cross-covariances imply independence. This Banach-valued +independence can be checked on a countable separating family of derivative +point-evaluations and then extended to the Borel sigma algebra. Indeed C2 norm +balls are generated by derivative evaluations of orders at most two on S using +suprema on the countable dense set. No probability measure on a nonseparable +norm-dual is introduced. + +Because H embeds continuously in X, D_chi'(f)|_H is continuous. If it is nonzero, +it cannot vanish on the dense h_ell family. Thus at every charted connection +satisfying the A3–A4 premise, at least one direction has + + D_chi'(f)[h_ell] != 0. (R3d) + +This proves the needed A5 direction/decomposition statement for the new source. +It does not prove A3–A4's nonvanishing premise. + +## 8. A6 applied to these charts, not to an uncorrected predecessor + +Assume A2-D and the A3–A4 premise. For each fixed chi and ell define + + B_chi,ell={f in U_chi^rob:D_chi(f)=0, + D_chi'(f)[h_ell]!=0}. (R4a) + +This is Borel: U_chi^rob is open, and both scalar functions are continuous there. +Fix a residual g in (R3b). The validity set + + I_g={t in R:g+t h_ell in U_chi^rob} + +is open and is a countable disjoint union of open intervals. On each interval +F_g(t)=D_chi(g+t h_ell) is C1. At every zero contributing to B_chi,ell, F_g'(t) is +nonzero. The scalar inverse/implicit-function theorem makes that zero isolated +among the zeros in its interval. Such a subset of R is countable: each point can +be assigned a rational-endpoint isolating interval containing no other zero. +Accumulation at singular zeros or at interval boundaries is allowed and does +not destroy this countability argument. + +The conditional scalar law is standard Gaussian, by the INDEPENDENT residual +construction, so it charges that countable set with probability zero for every +fixed g. The inverse image of (R4a) under (g,t)->g+t h_ell is Borel, so Tonelli +applies to the residual law times the scalar Gaussian law. Hence mu(B_chi,ell)=0. +By (R2b) and (R3d), + + Connection intersect Omega_gen subset union_chi,ell B_chi,ell. + +The union is countable and Borel null. If the connection event itself has not +separately been proved Borel, its immediate conclusion is outer measure zero, +and it is measurable and null in the completed Gaussian probability space. +With the separate assumption mu(Omega_gen)=1 this gives the conditional almost- +sure conclusion. Fields outside Omega_gen along a shift line are not assumed +absent; only the open validity intervals and their regular zeros are used. + +This completes A6's application to the actual successor predicate, CONDITIONAL +on the inputs explicitly stated above. The full C103 or any downstream regional +estimate still requires its own premise and review chain. + +## 9. Boundary examples that the new predicate actually excludes + +The BR torus example is F(x,y)=sin(2pi x)(2-cos(2pi y)). Its two saddles on y=0 +are connected; central Sigma={(1,y):0<=y<=1/200} is first hit at its lower endpoint. +All the old strict speed, gradient and angle margins can hold. Vertical field +translation moves the branch below the segment. The new P3 excludes the unshifted +field because F2 fails. This does not exclude the connection from the UNION of +new charts: a central segment with endpoints on opposite sides of the hit and +smaller positive margins supplies a valid chart. + +Simply replacing the closed segment by its relative interior is not enough. +For a concrete smooth embedded arc on 0<=t<=5/2, use + + gamma_eps(t)=((t-1)(t-2),(t-1)^2+eps), + Sigma={(0,y):0<=y<=2}. + +At eps=0 there is a transverse endpoint contact at t=1 and an interior contact +at t=2. A rule that ignores the first contact and asks only for the first INTERIOR +hit chooses t=2. For every small positive eps it chooses t=1 instead. The arcs +converge in C1, yet that rule is discontinuous. Our F1 sees the earlier closed +contact and F2 rejects its endpoint at eps=0. This is a geometric first-hit +counterexample, not a newly asserted gradient connection on the torus. + +The launch and terminal slacks are independently necessary. On gamma(t)=(t-1,1/2) +for 0<=t<=1, the hit is transverse and interior but at terminal time; shifting +x slightly negative makes it miss the section on that domain. An arc starting +on the section has first contact at zero and is likewise excluded. Compact tube +clearance must include the whole prefix, not merely its hit: a path can leave a +tube and return before a good transverse hit. Every local label is checked, since +a discontinuous local launch would invalidate even a well-behaved central hit. + +## 10. What the finite controls can and cannot establish + +The standard-library program tests rational piecewise-affine paths against a +closed vertical segment and an open rectangular tube. It certifies only that +finite model and is deliberately stricter at polyline corners than the smooth +lemma: its transverse hit must lie inside one affine piece. It neither samples +an ODE nor certifies arbitrary fields' gradient minima, stable manifolds or +infinite-dimensional chart membership. + +Tests exercise the real endpoint/earlier-contact/terminal/tube/local-label +failures, strict scalar gradient margins, rational moving-hit models, the smooth +polynomial first-interior counterexample, exact finite Gaussian covariance +splitting, finite evaluation rank, and exclusion of singular slicing zeros. +Semantic mutants independently remove each important condition. The tests do +not substitute for R1's compact-prefix argument, the infinite-dimensional RKHS +density proof, A2 regularity or the Tonelli measurability argument. + +The current proof is an additive source-level alternative. Independent review +must decide the R1/R2/R3/R4 claims at their exact dependency scope. Publishing it, +passing its tests or merging it as a candidate does not flip the predecessor's +AMEND, assert an independently closed A2–A4 chain, or promote C103. diff --git a/frontiers/sard_g_robust_charts_20260929/README.md b/frontiers/sard_g_robust_charts_20260929/README.md new file mode 100644 index 000000000..c4746231f --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/README.md @@ -0,0 +1,30 @@ +# SARD-G: the missing robust first-contact source application + +Author-side interface repair, nonauthor analytic review required. Scientific effect NONE. + +[PROOF.md](PROOF.md) supplies an actual successor predicate at every local and +central section. It proves first CLOSED contact persistence using an early compact +prefix and a transverse terminal interval, retains endpoint/time/open-tube margins, +and supplies countable chart coverage. The original AMEND texts are untouched. + +It also replaces the unneeded norm-dense Banach-dual construction by rational +finite combinations of dense point evaluations, whose covariance images are dense +in the Cameron–Martin space. Gaussian independence and Borel/regular-zero slicing +are then proved on the corrected charts. + +A2-T (local-branch continuity) and A2-D (C1 parameter regularity) are DISTINCT named +premises. The conditional slicing conclusion also needs the original A3–A4 +nonvanishing input and the separate generic full-measure input. This packet does +not certify those inputs, any C103 regional estimate, RN/JETMOD or a 3D theorem. + +Run from this directory: + + python -B -S verify.py --output /path/to/new-output + python -B -O -S verify.py --output /path/to/other-new-output + +Each invocation runs 19 finite tests and rejects 8 semantic mutants in BOTH modes. +The polyline checker is a finite illustration, not a numerical field-membership +algorithm; hits at polyline corners are deliberately not certified. No sampled +gradient minimum is asserted to be a continuum certificate. The executable +verifies this exact flat source packet but does not fetch or replay upstream +proofs. SOURCE_MAP.json pins those separately read sources. diff --git a/frontiers/sard_g_robust_charts_20260929/RECONNAISSANCE.md b/frontiers/sard_g_robust_charts_20260929/RECONNAISSANCE.md new file mode 100644 index 000000000..4be5c9d34 --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/RECONNAISSANCE.md @@ -0,0 +1,25 @@ +# Dependency-focused reconnaissance — 29 September 2026 + +The exact SG/BR/RI project sources were read through the GitHub connector. The +new source applies Harper's geometric proposal and supplies the missing early- +prefix proof; it does not claim invention of transverse-hit persistence, RKHS +reproducing identities, Gaussian regression, Lindelof countability or Tonelli. + +Primary-source records read in this pass: + +- Martin Hairer, An Introduction to Stochastic PDEs, arXiv:0907.4178v2 (2023 + revision). https://arxiv.org/abs/0907.4178 . Abstract and version record only, + not a full-text theorem import. The direction/decomposition proof is displayed + directly in this packet rather than inferred from that abstract. +- C. M. Judd, P. Collins, B. Krauskopf, H. M. Osinga, Tangency bifurcations of + global Poincare maps, University of Bristol working-paper record (2007). + https://research-information.bris.ac.uk/en/publications/tangency-bifurcations-of-global-poincare-maps/ + Abstract-level context: global sections can give discontinuous or undefined + return maps despite the local transverse theorem. Its full proof was not read + and no claim here is imported from it. + +The broader search also located MIT's Poincare-section lecture notes, but those +notes were not consumed at theorem level. No new Consensus call was made in this +pass; the preceding pass recorded its monthly quota limit. None of these discovery +records is represented as a new analytic review, exhaustive novelty audit, or +proof of invariant-manifold differentiability at the exact C2 topology. diff --git a/frontiers/sard_g_robust_charts_20260929/RESULTS.json b/frontiers/sard_g_robust_charts_20260929/RESULTS.json new file mode 100644 index 000000000..76c28f9fb --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/RESULTS.json @@ -0,0 +1,8 @@ +{ + "tests_per_mode": 19, + "semantic_mutants_per_mode": 8, + "identical_output_pairs": 9, + "all_intended_failures": true, + "scientific_effect": "NONE", + "continuum_proof_verified_by_code": false +} diff --git a/frontiers/sard_g_robust_charts_20260929/SOURCE_FILES.json b/frontiers/sard_g_robust_charts_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..a2f72b0cf --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/SOURCE_FILES.json @@ -0,0 +1,53 @@ +{ + "schema": 1, + "files": [ + { + "path": "PROOF.md", + "bytes": 25022, + "sha256": "b91b9f792c6322204a0f2a573b2ca76d5c951e49ddd7caa6ffd1abed0aa79e79", + "git_blob": "7e2237063a8dd0120e9d5bd15a3caaa32e8495fa" + }, + { + "path": "README.md", + "bytes": 1693, + "sha256": "71e5a4c08e9daa08e331e735a3e7f8c0409da0d4821b70cdd65b573a0d46a387", + "git_blob": "c4746231fa43e1ccd754e2d5f3277b5e268e7aea" + }, + { + "path": "RECONNAISSANCE.md", + "bytes": 1577, + "sha256": "f6aeb058052b74a5ef00e893b383b1da9cab78e2e2a95174d9c57f8eca9cbfaa", + "git_blob": "4be5c9d348d884a75bff3f75026f97c530b4a86b" + }, + { + "path": "RESULTS.json", + "bytes": 201, + "sha256": "29c96c87073f800fd9104914ab3b2d0625b03bb28ec935ad1b8e09c6704d12ae", + "git_blob": "76c28f9fbe16ba456e431f8dc0866042bc6ee8d4" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 1644, + "sha256": "f248f92eca8cfd39f56ff26b23512be4fb14855105e45888d92a13586a5bd03f", + "git_blob": "bcf52b3cd64ab80f7338776888a996f6a6061d1f" + }, + { + "path": "charts.py", + "bytes": 4931, + "sha256": "99270bf5959a8534eb53306f572843a3c8d1e89bb669b68bce1a70621aaae74f", + "git_blob": "4096b52c98ae54a8d02753688584d3b2c83a72bc" + }, + { + "path": "test_charts.py", + "bytes": 4515, + "sha256": "8b03e49bc885c6bbac392e4bcf23bbf6a2ba20684856eb0bb10b83cec8214644", + "git_blob": "79a28fe42be24cb17512b01c240384ff5f555f8b" + }, + { + "path": "verify.py", + "bytes": 4688, + "sha256": "4f0b32879d1502dfdb95b3892e5e7cfa91a7deb3b8e6974e0d98021238791064", + "git_blob": "d83f30056f3453f077a68bc120bf63b3fc1aa64e" + } + ] +} diff --git a/frontiers/sard_g_robust_charts_20260929/SOURCE_MAP.json b/frontiers/sard_g_robust_charts_20260929/SOURCE_MAP.json new file mode 100644 index 000000000..bcf52b3cd --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/SOURCE_MAP.json @@ -0,0 +1,39 @@ +{ + "scientific_effect": "NONE", + "sources": [ + { + "id": "SG", + "repository": "d6g8k5htny-coder/main", + "commit": "a1fc9581291b6f81c76c903c96a13955b51f8d54", + "path": "research/q0/sard_g/SARD_G_EXECUTION_REPAIR_20260925.md", + "git_blob": "8f86e0c9ef91fde473e2344a3e461c31f63f8529", + "use": "Explicit predecessor predicate and conditional A2–A4; new source replaces chart/direction/slicing application, not the original file." + }, + { + "id": "BR", + "repository": "d6g8k5htny-coder/main", + "commit": "f43f243c54e12c63fc2c23c89c5b2998766f21b7", + "path": "reviews/sard_g_successor_a1_a6_20260926/REVIEW.md", + "git_blob": "9fc61b47c2b4c4bcc3898a6c61a6dcf9cbe1d136", + "use": "Exact AMEND, endpoint and early-contact boundaries, completed-measure qualification, and no dual-separability assumption." + }, + { + "id": "RI", + "repository": "d6g8k5htny-coder/Math-", + "commit": "0b0b281989db62ccf3ff5e1327df6f9efda073ea", + "path": "incoming/grok-cycle4-20260926/harper/SARD_G_A1_RELATIVE_INTERIOR_LEMMA.md", + "git_blob": "0ee24f953a4402e58c97ac6d3897eb80d17513a9", + "use": "Harper robust first-interior-hit proposal, now explicitly applied in P1–P4 with a full early-prefix proof." + } + ], + "unproved_here": [ + "A2-T local branch C1-arc continuity", + "A2-D C1 dependence in C2 field topology", + "A3–A4 directional nonvanishing", + "generic full-measure premise", + "C103 regional Kac–Rice estimates" + ], + "upstream_bytes_locally_replayed": false, + "new_nonauthor_review_required": true, + "existing_status_changed": false +} diff --git a/frontiers/sard_g_robust_charts_20260929/charts.py b/frontiers/sard_g_robust_charts_20260929/charts.py new file mode 100644 index 000000000..4096b52c9 --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/charts.py @@ -0,0 +1,112 @@ +"""Exact finite first-contact and Gaussian-slicing illustrations. + +Polyline controls are stricter than the smooth-arc theorem: a certified hit must +lie inside a single affine piece. This is not a numerical ODE or SARD-G verifier. +""" +from fractions import Fraction as F + +MUTANT=None + +def _data(path, section): + pts=[tuple(F(v) for v in p) for p in path] + lo,hi=map(F,section) + if len(pts)<2 or any(len(p)!=3 for p in pts) or not lo=q[0] for p,q in zip(pts,pts[1:])): + raise ValueError('path times must start at zero and increase strictly') + return pts,lo,hi + +def closed_contacts(path,section): + """All first-contact candidates with the CLOSED vertical segment x=0.""" + pts,lo,hi=_data(path,section);hits=[] + for i,(p,q) in enumerate(zip(pts,pts[1:])): + t0,x0,y0=p;t1,x1,y1=q + if x1!=x0: + u=-x0/(x1-x0) + if 0<=u<=1 and lo<=y0+u*(y1-y0)<=hi: + hits.append(dict(time=t0+u*(t1-t0),height=y0+u*(y1-y0), + speed=(x1-x0)/(t1-t0),interior_piece=0margin:return False + if MUTANT!='allow-terminal' and not pts[-1][0]-tau>margin:return False + endpoint_ok= min(height-lo,hi-height)>margin + if MUTANT=='allow-endpoint':endpoint_ok=min(height-lo,hi-height)>=margin + if not endpoint_ok:return False + inside_piece=h['interior_piece'] + if MUTANT=='allow-terminal' and tau==pts[-1][0]:inside_piece=True + if not inside_piece or not abs(h['speed'])>margin:return False + prefix=[(p[1],p[2]) for p in pts if p[0]margin for x,y in prefix):return False + return True + +def chart_hits(paths,section,tube): + paths=list(paths) + if not paths:raise ValueError('at least one declared hit required') + if MUTANT=='skip-local':paths=paths[-1:] + return all(robust_hit(p,section,tube) for p in paths) + +def gradient_slack(minimum,eta): + minimum,eta=F(minimum),F(eta) + if eta<=0:raise ValueError('positive exclusion threshold required') + return minimum>=eta if MUTANT=='nonstrict-gradient' else minimum>eta + +def gaussian_split(Q,a): + """Rational unstandardized form: xi=a.F, b=Qa/Var(xi), g=F-b xi.""" + a=list(map(F,a));Q=[list(map(F,row)) for row in Q];n=len(a) + if n==0 or len(Q)!=n or any(len(row)!=n for row in Q): + raise ValueError('matching square covariance and vector required') + if any(Q[i][j]!=Q[j][i] for i in range(n) for j in range(n)): + raise ValueError('symmetric covariance required') + v=[sum((Q[i][j]*a[j] for j in range(n)),F(0)) for i in range(n)] + var=sum((a[i]*v[i] for i in range(n)),F(0)) + if var<=0:raise ValueError('positive scalar variance required') + b=[x/var for x in v] + R=[[Q[i][j]-(0 if MUTANT=='leave-covariance' else v[i]*v[j]/var) + for j in range(n)] for i in range(n)] + return var,b,R + +def rank(A): + M=[list(map(F,row)) for row in A] + if not M:return 0 + if any(len(row)!=len(M[0]) for row in M):raise ValueError('rectangular matrix required') + k=0 + for j in range(len(M[0])): + pivot=next((i for i in range(k,len(M)) if M[i][j]),None) + if pivot is None:continue + M[k],M[pivot]=M[pivot],M[k] + z=M[k][j];M[k]=[v/z for v in M[k]] + for i in range(k+1,len(M)): + z=M[i][j];M[i]=[v-z*w for v,w in zip(M[i],M[k])] + k+=1 + if k==len(M):break + return k + +def regular_zero(coefficients,x): + coeff=list(map(F,coefficients));x=F(x) + value=sum((a*x**i for i,a in enumerate(coeff)),F(0)) + deriv=sum((i*coeff[i]*x**(i-1) for i in range(1,len(coeff))),F(0)) + return value==0 and (True if MUTANT=='count-singular-zero' else deriv!=0) diff --git a/frontiers/sard_g_robust_charts_20260929/test_charts.py b/frontiers/sard_g_robust_charts_20260929/test_charts.py new file mode 100644 index 000000000..79a28fe42 --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/test_charts.py @@ -0,0 +1,104 @@ +"""Exact finite illustrations. They do not verify any infinite-dimensional premise.""" +from fractions import Fraction as F +import unittest +import charts as c + +SECTION=(F(0),F(1)) +TUBE=(-3,3,-2,3) +GOOD=[(0,-1,F(1,2)),(2,1,F(1,2))] + +class ChartTests(unittest.TestCase): + def test_endpoint_hit_excluded(self): + self.assertFalse(c.robust_hit([(0,-1,0),(2,1,0)],SECTION,TUBE)) + + def test_earlier_endpoint_not_hidden_by_later_interior(self): + path=[(0,-1,-1),(2,1,1),(3,1,F(1,2)),(5,-1,F(1,2))] + self.assertFalse(c.robust_hit(path,SECTION,TUBE)) + self.assertEqual(c.closed_contacts(path,SECTION)[0]['time'],1) + + def test_terminal_hit_excluded(self): + self.assertFalse(c.robust_hit([(0,-1,F(1,2)),(1,0,F(1,2))],SECTION,TUBE)) + + def test_launch_on_section_excluded(self): + self.assertFalse(c.robust_hit([(0,0,F(1,2)),(2,1,F(1,2))],SECTION,TUBE)) + + def test_compact_prefix_tube_clearance(self): + path=[(0,-1,F(1,2)),(1,-1,4),(2,-1,F(1,2)),(4,1,F(1,2))] + self.assertFalse(c.robust_hit(path,SECTION,TUBE)) + + def test_tube_boundary_excluded(self): + path=[(0,-3,F(1,2)),(4,1,F(1,2))] + self.assertFalse(c.robust_hit(path,SECTION,TUBE)) + + def test_strict_gradient_threshold(self): + self.assertFalse(c.gradient_slack(F(1),F(1))) + self.assertTrue(c.gradient_slack(F(3,2),F(1))) + + def test_transverse_corner_not_certified(self): + path=[(0,-1,F(1,2)),(1,0,F(1,2)),(2,-1,F(1,2))] + self.assertFalse(c.robust_hit(path,SECTION,TUBE)) + + def test_robust_interior_family(self): + for eps in [F(i,100) for i in range(-20,21)]: + p=[(0,-1,F(1,2)+eps),(2,1,F(1,2)+eps)] + self.assertTrue(c.robust_hit(p,SECTION,TUBE)) + self.assertEqual(c.closed_contacts(p,SECTION)[0]['time'],1) + + def test_hitting_time_continuity_model(self): + for eps in (F(-1,8),F(0),F(1,8)): + p=[(0,-1+eps,F(1,2)),(2,1+eps,F(1,2))] + self.assertTrue(c.robust_hit(p,SECTION,TUBE)) + self.assertEqual(c.closed_contacts(p,SECTION)[0]['time'],1-eps) + + def test_earlier_collinear_contact_excluded(self): + p=[(0,0,-1),(2,0,1),(3,1,F(1,2)),(5,-1,F(1,2))] + self.assertFalse(c.robust_hit(p,SECTION,TUBE)) + self.assertEqual(c.closed_contacts(p,SECTION)[0]['time'],1) + + def test_relative_interior_only_time_jumps(self): + # Smooth embedded gamma(t)=((t-1)(t-2),(t-1)^2+eps), roots at1,2. + for eps in (F(0),F(1,100),F(1,10000)): + interior=[t for t in (1,2) if 0<(t-1)**2+eps<2] + self.assertEqual(min(interior),2 if eps==0 else 1) + self.assertEqual(min(t for t in (1,2) if 0<=(t-1)**2+eps<=2),1) + + def test_gaussian_residual_orthogonality(self): + Q=[[F(2),F(1)],[F(1),F(3)]];a=[F(1),F(2)] + var,b,R=c.gaussian_split(Q,a) + self.assertEqual(var,18) + self.assertEqual(sum(x*y for x,y in zip(a,b)),1) + self.assertEqual([sum(row[j]*a[j] for j in range(2)) for row in R],[0,0]) + for i in range(2): + for j in range(2): + self.assertEqual(R[i][j]+var*b[i]*b[j],Q[i][j]) + + def test_degenerate_gaussian_direction_rejected(self): + with self.assertRaises(ValueError):c.gaussian_split([[1,1],[1,1]],[1,-1]) + + def test_distinct_evaluations_span_polynomials(self): + for n in range(1,7): + V=[[F(i)**j for j in range(n)] for i in range(n)] + self.assertEqual(c.rank(V),n) + self.assertEqual(c.rank(V+[V[0]]),n) + + def test_regular_zeros_only(self): + # p(t)=t(t-1)^2; the zero at1 has derivative0. + self.assertTrue(c.regular_zero([0,1,-2,1],0)) + self.assertFalse(c.regular_zero([0,1,-2,1],1)) + self.assertFalse(c.regular_zero([0,1,-2,1],2)) + + def test_all_local_sections_checked(self): + bad=[(0,-1,0),(2,1,0)] + self.assertFalse(c.chart_hits([bad,GOOD],SECTION,TUBE)) + self.assertTrue(c.chart_hits([GOOD,GOOD],SECTION,TUBE)) + + def test_positive_quantitative_margins(self): + self.assertTrue(c.robust_hit(GOOD,SECTION,TUBE,margin=F(1,4))) + self.assertFalse(c.robust_hit(GOOD,SECTION,TUBE,margin=F(1,2))) + + def test_invalid_path_and_section(self): + with self.assertRaises(ValueError):c.robust_hit([(0,-1,0),(0,1,0)],SECTION,TUBE) + with self.assertRaises(ValueError):c.robust_hit(GOOD,(1,0),TUBE) + with self.assertRaises(ValueError):c.robust_hit(GOOD,SECTION,TUBE,margin=F(-1)) + +if __name__=='__main__':unittest.main() diff --git a/frontiers/sard_g_robust_charts_20260929/verify.py b/frontiers/sard_g_robust_charts_20260929/verify.py new file mode 100644 index 000000000..d83f30056 --- /dev/null +++ b/frontiers/sard_g_robust_charts_20260929/verify.py @@ -0,0 +1,95 @@ +"""Verify exact packet membership, both Python modes and intended semantic failures.""" +import argparse +import hashlib +import io +import json +from pathlib import Path +import subprocess +import sys +import unittest + +ROOT=Path(__file__).resolve().parent +MUTANTS={ + 'allow-endpoint':'test_endpoint_hit_excluded', + 'ignore-earlier-closed':'test_earlier_endpoint_not_hidden_by_later_interior', + 'allow-terminal':'test_terminal_hit_excluded', + 'skip-tube':'test_compact_prefix_tube_clearance', + 'skip-local':'test_all_local_sections_checked', + 'nonstrict-gradient':'test_strict_gradient_threshold', + 'leave-covariance':'test_gaussian_residual_orthogonality', + 'count-singular-zero':'test_regular_zeros_only', +} + +def require(ok,message): + if not ok:raise ValueError(message) + +def decode(text): + def unique(pairs): + d={} + for k,v in pairs: + require(k not in d,'duplicate JSON key: '+k);d[k]=v + return d + return json.loads(text,object_pairs_hook=unique) + +def identity(path): + require(path.is_file() and not path.is_symlink(),'regular source required') + data=path.read_bytes() + return dict(bytes=len(data),sha256=hashlib.sha256(data).hexdigest(), + git_blob=hashlib.sha1(f'blob {len(data)}\0'.encode()+data).hexdigest()) + +def sources(): + identity(ROOT/'SOURCE_FILES.json') + rows=decode((ROOT/'SOURCE_FILES.json').read_text())['files'] + names=[row['path'] for row in rows] + require(len(names)==len(set(names)) and all(Path(n).name==n and n!='SOURCE_FILES.json' for n in names), + 'unique flat manifest paths required') + require(sorted(p.name for p in ROOT.iterdir())==sorted(names+['SOURCE_FILES.json']), 'source membership differs') + for row in rows: + require(identity(ROOT/row['path'])=={k:row[k] for k in ('bytes','sha256','git_blob')}, + 'source identity differs: '+row['path']) + return {p.name:identity(p) for p in sorted(ROOT.iterdir())} + +def child(mutant): + import charts,test_charts + charts.MUTANT=mutant + result=unittest.TextTestRunner(stream=io.StringIO()).run(unittest.defaultTestLoader.loadTestsFromModule(test_charts)) + print(json.dumps(dict(tests=result.testsRun,passed=result.wasSuccessful(), + failures=sorted(t.id().rsplit('.',1)[-1] for t,_ in result.failures), + errors=sorted(t.id().rsplit('.',1)[-1] for t,_ in result.errors)),sort_keys=True)) + return 0 if result.wasSuccessful() else 1 + +def replay(out): + out=out.resolve() + require(not out.exists() and not out.is_relative_to(ROOT),'new output outside packet required') + before=sources();out.mkdir(parents=True);records={} + for case in ['baseline',*MUTANTS]: + pair=[] + for mode,flags in [('normal',[]),('optimized',['-O'])]: + cmd=[sys.executable,'-B',*flags,'-S',str(ROOT/'verify.py'),'--child'] + if case!='baseline':cmd+=['--mutant',case] + run=subprocess.run(cmd,capture_output=True,timeout=30) + (out/(case+'_'+mode+'.stdout')).write_bytes(run.stdout) + (out/(case+'_'+mode+'.stderr')).write_bytes(run.stderr) + obj=decode(run.stdout.decode()) + require(not run.stderr and not obj['errors'],'execution error: '+case) + require(obj['tests']==19,'wrong test count') + if case=='baseline':require(run.returncode==0 and obj['passed'] and not obj['failures'],'baseline failed') + else:require(run.returncode==1 and not obj['passed'] and MUTANTS[case] in obj['failures'], + 'intended semantic assertion absent: '+case) + pair.append(run.stdout) + require(pair[0]==pair[1],'Python modes disagree: '+case) + records[case]=decode(pair[0].decode()) + summary=dict(tests_per_mode=19,semantic_mutants_per_mode=8,identical_output_pairs=9, + all_intended_failures=True,scientific_effect='NONE',continuum_proof_verified_by_code=False) + require(summary==decode((ROOT/'RESULTS.json').read_text()),'stored summary differs') + require(before==sources(),'source changed during replay') + (out/'REPORT.json').write_text(json.dumps(dict(summary=summary,cases=records,source_identities=before),indent=2,sort_keys=True)+'\n') + print(json.dumps(summary,indent=2,sort_keys=True)) + return 0 + +if __name__=='__main__': + p=argparse.ArgumentParser(description=__doc__);g=p.add_mutually_exclusive_group(required=True) + g.add_argument('--child',action='store_true');g.add_argument('--output',type=Path) + p.add_argument('--mutant',choices=MUTANTS);a=p.parse_args() + require(a.child or a.mutant is None,'mutant requires child mode') + raise SystemExit(child(a.mutant) if a.child else replay(a.output)) diff --git a/reviews/d5_punctured_pin_continuum_claude_20260929/RESULTS.json b/reviews/d5_punctured_pin_continuum_claude_20260929/RESULTS.json new file mode 100644 index 000000000..b1b98cfdf --- /dev/null +++ b/reviews/d5_punctured_pin_continuum_claude_20260929/RESULTS.json @@ -0,0 +1,14 @@ +{ + "checks": { + "FRAME": true, + "MEAN": true, + "NORMALIZER": true, + "REFLECTION": true, + "REGIONS": true, + "TAYLOR": true, + "TRIANGLE": true + }, + "object": "CLAUDE-REVIEW-D5-PUNCTURED-PIN-CONTINUUM-20260929-v1", + "passed": true, + "scope": "exact finite identities only; the Gaussian and Kac-Rice steps are reviewed in REVIEW.md" +} diff --git a/reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md b/reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md new file mode 100644 index 000000000..4904e3d92 --- /dev/null +++ b/reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md @@ -0,0 +1,150 @@ +# Nonauthor analytic record: D5 punctured-pin continuum steps (P2) + +Scientific effect: **NONE**. This record changes no register, status, graph node, proof-index entry, lemma flag, prize +or source. Integration is a separate act by a non-Claude lane. + +## Why this record exists + +- **Only committed record.** The committed nonauthor record for this source, `reviews/d5_punctured_pin_nonauthor_20260928/` + (xAI/Grok, #111), accepts the algebraic skeleton (P4), (P9), (P17) and the (P20) power count. It keeps the continuum + steps on **HOLD**: the Schur floor behind (P10), the density (P11), the conditional moment (P12) and Kac–Rice (P18), + hence (P2). +- **Unrecorded verdict.** My analytic review of the same bytes, posted on #105 on 2026-09-28 + ([5872932723](https://github.com/d6g8k5htny-coder/Math-/pull/105#issuecomment-5872932723), with the runner replay + [5872950920](https://github.com/d6g8k5htny-coder/Math-/pull/105#issuecomment-5872950920)), confirmed every requested + interface. It was never committed as a review record. +- **Downstream consumption.** Later records consume (P2) as an accepted input: + - the scaled-ball corollary C2 in `reviews/d5_collar_count_20260928/`; + - the (I5) synthesis in `reviews/d5_i5_planar_f_20260928/` and in my `reviews/d5_intermediate_window_claude_20260928/`; + - the row "P2 | recorded ACCEPT" in `reviews/d5_consumption_bridge_20260928/BRIDGE.md`, which cites the author source + itself. +- **What this record is.** It closes that record gap. It commits the 2026-09-28 verdict, re-derived on 2026-09-29 at + unchanged bytes, with a new exact companion. It is **not** a second independent review; the reviewer is the same. + +## Object and exposure + +| Field | Value | +|---|---| +| Object | OA-D5-PUNCTURED-PIN-20260928-v1 (OpenAI / ChatGPT), `reviews/d5_local_collar_20260928/PUNCTURED_PIN_PROOF.md` | +| Bytes | 23771 B, SHA256 `f972e50bc07674ebce9d971d1a1bd4dba2f8036dde37ecb57d8a44a35650f76a`, blob `d8acf0bcb9025b1562c03c077c8e0094ae282060` | +| Heads | Reviewed at #105 head `b9fdaea096c4ea136507722641727beb96cc69ce`; re-verified on Math- `main` `dbccbb41a58f2328b3bec6c4609a4b8fb3ac811f`. The bytes are identical. | +| Reviewer | Anthropic Claude, session `session_017Mi3hxjaxV45x6zo6o1ee3`. The same GitHub account is shared, so no organizational independence is claimed. | +| Exposure | My #104 contains a parallel pin-disk derivation: the angle-free triangle bound (T3), which is the device of (P17), and the same Cauchy–Binet constant `9/131072`. My intermediate-window review consumes C2. So this is not a blind review. **I do not count my own vote on (P17)**; its acceptance rests on Grok's #111. | +| Own checks | `pp_continuum_check.py`: exact identities under the continuum steps, 7 groups, 5 mutants, identical under `-O`. | +| Author controls | `run_pin_validation.py`, replayed 2026-09-29: rc 0, and the report equals `PIN_RESULTS.json`. It was also replayed on 2026-09-28 at `b9fdaea`, where all 6 mutations were rejected in both modes. | + +## Verdicts + +| Step | Verdict | +|---|---| +| §3 endpoint regression: `E_r` invertibly equivalent to the six pins, target `e = (b,0,0,0,−12k,0)`, `E_r − E_0 = O_{L^s}(r)`, jet positivity, uniform `C^m` moments under `Q_r` | **ACCEPT** | +| §4 (P4)–(P7) relative remainders | **ACCEPT** (agrees with #111 on (P4)) | +| §5 (P8)–(P10): the error ratios `R = O_{L^s}(r)`, the Schur floor for `Cov_{Q_r}(J)` and the `L²` perturbation giving `c_0 I ≤ Σ ≤ C_0 I` | **ACCEPT**. This lifts #111's HOLD on the Schur/compactness step. | +| §6 (P11) density `≤ C r^{−3} Δ^{−2} e^{−cχ²}` | **ACCEPT** | +| §6 (P12) `E_{Q_r}[K^6 | ∇f(X) = 0] ≤ C(1 + χ^6)` | **ACCEPT** | +| §7 (P13)–(P14) `Z_r ≥ c_Z r²` | **ACCEPT** | +| §8 (P15)–(P16) angle-sensitive product | **ACCEPT** | +| §8 (P17) angle-free product | Not voted (exposure). ACCEPT stands from #111. | +| §9 (P18) weighted Kac–Rice at the fixed zero level | **ACCEPT** | +| §10 (P19)–(P20) regions, puncture exhaustion; §10.1 reflection to `S` | **ACCEPT** | +| **(P2)** `E_{Q_r^W} N_j(M + rE) ≤ C r³|E|` for Borel `E ⊂ D`, and the `S` version | **ACCEPT, existential.** No numerical `C` or `r_*`. Uniform in `b`, `k`, frame, `j` and `E`, for fixed `T` and compact marks. | + +No defect was found. + +## Hand re-derivations of the formerly held steps + +**Schur floor (P10).** +- The ten functionals `E_0 = (f, f_x, f_z, f_xx, −f_xxx, f_xz)(M)` and `J = (f_xxxx, f_xxz, f_zz, f_xzz)(M)` are distinct + one-site monomials. By the lattice-polynomial argument of §3 their joint covariance is positive definite. It is + continuous on the compact `O(2)`, so its least eigenvalue has a uniform positive lower bound. +- `E_r → E_0` in `L²` uniformly. So `Cov((E_r, J))` stays uniformly positive definite for small `r`, and so does its + Schur complement `Cov_{Q_r}(J)`. +- Then `Cov(BJ) = B Cov_{Q_r}(J) Bᵀ ≥ λ_min σ_min(B)² I`. Here (P9) and the bounded trace give `σ_min(B)² ≥ det/tr`. +- For a unit `v`, `sd(v·Y) ≥ sd(v·BJ) − ‖v·(R − ER)‖_2`, with the second term `O(r)`. This gives (P10). + +**Error ratios (P8).** +- `r²|p|/Δ ≤ r` and `r|q|/Δ ≤ r` use `Δ ≥ r|p|` and `Δ ≥ |q|`. +- The terms `r|p|q²` and `r|q|³` need `Δ ≥ |q|`: they give `r|p||q|` and `rq²`. +- For `ε_2`, `r|pq|/Δ ≤ r|p|` and `rq²/Δ ≤ r|q|`. +- The companion checks all six ratios exactly, including both axes. + +**Density (P11).** +- `∇f(X) = diag(r²Δ, rΔ) Y`, so the Jacobian is `r³Δ²`. +- The Gaussian density of `Y` at 0 is at most `C exp(−|m_Y|²/(2C_0))`, with `m_Y = d + O(1)`. +- `|m_Y|² ≥ |d|²/2 − O(1)` and `|d| = 6k|p||p − 1|/Δ ≥ (9k_−/2)χ`. + +**Conditional moment (P12).** +- Conditioning on `∇f(X) = 0` is conditioning on `Y = 0`. The regression replaces `f` by `m_f − CΣ^{−1}m_Y + R_f`, with + `R_f` independent of `Y`. +- `‖CΣ^{−1}‖_{C³}` is bounded, by Cauchy–Schwarz, the §3 moments and (P10). `E‖R_f‖^6_{C³}` is bounded by Minkowski. +- The mean is `O(1 + |d|) = O(1 + χ)`. +- `K ≤ C(1 + ‖f‖_{C³})` dominates both the Hessian supremum and its Lipschitz constant on the triangle. + +**Normalizer (P14).** +- From (P4)–(P5): `g''(0) = −6kr + O(r²)`, `g''(r) = 6kr + O(r²)`, `f_xz = h' = O(r)` at both pins, and + `f_zz(S) = S_0 + O(r)`. +- On `S_0 ∈ [−2, −1]`, with every error at most `k_−`: + - `H_M` is negative definite with `det/r ≥ 5k_−`; + - `H_S` is indefinite with `|det|/r ≥ 5k_−` (companion, exact corners). +- The error events have probability `O(r^s)` by Markov, and `Q_r(S_0 ∈ [−2, −1]) ≥ p_0` uniformly. Hence + `Z_r ≥ (p_0/2)(5k_−r)²`. + +**Kac–Rice (P18).** +- On compact sets excluding `M` and `S`, the six pin functionals and `∇f(X)` sit at three distinct sites. They are + independent by Fourier uniqueness plus localized test functions, so the covariance of `∇f(X)` under `Q_r` is positive + definite. `Q_r` is a (non-centred) Gaussian regression law with smooth paths. +- The mark `W_r · 1{H_X nonsingular of index j}` is lower semicontinuous: `F_j` is continuous through singular matrices, + and the index set is open. It depends on the field at the zero and at two fixed sites. +- This is the same interface as D1 parent §9 (AAL arXiv:2304.07424v3, Thm 7.1 with an additional Gaussian mark, + extended by monotone approximation), which is accepted in the D1 reconciliation. +- Dividing by `Z_r` gives the intensity under `Q_r^W`. + +**Regions (P19)–(P20).** +- *Region I.* `χ² = t²/(1 + r²t²) ∈ [t²/2, t²]` and `q²/Δ² ≤ 1`, so + `ρ ≤ C r (1 + t²)³ (1 + t^6) e^{−ct²/2}`. +- *Region II.* `χ² ∈ [1/(2r²), 1/r²]` and `(p² + q²)/Δ² ≤ 2/r²`, so `ρ ≤ C r^{−10} e^{−c/(2r²)} ≤ C' r²`. + - The angle-sensitive (P16) would be unbounded on the axis (companion mutant `angle-sensitive-axis`). That is why (P17) + is used there. +- *Integration.* `dX = r² dp dq`, and monotone convergence over compact punctures gives (P2). + +**Reflection (§10.1).** `b̃ = b − kr³` and `k̃ = −k` give `b̃ − k̃r³ = b`. Only `|k|` enters the mean penalty. `Z_r` +and the mark are the original random variables with their factors relabelled. Determinants and negative indices are +reflection-invariant. + +## Consequence map (no register change; for the integrating lane) + +| D5 piece | Reviewed source after this record | +|---|---| +| Inner pin disks, all heights, both endpoints (P2) | this record + #111 (algebra, (P17)) | +| Collar C1 on `C(η, R)` and the scaled ball C2 minus pins | `reviews/d5_collar_count_20260928/` (C2 = P2 + C1) | +| Intermediate window (I3), (I4) | `reviews/d5_i5_planar_f_20260928/` (xAI) and `reviews/d5_intermediate_window_claude_20260928/` | +| Remote window, D4 Theorem A | `frontiers/remote_window_20260924/PROOF.md` (reviewed) | +| Global window first moment (I5) `E_{Q^W} N_{I_r}(T² ∖ {M,S}) ≤ C r³` and planar `P(A_r) ≍ r³` | the two I5 records above, now with every input committed as reviewed | + +- **Stale navigation.** + - The main `STATUS.md` D5 row says: "the inner microdisk bound and collar to the reviewed annulus are not complete, + and the claimed summed pin-neighborhood bound remains AMEND". + - The first two D5 bullets of `PROOF_INDEX.md` ("pin neighborhoods" and "intermediate scale") predate these records. + - All three read as stale navigation. +- **Still open, not touched here.** + - The shrinking multiple-witness collision near the pins (a factorial-moment estimate; the third D5 bullet and catalog + C6); + - numerical constants; + - uniformity in `T` and as `k ↓ 0`; + - elder pairing. +- Any STATUS, PROOF_INDEX or GRAPH change is for a non-Claude lane to make after its own check. + +## Notes + +- **n1.** #111's "(P2) HOLD" remains a true statement of what #111 checked. This record does not edit it. +- **n2.** The (P8) sentence "the other terms … have the same bound" is correct but needs `Δ ≥ |q|` for the two cubic + terms. It is spelled out above. +- **n3.** In (P16) the constant 1 is loose (the displayed factors multiply to 1/2), as the source itself says. +- **n4.** (P2) counts critical points of every index at all heights, with the pin excluded. It supplies no height + window, so (I5)'s window is carried by (I4), not by (P2). + +## Reproduce + + python -B -S pp_continuum_check.py # prints RESULTS.json byte for byte + python -B -O -S pp_continuum_check.py # identical + python -B -S pp_continuum_check.py --mutant M # exit 1 for each of the 5 mutants diff --git a/reviews/d5_punctured_pin_continuum_claude_20260929/SOURCE_FILES.json b/reviews/d5_punctured_pin_continuum_claude_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..fa36cd123 --- /dev/null +++ b/reviews/d5_punctured_pin_continuum_claude_20260929/SOURCE_FILES.json @@ -0,0 +1,39 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW_RECORD", + "record_of": { + "comments": [ + "d6g8k5htny-coder/Math-#105 issuecomment-5872932723", + "d6g8k5htny-coder/Math-#105 issuecomment-5872950920" + ], + "reviewed_head": "b9fdaea096c4ea136507722641727beb96cc69ce", + "reverified_on_main": "dbccbb41a58f2328b3bec6c4609a4b8fb3ac811f" + }, + "reviewed_object": { + "path": "reviews/d5_local_collar_20260928/PUNCTURED_PIN_PROOF.md", + "bytes": 23771, + "sha256": "f972e50bc07674ebce9d971d1a1bd4dba2f8036dde37ecb57d8a44a35650f76a", + "git_blob": "d8acf0bcb9025b1562c03c077c8e0094ae282060" + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 10501, + "sha256": "124c472cc064ba24021cb4bb8da1002836a4ce26c8df506228f5c20609f6575a", + "git_blob": "4904e3d929d6dc7bc16b49eee85d7c3a21b6b484" + }, + { + "path": "RESULTS.json", + "bytes": 357, + "sha256": "599e21c525ad0aec7938d94f80f7771bd8e14aeb9ae1b0a60ba434428496c464", + "git_blob": "b1b98cfdf15992736dd54f258afe26dde3d76baf" + }, + { + "path": "pp_continuum_check.py", + "bytes": 10012, + "sha256": "57bc87d11271b47ebccec6ea73abf823fa90e3a8c3c7d7cd2165bdc6f7e4175c", + "git_blob": "b0d6321f7e480d7ea855a2017532588d241f5d34" + } + ] +} diff --git a/reviews/d5_punctured_pin_continuum_claude_20260929/pp_continuum_check.py b/reviews/d5_punctured_pin_continuum_claude_20260929/pp_continuum_check.py new file mode 100644 index 000000000..b0d6321f7 --- /dev/null +++ b/reviews/d5_punctured_pin_continuum_claude_20260929/pp_continuum_check.py @@ -0,0 +1,220 @@ +"""Exact companion for the continuum review of OA-D5-PUNCTURED-PIN-20260928-v1 (PUNCTURED_PIN_PROOF.md). + +Standard library, exact rationals. It checks the finite identities on which the reviewed continuum steps rest: + TAYLOR (P4)/(P5): pin identities of the cubic + quartic interpolant, the 2x2 system giving u''(0) = O(r^3) and + u'''(0) = O(r^2) (scaled solution independent of r), the leading derivative terms, and the P5 cubic model. + FRAME (P8)/(P9): Cauchy-Binet for the 2x3 block, |a|,|b|,|c| floors attained at p = 1/4, and the Gram floor + 9/131072 on a rational grid of p and Pythagorean (alpha, beta) including both axes; the error ratios + r^2|p|/Delta, r|q|/Delta, r|p|q^2/Delta, r|q|^3/Delta, r|pq|/Delta, r q^2/Delta are <= r. + MEAN (P11): |d| >= (9 k_-/2) chi, since |p - 1| >= 3/4 on |p| <= 1/4. + NORMALIZER (P13)/(P14): on S_0 in [-2, -1] with errors <= k_-, H_M is negative definite, H_S indefinite, and both + |det|/r >= 5 k_-. + TRIANGLE (P16)/(P17): coordinate area identity, sine at C = r sigma / ell, r^4 d^2/sigma^4 = r^6 q^2 (1+t^2)^3, + and r d^2 = r^3 (p^2+q^2). + REGIONS (P19)/(P20): chi^2 in [t^2/2, t^2] and q^2/Delta^2 <= 1 in Region I; chi^2 in [1/(2r^2), 1/r^2] and + (p^2+q^2)/Delta^2 <= 2/r^2 in Region II; the Region II spatial factor stays bounded by 2/r^2 on the axis, + while the angle-sensitive factor q^2 (1+t^2)^3 / Delta^2 would be unbounded there; power ledger -10 + 12 = 2. + REFLECTION §10.1 targets: tilde b - tilde k r^3 = b; determinants and negative indices invariant under reflection. +Mutants (each must fail): wrong-a-floor, drop-minor, angle-sensitive-axis, same-sign-k, absolute-remainder. +""" +import argparse +import json +import sys +from fractions import Fraction as F + +MUTANTS = ("wrong-a-floor", "drop-minor", "angle-sensitive-axis", "same-sign-k", "absolute-remainder") +MUT = None +RS = (F(1, 10), F(1, 100), F(1, 1000)) +PS = [F(k, 40) for k in range(-10, 11)] +PYTH = [(F(1), F(0)), (F(0), F(1)), (F(3, 5), F(4, 5)), (F(-4, 5), F(3, 5)), (F(5, 13), F(-12, 13)), + (F(-8, 17), F(-15, 17)), (F(20, 29), F(21, 29)), (F(-1), F(0))] + + +def poly_eval(c, x): + return sum(ci * x ** i for i, ci in enumerate(c)) + + +def poly_der(c): + return [i * c[i] for i in range(1, len(c))] + + +def poly_mul(a, b): + out = [F(0)] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + out[i + j] += x * y + return out + + +def poly_add(a, b): + n = max(len(a), len(b)) + return [(a[i] if i < len(a) else 0) + (b[i] if i < len(b) else 0) for i in range(n)] + + +def check_taylor(): + ok = True + for r in RS: + for b, k, A4 in ((F(1), F(1, 2), F(3)), (F(-2), F(2), F(-5, 7))): + H = [b, F(0), -3 * r * k, 2 * k] # b + k(2x^3 - 3 r x^2) + Q = poly_mul(poly_mul([F(0), F(1)], [F(0), F(1)]), poly_mul([-r, F(1)], [-r, F(1)])) # x^2 (x-r)^2 + g = poly_add(H, [A4 / 24 * c for c in Q]) + dg = poly_der(g) + ok &= poly_eval(g, 0) == b and poly_eval(dg, 0) == 0 # pins at M + ok &= poly_eval(g, r) == b - k * r ** 3 and poly_eval(dg, r) == 0 + for p in (F(1, 4), F(-1, 4), F(1, 7), F(-1, 1000)): + lead = 6 * k * r ** 2 * p * (p - 1) + r ** 3 * A4 / 12 * p * (p - 1) * (2 * p - 1) + ok &= poly_eval(dg, r * p) == lead + # u = A x^2/2 + B x^3/6 + remainder: u(r) = e1 = r^5 E1, u'(r) = e2 = r^4 E2 => A/r^3, B/r^2 independent of r + E1, E2 = F(2, 3), F(-5, 4) + e1, e2 = r ** 5 * E1, r ** 4 * E2 + det = (r * r / 2) * (r * r / 2) - (r ** 3 / 6) * r + A = ((r * r / 2) * e1 - (r ** 3 / 6) * e2) / det + B = (-r * e1 + (r * r / 2) * e2) / det + scale = 1 if MUT == "absolute-remainder" else r ** 3 + ok &= A / scale == 6 * E1 - 2 * E2 and B / r ** 2 == -12 * E1 + 6 * E2 + # (P5) cubic model h = h1 x + T3 x^2/2 + c3 x^3 with h(0) = h(r) = 0 + T3, c3 = F(3, 2), F(-7, 3) + h1 = -T3 * r / 2 - c3 * r * r + for p in (F(1, 4), F(-1, 5), F(1, 1000)): + x = r * p + h = h1 * x + T3 * x * x / 2 + c3 * x ** 3 + ok &= h - r * r / 2 * p * (p - 1) * T3 == c3 * r ** 3 * p * (p * p - 1) + return ok + + +def abc(p): + a = (p - 1) * (2 * p - 1) / 12 + return a, (p - 1) / 2, p - F(1, 2) + + +def check_frame(): + ok = True + a4, b4, c4 = abc(F(1, 4)) + floor_a = F(1, 24) if MUT == "wrong-a-floor" else F(1, 32) + ok &= a4 == floor_a and b4 == -F(3, 8) and c4 == -F(1, 4) + for p in PS: + a, b, c = abc(p) + ok &= abs(a) >= floor_a and abs(b) >= F(3, 8) and abs(c) >= F(1, 4) + for al, be in PYTH: + q = F(1, 16) * be + B = [[a * al, c * be, F(0), q / 2 * be], [F(0), b * al, be, F(0)]] + m12, m13, m23 = a * b * al * al, a * al * be, c * be * be + B3 = [row[:3] for row in B] + gram3 = [[sum(x * y for x, y in zip(u, v)) for v in B3] for u in B3] + det3 = gram3[0][0] * gram3[1][1] - gram3[0][1] * gram3[1][0] + ok &= det3 == m12 ** 2 + m13 ** 2 + m23 ** 2 + gram = [[sum(x * y for x, y in zip(u, v)) for v in B] for u in B] + det4 = gram[0][0] * gram[1][1] - gram[0][1] * gram[1][0] + lower = m12 ** 2 if MUT == "drop-minor" else m12 ** 2 + m23 ** 2 + ok &= det4 >= det3 >= lower >= F(9, 131072) + for r in RS: + for p, q in ((F(1, 4), F(0)), (F(0), F(1, 4)), (F(1, 1000), F(-1, 7)), (F(-1, 5), F(1, 10 ** 6))): + D2 = q * q + r * r * p * p + for num in (r * r * abs(p), r * abs(q), r * abs(p) * q * q, r * abs(q) ** 3, r * abs(p * q), r * q * q): + ok &= num * num <= r * r * D2 + return ok + + +def check_mean(): + km = F(1, 3) + ok = True + for p in PS: + if p == 0: + continue + for q in (F(0), F(1, 9), F(-1, 5)): + r = F(1, 100) + D2 = q * q + r * r * p * p + d2 = (6 * km * p * (p - 1)) ** 2 / D2 + chi2 = p * p / D2 + ok &= d2 >= (F(9, 2) * km) ** 2 * chi2 + return ok + + +def check_normalizer(): + ok = True + for km, kp in ((F(1, 2), F(2)), (F(1), F(1))): + for k in (km, kp): + for S0 in (F(-2), F(-3, 2), F(-1)): + for e in (-km, km): + fxx_M = -6 * k + e + detM = -6 * k * S0 + e + detS = 6 * k * S0 + e + ok &= fxx_M < 0 and detM > 0 and detS < 0 + ok &= detM >= 5 * km and -detS >= 5 * km + return ok + + +def check_triangle(): + ok = True + for r in RS: + for p, q in ((F(1, 5), F(1, 7)), (F(-1, 4), F(1, 100)), (F(0), F(1, 4)), (F(1, 1000), F(-1, 3))): + A, Bp, C = (F(0), F(0)), (r, F(0)), (r * p, r * q) + d2 = C[0] ** 2 + C[1] ** 2 + l2 = (Bp[0] - C[0]) ** 2 + (Bp[1] - C[1]) ** 2 + area2 = ((Bp[0] - A[0]) * (C[1] - A[1]) - (Bp[1] - A[1]) * (C[0] - A[0])) ** 2 / 4 + sig2 = q * q / (p * p + q * q) + ok &= area2 == r * r * d2 * sig2 / 4 # angle at A + sigC2 = r * r * sig2 / l2 + ok &= area2 == d2 * l2 * sigC2 / 4 # angle at C: sin = r sigma / ell + t2 = (p / q) ** 2 + ok &= r ** 4 * d2 / sig2 ** 2 == r ** 6 * q * q * (1 + t2) ** 3 + ok &= r * d2 == r ** 3 * (p * p + q * q) + return ok + + +def check_regions(): + ok = True + for r in (F(1, 10), F(1, 100)): + for p in PS: + for q in (F(1, 4), F(1, 40), F(1, 10 ** 4), F(1, 10 ** 8), F(0)): + if p == 0 and q == 0: + continue + D2 = q * q + r * r * p * p + chi2 = p * p / D2 + if q != 0 and q * q >= r * r * p * p: # Region I + t2 = (p / q) ** 2 + ok &= t2 / 2 <= chi2 <= t2 and q * q <= D2 + elif q * q < r * r * p * p: # Region II + ok &= 1 / (2 * r * r) <= chi2 <= 1 / (r * r) + spatial = (p * p + q * q) / D2 + if MUT == "angle-sensitive-axis" and q != 0: + spatial = q * q * (1 + (p / q) ** 2) ** 3 / D2 + ok &= spatial <= 2 / (r * r) + ok &= -2 - 3 + 3 - 2 - 6 == -10 and -10 + 12 == 2 + return ok + + +def check_reflection(): + ok = True + for b, k, r in ((F(1), F(1, 2), F(1, 10)), (F(-3), F(2), F(1, 100))): + bt = b - k * r ** 3 + kt = k if MUT == "same-sign-k" else -k + ok &= bt - kt * r ** 3 == b and abs(kt) == k + R = [[F(-1), F(0)], [F(0), F(1)]] + for H in ([[F(-2), F(1, 3)], [F(1, 3), F(-1)]], [[F(1), F(2)], [F(2), F(-1)]], [[F(3), F(-1)], [F(-1), F(2)]]): + Hr = [[sum(R[i][a] * H[a][b2] * R[j][b2] for a in range(2) for b2 in range(2)) for j in range(2)] + for i in range(2)] + det = H[0][0] * H[1][1] - H[0][1] ** 2 + detr = Hr[0][0] * Hr[1][1] - Hr[0][1] ** 2 + ok &= det == detr and H[0][0] + H[1][1] == Hr[0][0] + Hr[1][1] + return ok + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = {"TAYLOR": check_taylor(), "FRAME": check_frame(), "MEAN": check_mean(), + "NORMALIZER": check_normalizer(), "TRIANGLE": check_triangle(), "REGIONS": check_regions(), + "REFLECTION": check_reflection()} + passed = all(checks.values()) and len(checks) == 7 + print(json.dumps({"object": "CLAUDE-REVIEW-D5-PUNCTURED-PIN-CONTINUUM-20260929-v1", "checks": checks, + "passed": passed, + "scope": "exact finite identities only; the Gaussian and Kac-Rice steps are reviewed in REVIEW.md"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/reviews/sard_closure_integration_20260929/HARPER_REVIEW_RECORD.md b/reviews/sard_closure_integration_20260929/HARPER_REVIEW_RECORD.md new file mode 100644 index 000000000..7ab2033d9 --- /dev/null +++ b/reviews/sard_closure_integration_20260929/HARPER_REVIEW_RECORD.md @@ -0,0 +1,74 @@ +# Editorial record of Harper's R1/R2 review + +Recorded by OpenAI / ChatGPT, 29 September 2026. Scientific effect NONE. +This is an attributed editorial SUMMARY of a published xAI/Harper discussion +review, not an original Harper manuscript, not a verbatim archival capture, and +not another independent OpenAI verdict. No execution is claimed by this document. + +Source: Math-#135, comment 5890799898, read in its updated pickup-plus-verdict +form on 29 September 2026: +https://github.com/d6g8k5htny-coder/Math-/pull/135#issuecomment-5890799898 + +The reviewed source is fixed at ee94b06368c29bceca80662698b4b4d6ee81ec91, +`frontiers/sard_g_robust_charts_20260929/PROOF.md`, blob +`7e2237063a8dd0120e9d5bd15a3caaa32e8495fa`, SHA256 +`b91b9f792c6322204a0f2a573b2ca76d5c951e49ddd7caa6ffd1abed0aa79e79`. +A Git commit pins these repository bytes, not the mutable discussion body. + +## Attributed verdict and limits + +Harper accepts R1 and the geometric R2 argument under imported A2-T. The C1 +mismatch conclusion belongs to A2-D and is not independently proved by Harper. +Graph coordinates are understood as fixed with the field atlas, consistently +with #137 v2. No source amendment, scientific-register change or C103 promotion +is authorized by that verdict. Claude's separate second-provider review adds +evidence rather than replacing or cancelling Harper's completed slice. + +## Recorded reasoning + +The entire travelled arc meets the section, so it cannot serve as a compact +separated set. The early prefix ending strictly before the first contact is +compact and disjoint from the CLOSED section. Its positive distance persists +under small C1 perturbations. Relative interior alone is not a closed set and +would not justify that separation step. + +The explicit family gamma_eps(t)=((t-1)(t-2),(t-1)^2+eps), tested against the +vertical segment 0<=y<=2, has an endpoint contact at t=1 and a later interior +contact at t=2 when eps=0. Ignoring the earlier endpoint makes a first-interior +selection jump under perturbation. Requiring the first CLOSED contact to lie +in the relative interior rejects that bad boundary parameter. + +On a short terminal interval about a valid hit, the normal derivative retains +one sign and is bounded away from zero. The continued normal zero is unique. +The early-prefix separation excludes prior contacts; terminal-time slack keeps +the hit inside the arc domain. The scalar implicit-function derivative is then +the derivative of the true first-contact time, not merely a later crossing. + +A local branch uses a graph coordinate fixed with the atlas. Physical gradient +flow from its saddle anchor is stationary, so a positive physical-speed condition +must not be imposed there. The first local-section contact defines the regular +launch. P2 applies the robust conditions to every local label section, P3 to +both central contacts, and P4 to any other section used in the mismatch. + +Second countability of C2 and a once-chosen Lindelof subcover give a countable +local field atlas. No first-chart measurable selector is introduced. Strictly +monotone f along a connecting gradient orbit gives embedded compact regular +arcs. Small local and central sections avoid the earlier compact prefixes; +rational approximations of endpoints, horizons and margins preserve strict +slack. This proves countable coverage of each genuine connection. + +## Exposure and finite-control boundary + +Harper authored the earlier RI proposal at +`incoming/grok-cycle4-20260926/harper/SARD_G_A1_RELATIVE_INTERIOR_LEMMA.md`, +blob `0ee24f953a4402e58c97ac6d3897eb80d17513a9`. The new review corroborates that +prior input's source-level application, not independent truth of Harper's own +RI proposal. All lanes share one GitHub account; organizational independence +is not claimed. + +Harper correctly distinguishes the finite polyline controls, which reject +corner hits, from the smooth-arc proof. Their successful hosted run is not an +analytic proof. The already merged Claude R3/R4 review remains conditional on +R2 openness. The completed R1/R2 review supplies its geometric layer; #137 v2 +supplies the separately reviewed regularity layer. No regional, quantitative +or conditional-law conclusion is inferred from geometry alone. diff --git a/reviews/sard_closure_integration_20260929/READING_RULE.md b/reviews/sard_closure_integration_20260929/READING_RULE.md new file mode 100644 index 000000000..6860b19b1 --- /dev/null +++ b/reviews/sard_closure_integration_20260929/READING_RULE.md @@ -0,0 +1,119 @@ +# Reviewed qualitative SARD chain: integration reading rule + +Integrator: OpenAI / ChatGPT, 29 September 2026. +Scientific effect NONE. This is a source/review integration, not a new scientific +register, a registry transition, or an independent proof-assistant alignment. + +## Exact integrated heads + +- Base: dbccbb41a58f2328b3bec6c4609a4b8fb3ac811f (already merged R3/R4 record). +- Robust charts #135: ee94b06368c29bceca80662698b4b4d6ee81ec91. +- Corrected A2 and qualitative closure #137: aacb962c8bd5d324231b4757fe3049264a20a7f3. +- Claude source/reviews #138: 6fce8d2089478d0e46d9d79e148ce6b97e08d5a6. + +All three source heads remain ancestors. Their original files, including the +withdrawn #137 v1, are preserved byte for byte. The full comparison against the +base must contain only additions. No original SG/AMEND body, STATUS, PROOF_INDEX, +GRAPH, lemma flag, premise or prize is changed by this integration. + +## One complete mathematical route, not mutually assumed premises + +1. Use the ACTUAL robust first-CLOSED-contact P1-P4 predicate in + `frontiers/sard_g_robust_charts_20260929/PROOF.md`, blob + 7e2237063a8dd0120e9d5bd15a3caaa32e8495fa. Every local and central section is + covered; margins, terminal slack and compact early-prefix separation matter. + Reviews: Harper 5890799898 (editorially recorded here), and Claude's complete + `reviews/sard_g_r1r2_claude_20260929/REVIEW.md`. +2. Read the graph axes as fixed with each atlas neighborhood. The A2 premise is + supplied by `frontiers/sard_g_a2_parameter_20260929/v2/A2_FIXED_FRAME.md`, + blob 09c45efbde38f81bc152e30ba4b4a51a37c9272b. It proves joint Frechet C1 + EVALUATION and continuous C1 arc dependence using unweighted bounded backward + trajectories. It does NOT assert differentiability into the C1 arc norm. + The old moving-eigenframe proof is withdrawn and is not consumed. +3. The companion `v2/NONVANISHING_AND_CLOSURE.md`, blob + 7da6a393cabc08063e68587b6e4007c39baba38f, supplies localized scalar-potential + variation, the hit-time projection, Fourier nonvanishing, genericity and + countable Gaussian slicing. Its small supported C2 bump can be smoothed in + the same open support neighborhood, as its Section 3 explicitly states. + Claude's `reviews/sard_g_a2_fixed_frame_claude_20260929/REVIEW.md` accepts the + corrected A2 and companion arguments with their geometric dependency. +4. R3/R4 may be consumed from the already merged + `reviews/sard_g_r3r4_claude_20260929/REVIEW.md`, with its stated dependencies + now supplied by steps 1-3. Alternatively the companion's independent Fourier + coordinates give the displayed equivalent ending. Neither route assumes + every field along a slicing line is Morse. +5. For PINNED laws use `frontiers/sard_g_pinned_transfer_20260929/PROOF.md`, + blob 314e38c6f5f2bd78da79e423f30a341a3d45e22c, with TRANSFER_REVIEW.md here. + Project the Cameron-Martin space to the common kernel of all value/gradient + pins, approximate the supported perturbation with EXACT finite jet correction, + and slice on that affine support. The deterministic mean is in the residual. + Only then transfer to the determinant tilt via absolute continuity relative + to the pinned law, not the unconditioned law. +6. Genericity for the admissible original two-pin laws is the exact D1 parent + Section 8, blob dfed3b8d318a3ab1950957f393307733a4bef3f2, SHA256 + 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7. + The general finite-pin Theorem P retains Q(Omega_gen)=1 as a hypothesis. + +The topology proof consumes only continuity of branches, which the corrected A2 +proof establishes without robust-hit geometry. Its later robust-hit application +uses R1. Hence this ordering is not a circular proof of branch existence and +chart openness. Claude's diagnostic Lemma J and alternate A2-G reduction remain +credited. Its citation-only manifold argument is not used to fill an unproved +step in this selected route. + +## Result and exclusions + +The assembled, source-reviewed qualitative result is: the unconditioned planar +periodized field is almost surely Morse with distinct critical values and no +saddle-saddle gradient connection. The same holds for each fixed admissible +original two-pin law and its original full determinant tilt. Thus their planar +gradient flows are almost surely Morse-Smale, in the completed-measure sense. + +Admissible pin sites are distinct on the torus, the gap is positive, and the +parameters lie in the named parent validity regime or a separately proved +extension. The theorem is per fixed law. It is not one common probability-one +set for all uncountably many targets, and provides no uniform quantitative +constants as the pins coalesce. Arbitrary pinned means still need their own +Q(Omega_gen)=1 hypothesis. + +No regional C103 estimate, numerical normalizer floor, C103/R0 Boolean transition, +RN/JETMOD closure, P0.1 release, three-dimensional Morse-Smale result, quantitative +near-connection rate, or global multi-witness factorial upper bound follows from +this source integration alone. Consumer status updates require a separate exact +object/measure/radius reading and the existing byte-tracked dependency mechanism. + +## D5 review-record completion included at the peer's request + +The same #138 head also adds +`reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md`, blob +4904e3d929d6dc7bc16b49eee85d7c3a21b6b484. It commits/re-derives Claude's earlier +#105 analytic review of unchanged PUNCTURED_PIN_PROOF.md, blob +d8acf0bcb9025b1562c03c077c8e0094ae282060, SHA256 +f972e50bc07674ebce9d971d1a1bd4dba2f8036dde37ecb57d8a44a35650f76a. +It is NOT a second independent reviewer. Claude declines a new vote on the +angle-free P17 device because of authorship exposure; its separate xAI acceptance +remains the input. The original xAI record's narrower HOLD is not overwritten. + +The new committed record makes the previously discussion-only continuum review +available to existing collar/intermediate/global-first-moment consumers. Its +all-height pin-disk first moment is not a shrinking multiple-witness factorial +bound. Historical STATUS/navigation sentences may need a later scoped refresh, +but this integration changes none of those rows and claims no numerical constant. +The integrator read the complete P2 source and review; this is source-exposed +consistency checking, not another foundational vote. + +## Verification and lineage + +The integrator freshly replayed the exact transfer checker in both Python modes: +five predicates pass, three semantic mutants fail the intended predicate, four +stdout pairs identical, stderr empty. See TRANSFER_REVIEW.md for its exact blob. +This is not a local full checkout of every author/reviewer package. All combined +source, author, reviewer and required downstream/formal checks must be observed +on the current integration head before an ordinary expected-head merge. Old +separate-head success, a quota notice or a mere task pickup is not that evidence. + +Existing scalar Lean execution does not formalize the entire SARD proof. Exact +byte hashes certify identity, not analytic correctness. A separately authenticated +alignment review remains distinct. Shared-account/provider/dependency exposure is +preserved in each record. No paused external process, timer or private workspace +publication is part of this work. diff --git a/reviews/sard_closure_integration_20260929/SOURCE_FILES.json b/reviews/sard_closure_integration_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..df013436c --- /dev/null +++ b/reviews/sard_closure_integration_20260929/SOURCE_FILES.json @@ -0,0 +1,24 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "files": [ + { + "path": "HARPER_REVIEW_RECORD.md", + "bytes": 4202, + "sha256": "be65705f2755b272aa0c3596d40d822904da57d763791e312233e2fef95f165d", + "git_blob": "7ab2033d9b66cfcf9c18819a041df88a051b994f" + }, + { + "path": "READING_RULE.md", + "bytes": 7320, + "sha256": "65a1037f270b22fc776ac4fb85484b118fe9c8d79f1036ac6c70045180e2a744", + "git_blob": "6860b19b1bc9a426a7fa627952b6221bd9c00618" + }, + { + "path": "TRANSFER_REVIEW.md", + "bytes": 8811, + "sha256": "15e633aeb59671dfb570921039e9b7629ceb3585054def4edde03df6624530a8", + "git_blob": "387aab73370b31f67fad6778b716751798718597" + } + ] +} diff --git a/reviews/sard_closure_integration_20260929/TRANSFER_REVIEW.md b/reviews/sard_closure_integration_20260929/TRANSFER_REVIEW.md new file mode 100644 index 000000000..387aab733 --- /dev/null +++ b/reviews/sard_closure_integration_20260929/TRANSFER_REVIEW.md @@ -0,0 +1,158 @@ +# Review of the pinned SARD-G transfer and its admissible-law composition + +Reviewer: OpenAI / ChatGPT, 29 September 2026. +Scientific effect NONE. This is a source-bound mathematical review and reading +record, not a scientific-status register or a new independence vote. + +## Object, exact sources, and exposure + +Reviewed object: Claude's CL-SARD-PINNED-TRANSFER-20260929-v1, clarified version v2, +`frontiers/sard_g_pinned_transfer_20260929/PROOF.md` at +`c460a8035994032e47dc464254d352c95c40ad36`, unchanged at selected integration head +`6fce8d2089478d0e46d9d79e148ce6b97e08d5a6`. +Its blob is `314e38c6f5f2bd78da79e423f30a341a3d45e22c`, 8912 bytes, SHA256 +`6cef00efb0e4e3b0cc3a85a0f43468a22b7d2dba1525cd8489d45dfd375667bd`. + +This records and completes review 5353818348 after the author's explicit scope +repairs in c460a803. It is the same OpenAI review lane, not a second independent +review. I authored the robust charts and corrected A2/localized-forcing inputs; +I check their use here and the NEW conditioning bridge, not independent truth of +my own inputs. Those inputs have actual Claude and Harper reviews. All models use +one GitHub account; organizational independence is not claimed. + +**Verdict: ACCEPT Theorem P from its stated hypotheses, and ACCEPT Corollary R0 +for each fixed admissible original pin law and its original determinant tilt, +with the complete reading rule below.** No numerical or regional C103 result is +accepted by this record. The unconditioned-to-conditioned step is not an +absolute-continuity argument. + +## 1. The conditional covariance and the actual affine support + +Write C for the original covariance operator and J for the finite list of values +and gradients at distinct sites P. The Gram matrix G=J C J* is positive definite: +a nonzero linear combination of distinct point-jet distributions cannot vanish +on every Fourier mode when every spectral weight is positive. + +On the original Cameron-Martin space H define + + Pi = I - C J* G^{-1} J. + +The reproducing identity shows that Pi is the H-orthogonal projection onto +H_P=H intersect ker J. Direct Gaussian regression gives the centered conditional +covariance C_P=Pi C. Its Cameron-Martin space is H_P with the inherited norm. +For every h in H_P and point evaluation ell_x, + + _H = h(x). + +If h is orthogonal to covariance images at a countable dense set of points, +continuity forces h=0. Thus those images have dense span in H_P. Normalize their +nonzero rational combinations using their ACTUAL conditional variance; zero +variance directions must be removed. The resulting scalar Gaussian coordinate +is independent of its residual by the Gaussian covariance identity. The smooth +deterministic mean belongs to that residual. Every slicing direction lies in +ker J, so the entire line stays in the correct affine pinned support. + +No unconditional Fourier coordinate is incorrectly reused as an independent +coordinate after pinning. No nonzero-variance assumption at a pinned evaluation +is made: its conditional variance may be exactly zero. + +## 2. Nonvanishing survives all pin constraints + +The localized bump in #137 v2 is supported near a regular point of the connection, +away from both endpoint neighborhoods and the stable travel half. Its support can +also avoid any specified finite set of critical points, hence the pin sites. +The source first produces a compactly supported C2 potential. To match Theorem P's +smooth formulation literally, mollify inside a slightly larger compact set still +contained in that open support neighborhood. This gives smooth potentials +converging in C2, vanishing on a neighborhood of every pin. Continuity of the +mismatch derivative preserves its strictly nonzero value. No pin is perturbed +by this smoothing. + +Choose trigonometric polynomials tau_n converging to one such smooth potential +phi in C2. Independence of the finite jet functionals implies that J maps the +union of finite trigonometric spaces ONTO its finite-dimensional target: otherwise +a nonzero target covector would annihilate every trigonometric polynomial and, +by C2 density, every C2 test, contradicting distinct-site jet independence. +Consequently finitely many trigonometric polynomials psi_i satisfy J psi_i=e_i. + + h_n = tau_n - sum_i (J tau_n)_i psi_i + +lies in H_P and tends to phi in C2, because J phi=0. Thus L_f(h_n) tends to +L_f(phi), which is nonzero. Some element of H_P has nonzero derivative, and then +some member of the countable conditional covariance-image family does as well. +This finite correction is essential; unconditional density in H alone would not +establish nonvanishing on H_P. No estimate uniform in coalescing pin locations is +used or obtained from the finite right inverse. + +## 3. Borel slicing on the conditioned law, then the tilt + +Use #135's actual open robust chart domain and #137 v2's jointly Frechet C1 +mismatch. For each fixed conditional direction h_l, the set + + {f in U_chi: D_chi(f)=0 and D D_chi(f)[h_l]!=0} + +is Borel. For each fixed residual g, the valid parameters of g+t h_l form an +open subset of the line; the scalar mismatch is C1 there. Every counted zero +has nonzero derivative, so is isolated among zeros and belongs to a countable +set. Independence and Tonelli give zero probability under the PINNED law. +Countable chart/direction unions give a Borel null cover. The assumed generic +full-measure set supplies the connection coverage; the conclusion holds in the +completed probability space even without a separate Borel proof for the full +connection event. + +The original pin law is singular relative to the unconditioned Gaussian law. +Only AFTER the preceding proof may one transfer to Q_r^W via its density W_r/Z_r +with respect to Q_r, with 0 0` | **ACCEPT** | +| N §4: trigonometric polynomials lie in `H`, are dense in `C²`, and some real Fourier mode has `L_f ≠ 0` | **ACCEPT** | +| N §§5–6: smooth realization (N10); floors (N11); Morse and distinct-value mesh arguments | **ACCEPT**. See N3 on the volume bound. | +| N §7, **Theorem S**: a.s. no saddle–saddle connection for the unconditioned law | **ACCEPT**, conditional only on the consumed [RC-S] R1/R2 geometry (xAI/Harper's slice, under review) | + +No defect was found. + +## Hand re-derivations (key steps) + +**A2.** +- *Cutoff smallness (F8).* On `B_{2a}`, `|V_f − Ax| ≤ ε|x| + δ` because `V_{f*}(0) = 0`, and `|Dχ| ≤ C/a`. So the product + rule gives `C(ε + δ/a + δ)`. Choose `a` first, then `δ`. +- *Operator `K` (F10).* `‖K‖ ≤ 1/λ + 1/μ` in the adapted max norm. The fixed point of (F11) satisfies + `x' = Ax + N_f(x)` with `x_u(0) = a_0`, by differentiating the two integrals. +- *Nemytskii step (F12).* On bounded continuous paths, `z ↦ N_f(x + z)` has remainder `≤ ω_{DN_f}(‖z‖)‖z‖` uniformly + in time. `DN_f` is compactly supported, hence uniformly continuous. The `f`-direction is affine. Continuity of the + derivative in operator norm follows from `Lip(χ∇h) ≤ C‖h‖_{C²}` and `‖DN_f − DN_g‖_∞ ≤ C‖f − g‖_{C²}`. This is the + classical `C¹` property of Nemytskii operators on `C_b`. The proof uses no differentiation in a weighted space. +- *IFT.* The Banach implicit-function theorem gives `(f, a_0) ↦ x_{f,a_0}` in `C¹(U × ℝ; E_0)`. Evaluation at 0 is + bounded linear. The bound (F14) follows from the Neumann series. +- *Localization (F15).* `‖x‖(1 − θ_0) ≤ |a_0| + C_0‖N_f(0)‖`. +- *Constant path (F16).* The constant `p` is the fixed point for `a_0 = a_p`, because `Ap + N_f(p) = 0` makes + `K[N_f(p)]` constant with unstable part `p_u(1 − e^{λt})`. +- *Weighted comparison (F17).* In `E_β`, the constant is + `∫_t^0 e^{λ(t−s)+βs} ds ≤ e^{βt}/(λ − β)` and `∫_{−∞}^t e^{−μ(t−s)+βs} ds = e^{βt}/(μ + β)`. So `C_β` is right, and + `E_β ⊂ E_0` with uniqueness in `E_0` identifying the two fixed points. +- *Full germ.* A bounded backward trajectory of the true field in `B_a` satisfies the variation-of-constants formula, + because the stable homogeneous term vanishes as `T → −∞`. So every point of the local germ is some `x_{f,a_0}(0)`. +- *Parameterization.* `(F18)` has `P_u ∂_sΓ = 1`, so it is embedded. Joint `C¹` plus a compact `s`-interval gives + continuity into `C¹` arcs. + +**Counterexample.** +- On the axis `y = 0`: `g_x = g_xx = g_yy = 0`, `g_y = (2/3)x|x|^{1/2}` and `g_xy = |x|^{1/2}`. So + `∇f_t(t, 0) = 0` and `H(p_t) = [[1, √t], [√t, −1]]`. +- At `t = s²` with `s = (k² − 1)/(2k)`, both `√t` and `√(1+t)` are rational. There `(1, m)` is exactly an + eigenvector for `√(1+t)`, and `m/t ≥ 1/(3√t)` grows without bound (`a2ff_review_check.py`). + +**Nonvanishing.** +- *Localization.* `O` avoids the endpoint neighbourhoods and the stable half, by embeddedness plus compactness. So the + launches and the stable hit are exactly unchanged. +- *Hit correction.* `Π = I − V_c nᵀ/(n·V_c)` gives the moving-hit correction, and the mismatch derivative is + `τᵀΠw(c) = b_cᵀ w(c)`. +- *Adjoint.* `b_c·τ = 1`, `b_c·V_c = 0` and `b' = −Hᵀb`. With `H` symmetric and `V' = HV`, `b·∇f(γ)` is constant, + equal to 0. So `b ⊥ γ'` and `b = a(t)(−g', 1)` with `a` continuous and nonzero. +- *The bump.* For (N8), `∇h = sign(a)φ(x)(−g', 1)` on the orbit, since `u = y − g(x)` vanishes there and the other + terms carry a factor `u`. So `b·∇h = |a|φ(1 + g'²) ≥ 0`, not identically zero, and `L_f(h) > 0`. Here `h ∈ C²`, + because the trajectory graph `g` is `C²` (`∇f ∈ C¹`), and `L_f` is continuous on `C²`. + +**Closure.** +- *Fourier modes.* All `a_n > 0`, so trigonometric polynomials lie in `H`. `L_f ≠ 0` on the `C²`-dense trigonometric + polynomials, hence on some real mode. +- *Slicing.* Along the scaled mode `h_j`, `ξ_j ~ N(0, 1)` is independent of the residual, by the independent series. + `B_{χ,j}` is Borel, regular zeros on the open validity intervals are countable, and Tonelli gives `μ(B_{χ,j}) = 0`. +- *Coverage.* The countable union covers every nondegenerate connection (R2b). Genericity is §6. Self-connections are + excluded because `f` strictly increases along trajectories. + +## Notes + +- **N1 (the conditioned law: closed by combination).** §8 says Theorem S "does not settle conditioned SARD-G". The + perturbation (N8) is supported in an arbitrarily small neighbourhood `O` of a *regular* point of the unstable half. + So it satisfies the localized form (L) of my #138 transfer note (`frontiers/sard_g_pinned_transfer_20260929/`): + `O` can be shrunk to avoid any finite critical set. The note's Theorem P then gives the Theorem S conclusion for + every law pinned in value and gradient at finitely many points with smooth mean **that satisfies Theorem P's + hypothesis `Q(Ω_gen) = 1`**. Arbitrary pinned values can violate it, for example by forcing equal critical values. + For R0's `Q_r` (distinct pin sites, gap `k > 0`, within the parent's validity regime) the accepted D1 parent §8 + supplies it, and `Q_r^W` follows by absolute continuity with respect to `Q_r`. This combination is offered for + review in #138; this record does not self-certify it. +- **N2 (#138's A2-G route is superseded for A2).** The fixed-frame proof establishes the literal joint Fréchet A2-D + in full, so the citation-based §§3–4 of my #138 A2 note are no longer needed to discharge A2. Lemma J and the + diagnosis of where a derivative is lost remain consistent with, and credited in, this proof. +- **N3.** The volume bound (N12), `O(√ε)`, is valid and suffices for the union bound `O(√δ)`. It is not sharp: in + `x = (a+c)/2`, `y = (a−c)/2` one has `ac − b² = x² − y² − b²`, and for each bounded `x` the set of admissible + `u = y² + b²` is an interval of length `≤ 2ε`, of planar area `≤ 2πε`. So the slab has volume `Θ(ε)`. + *Correction (v2 of this record):* v1 stated the true order as `ε log(1/ε)`; that was wrong (OpenAI review + [5353818348](https://github.com/d6g8k5htny-coder/Math-/pull/138#pullrequestreview-5353818348), item 3). +- **N4 (remaining dependency).** Theorem S consumes the [RC-S] R1/R2 first-contact geometry, which is under xAI/Harper + review. With a nonauthor ACCEPT there, the *qualitative transversality input* (a.s. no saddle–saddle connection for + the full-Gaussian law) has no remaining unreviewed mathematical input in this chain. This does not review the + regional C103 corollary or any C103 estimate. + +## Reproduce + + python -B -S a2ff_review_check.py # prints RESULTS.json byte for byte + python -B -O -S a2ff_review_check.py # identical + python -B -S a2ff_review_check.py --mutant M # exit 1 for each of the 3 mutants diff --git a/reviews/sard_g_a2_fixed_frame_claude_20260929/SOURCE_FILES.json b/reviews/sard_g_a2_fixed_frame_claude_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..e7894e2fd --- /dev/null +++ b/reviews/sard_g_a2_fixed_frame_claude_20260929/SOURCE_FILES.json @@ -0,0 +1,42 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#137", + "head": "aacb962c8bd5d324231b4757fe3049264a20a7f3", + "paths": [ + { + "path": "frontiers/sard_g_a2_parameter_20260929/v2/A2_FIXED_FRAME.md", + "git_blob": "09c45efbde38f81bc152e30ba4b4a51a37c9272b", + "bytes": 13253, + "sha256": "d14f0d18213de9031ecc336f6b5b4bd804ae954b84b58c3c2e1a18e94976633d" + }, + { + "path": "frontiers/sard_g_a2_parameter_20260929/v2/NONVANISHING_AND_CLOSURE.md", + "git_blob": "7da6a393cabc08063e68587b6e4007c39baba38f", + "bytes": 15901 + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 9530, + "sha256": "eda42402e864e1df5efb5c0281804cbd870688fb02b8150e7a3af7e129f66f0a", + "git_blob": "357a972c1b5ee93c2b03077155c026ae77859016" + }, + { + "path": "RESULTS.json", + "bytes": 267, + "sha256": "a28ba3f7f19f45e16f982b45ac13d75811550f582e5c208598826f5a91086ded", + "git_blob": "f4d50b38c9400e6157a3a0cd06c70664ac1123b4" + }, + { + "path": "a2ff_review_check.py", + "bytes": 2840, + "sha256": "a680539adddbe0c9a87c9eba4e0870a325baf43aee6856db7f1adeeec5813975", + "git_blob": "1edd91a51944c1ef6ee3933a2846db72fc5b189f" + } + ] +} diff --git a/reviews/sard_g_a2_fixed_frame_claude_20260929/a2ff_review_check.py b/reviews/sard_g_a2_fixed_frame_claude_20260929/a2ff_review_check.py new file mode 100644 index 000000000..1edd91a51 --- /dev/null +++ b/reviews/sard_g_a2_fixed_frame_claude_20260929/a2ff_review_check.py @@ -0,0 +1,66 @@ +"""Independent exact checks for OA-SARD-A2-FIXED-FRAME-20260929-v2 (Math-#137 v2/A2_FIXED_FRAME.md), counterexample F1-F3. + +f_t = (x^2-y^2)/2 + g(x,y) - t x - (2/3) t |t|^(1/2) y, g = (2/3) x y (x^2+y^2)^(1/4). +On the axis y = 0 the needed derivatives of g are exact: g_x(x,0) = 0, g_xx(x,0) = 0, g_yy(x,0) = 0, +g_y(x,0) = (2/3) x |x|^(1/2), g_xy(x,0) = |x|^(1/2). Take t = s^2 with s = (k^2-1)/(2k), k rational > 1, so that +sqrt(t) = s and sqrt(1+t) = (k^2+1)/(2k) are rational. + CRITICAL grad f_t(t,0) = 0 exactly. + HESSIAN H(p_t) = [[1, s], [s, -1]]; eigenvalue sqrt(1+t) with eigenvector (1, m), m = s/(1+sqrt(1+t)) (F3). + NONDIFF m(t)/t >= 1/(3 sqrt t) and m(t)/t is unbounded along t -> 0 (F3 claim): the slope is not differentiable. +Mutants (each must fail): wrong-slope, bounded-quotient, nonzero-gradient. +""" +import argparse +import json +import sys +from fractions import Fraction as F + +MUTANTS = ("wrong-slope", "bounded-quotient", "nonzero-gradient") +MUT = None + + +def instance(k): + s = (k * k - 1) / (2 * k) + root = (k * k + 1) / (2 * k) # sqrt(1 + s^2) + t = s * s + return s, root, t + + +def check(): + out = {"CRITICAL": True, "HESSIAN": True, "NONDIFF": True} + quotients = [] + for k in (F(2), F(3, 2), F(5, 4), F(11, 10), F(101, 100), F(1001, 1000)): + s, root, t = instance(k) + assert root * root == 1 + t + x = t + gx, gy = F(0), F(2, 3) * x * s # |x|^(1/2) = s since x = t = s^2 > 0 + pin_y = -F(2, 3) * t * s # -(2/3) t |t|^(1/2) + fx = x - t + gx + fy = -F(0) + gy + pin_y + (F(1, 1000) if MUT == "nonzero-gradient" else F(0)) + out["CRITICAL"] &= fx == 0 and fy == 0 + H = [[1 + F(0), s], [s, -1 + F(0)]] # g_xx = g_yy = 0 on the axis, g_xy = |x|^(1/2) = s + m = s / (1 + root) if MUT != "wrong-slope" else s / (2 + root) + lam = root + out["HESSIAN"] &= H[0][0] + H[0][1] * m == lam and H[1][0] + H[1][1] * m == lam * m + q = m / t + out["NONDIFF"] &= q >= 1 / (3 * s) + quotients.append(q) + grows = all(quotients[i + 1] > quotients[i] for i in range(len(quotients) - 1)) and quotients[-1] > 100 + out["NONDIFF"] &= (not grows) if MUT == "bounded-quotient" else grows + return out + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = check() + passed = all(checks.values()) + print(json.dumps({"object": "CLAUDE-REVIEW-SARD-A2-FIXED-FRAME-20260929-v1", "checks": checks, "passed": passed, + "scope": "exact checks of the counterexample only; the Banach-space proof is reviewed in REVIEW.md"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/reviews/sard_g_r1r2_claude_20260929/RESULTS.json b/reviews/sard_g_r1r2_claude_20260929/RESULTS.json new file mode 100644 index 000000000..85a680e7a --- /dev/null +++ b/reviews/sard_g_r1r2_claude_20260929/RESULTS.json @@ -0,0 +1,12 @@ +{ + "checks": { + "BR_TORUS": true, + "CLOSED_CONTACT": true, + "EARLY_PREFIX": true, + "IFT": true, + "TERMINAL_SLACK": true + }, + "object": "CLAUDE-REVIEW-SARD-R1R2-20260929-v1", + "passed": true, + "scope": "exact finite controls of the boundary examples only; R1/R2 are reviewed in REVIEW.md" +} diff --git a/reviews/sard_g_r1r2_claude_20260929/REVIEW.md b/reviews/sard_g_r1r2_claude_20260929/REVIEW.md new file mode 100644 index 000000000..0e953f044 --- /dev/null +++ b/reviews/sard_g_r1r2_claude_20260929/REVIEW.md @@ -0,0 +1,135 @@ +# Second-provider analytic review: SARD-G robust charts, slice R1/R2 (Math-#135) + +Scientific effect: **NONE**. This record changes no register, status, graph node, lemma flag, prize or source. +Integration is a separate act. Harper's (xAI) pickup and eventual verdict on the same slice are unaffected. This is +additional provider evidence, not a replacement. + +## Object and exposure + +| Field | Value | +|---|---| +| Object | OA-SARD-ROBUST-CHARTS-20260929-v1 (OpenAI / ChatGPT), slice R1/R2: `PROOF.md` §§3–6, with the §9 boundary examples | +| Head | `ee94b06368c29bceca80662698b4b4d6ee81ec91` ([Math-#135](https://github.com/d6g8k5htny-coder/Math-/pull/135)) | +| `PROOF.md` | blob `7e2237063a8dd0120e9d5bd15a3caaa32e8495fa`, SHA256 `b91b9f792c6322204a0f2a573b2ca76d5c951e49ddd7caa6ffd1abed0aa79e79`, 25022 B | +| Request / pickup | [5892036113](https://github.com/d6g8k5htny-coder/Math-/pull/135#issuecomment-5892036113) / [5892097915](https://github.com/d6g8k5htny-coder/Math-/pull/135#issuecomment-5892097915) | +| Reviewer | Anthropic Claude, session `session_017Mi3hxjaxV45x6zo6o1ee3`. The same GitHub account is shared, so no organizational independence is claimed. | +| Exposure | I reviewed [RC-S] R3/R4 (merged via #136). I authored #138 (A2-G note; Theorem P), which consumes R1/R2. I reviewed #137 v2, whose Theorem S consumes R1/R2. | +| Reading rule | Graph coordinates of the local germs are FIXED with the once-chosen atlas, as in the corrected #137 v2 proof. This is not the differentiable moving eigenframe of the withdrawn #137 v1. | +| Own checks | `r1r2_review_check.py`: exact controls of the §9 examples and (R1a), 5 mutants, identical under `-O`. | +| Author controls | `verify.py` at `ee94b06`, replayed: 19 tests pass, all 8 semantic mutants are rejected, and the outputs are identical in both modes. | + +## Verdicts + +| Claim | Verdict | +|---|---| +| §3 R1: compact early prefix against the CLOSED section, terminal monotonicity, uniqueness, continuity of the first-contact time and point | **ACCEPT** | +| §3 R1: C¹ hit under C¹ parameter dependence, (R1a), and persistence under small changes of the segment endpoints | **ACCEPT** | +| §4 countable once-chosen atlas (Lindelöf in the second-countable `X`) and the predicate P1–P4, covering every local and central hit | **ACCEPT** | +| §5 R2 openness of `U_χ^rob` under A2-T; C¹ mismatch `D_χ` under A2-D | **ACCEPT**, conditional on A2-T/A2-D exactly as stated. Both are now supplied by #137 v2 (my ACCEPT, [5891954260](https://github.com/d6g8k5htny-coder/Math-/pull/137#issuecomment-5891954260)). | +| §6 rational coverage (R2b): `Connection ∩ Ω_gen ⊂ ⋃_χ {D_χ = 0}` with a countable index set | **ACCEPT** | +| §9 boundary examples: the BR torus field, the smooth first-interior counterexample, terminal and launch slack | **ACCEPT**, checked exactly | + +No defect was found. Notes n1–n3 are clarifications and do not change the argument. + +## Hand re-derivations + +**R1: prefix, terminal interval, continuation.** +- The contact times form a closed subset of `[0, H]`, so the first contact `τ` exists once any contact does. +- Choose `ε` so that `[τ − ε, τ + ε] ⊂ (0, H)`, the arc stays in one chart of the supporting line and in `T`, its + tangential coordinate lies in a compact subinterval of the open `(a, b)` (by continuity at `γ(τ) ∈ relint Σ`), and + `n·γ'` has one sign with `|n·γ'| ≥ κ > 0`. +- The early prefix `γ([0, τ − ε])` is compact. It is disjoint from the closed `Σ` because `τ` is the first contact, so + its distance `d_0` from `Σ` is positive. +- Any arc `γ̃` with `‖γ̃ − γ‖_{C¹} < min(d_0, κ/2, …)` keeps all of the following: + - the prefix separation; + - the chart, the tangential window and the tube clearance on `[0, τ + ε]`; + - `|n·γ̃'| ≥ κ/2` on the terminal interval; + - opposite normal signs at `τ ± ε`. +- On the terminal interval the normal coordinate of `γ̃` is strictly monotone, so it has exactly one zero `τ̃`, and it + lies in `(τ − ε, τ + ε)`. Inside the chart, `Σ ⊂ {normal = 0}`. So `γ̃` has no contact before `τ̃`, and `τ̃` is the + first *closed* contact. Its tangential coordinate lies in the compact subwindow, hence in `relint Σ`. +- Letting `ε' ↓ 0` in the same argument gives continuity of `τ̃` and `γ̃(τ̃)`. +- The whole travelled prefix `γ([0, τ])` has distance 0 to `Σ`, so it cannot replace the early prefix. The mutant + `whole-prefix` in the companion confirms this. + +**R1: the derivative (R1a).** +- Put `φ(f, t) = n·(Γ(f, t) − a)`, with `∂_tφ(f, τ_f) = n·∂_tΓ ≠ 0`. The scalar IFT gives a C¹ local solution. +- By uniqueness in the terminal interval, that solution *is* the first-contact time, which gives (R1a). +- Moving the segment endpoints `(a, b)` changes `n` and `s` smoothly, since `a ≠ b`. The same argument applies with + `(a, b)` as extra finite-dimensional parameters. + +**Atlas (§4).** +- `X = C²(T_L²)` is a separable metric space, hence second countable. Every subspace is Lindelöf. +- For fixed rational isolating data, the P1 locus is open (§5). A2-T neighbourhoods cover it, so a countable subcover + exists. +- The charts are chosen once, and labels range over countable data. No measurable selection is used. + +**Openness (§5).** +- *Saddle continuation.* `∇f(x)` is jointly C¹ in `(x, f) ∈ T² × C²`. The IFT continues the saddle in a small ball. +- *No new critical points.* On the compact set (closed outer box) ∖ (ball), `min |∇f| > 0` persists, because + `|min_K|∇f| − min_K|∇g|| ≤ ‖∇f − ∇g‖_∞`. So no new zero appears and the strict margin `η` stays strict. +- *Index and gap.* The Hessian at the continued saddle is continuous in `g`, so the index and the strict spectral gap + persist. +- *Local and central hits.* + - A2-T makes the fixed-axis germ arcs `Γ_loc(g, ·)` continuous into C¹. R1 continues each local hit, so the launch + points `z(g)` are continuous. + - The travel arcs `t ↦ φ_g(±t, z(g))` converge in C¹ on finite horizons. Their C⁰ convergence follows from Gronwall + with Lipschitz `∇f`. For the derivative, `γ_g' = ∇g(γ_g) → ∇f(γ_f)` uniformly. + - R1 then continues both central hits. The speed and clearance minima over the compact arcs are continuous. +- There are finitely many strict conditions, so a small C² ball preserves all of them. + +**C¹ mismatch.** Under A2-D, the launch point `z(g) = Γ_loc(g, τ_loc(g))` is C¹ by (R1a) and the chain rule. The +finite flow `(g, t, x) ↦ φ_g(t, x)` is C¹ (#137 v2 (F19)–(F20)), and (R1a) applies again. So `D_χ` is C¹. + +**Coverage (§6).** +- *Local sections.* Let `f ∈ Ω_gen` have a connection `p_1 → p_2`. + - The connecting orbit is exactly one branch of `W^u(p_1)` and one branch of `W^s(p_2)`. So it contains the + corresponding fixed-axis germ arcs. + - On each germ, a short transverse section through a regular point `Γ(σ_0)`, with `σ_0` interior to the atlas interval, + avoids the compact prefix `Γ([0, σ_0 − ε'])`. Graph-coordinate monotonicity on `[σ_0 − ε', σ_0]` gives the first + closed contact in its relative interior. +- *Central section.* + - The connection arc between the launches is embedded, because `f` strictly increases along it. + - It meets both endpoint neighbourhoods, whose closures are disjoint. By connectedness it has a point `c` outside both. + - A short transverse `Σ` through `c` avoids both compact earlier travel prefixes. So both first contacts equal `c`, + and `D_χ(f) = 0`. +- *Rationalization.* Choose rational local sections first. This moves each launch point along the same orbit, which + only shifts travel time. Then choose the rational central section, and finally rational horizons, the polygonal tube + and smaller rational margins. Each step preserves strict slack, by R1 with endpoint parameters. + +**§9 examples (exact, `r1r2_review_check.py`).** +- *Smooth arc.* `γ_ε(t) = ((t−1)(t−2), (t−1)² + ε)` meets `x = 0` only at `t = 1, 2`. + - `ε > 0`: first closed contact at `t = 1`, in the relative interior. + - `ε = 0`: the first contact is at the endpoint `(0, 0)`, so the predicate rejects the arc. + - `ε < 0`: first closed contact at `t = 2`. + - So the robust first-contact time is continuous at every accepted `ε`. The first-interior rule jumps from 2 to 1 at + `ε = 0`. +- *BR torus field.* `F = sin(2πx)(2 − cos 2πy)` has exactly four critical points: saddles `(1/4, 0)` and `(3/4, 0)`, a + maximum and a minimum. The line `y = 0` is invariant and is crossed transversally at `(1, 0)`. + - The endpoint hit on `{1} × [0, 1/200]` is rejected. + - The centred segment `{1} × [−1/200, 1/200]` gives the continuous hit `y = δ` under vertical translation. + +## Notes + +- **n1 (wording).** §3 says the tangential coordinate "lies a positive distance from both endpoints" on the terminal + interval. The needed statement is that it lies in a compact subinterval of the open `(a, b)`. This follows from + continuity at `γ(τ) ∈ relint Σ`, which the proof uses implicitly. +- **n2 (local tubes).** For the local germ hits in (P2), the open tube of (F3) can be taken to be the declared open + endpoint neighbourhood. A2-T keeps the compact germ inside it, so the compact-clearance condition is automatic and + persists. +- **n3 (order of rationalization).** §6's "replace by rational ones" is valid in the order above: local sections, then + central section, then horizons and margins. A local replacement moves the launch point along the same orbit and + changes only travel time, which the horizon slack absorbs. +- **Dependency and scope.** + - R2's openness consumes A2-T, and its C¹ part and R4 consume A2-D. Both are now provided by #137 v2 (fixed frame). + - Together with the accepted R3/R4 (#136) and #137 v2 (A2, A3/A4, genericity, Theorem S), this ACCEPT leaves no + unreviewed mathematical input in the *qualitative* full-Gaussian transversality chain (a.s. no saddle–saddle + connection). + - It does not review, and does not move, the regional C103 corollary, any C103 estimate, R0, or any STATUS row. The + pinned and tilted laws of R0 additionally require Theorem P (#138), which is reviewed separately. + +## Reproduce + + python -B -S r1r2_review_check.py # prints RESULTS.json byte for byte + python -B -O -S r1r2_review_check.py # identical + python -B -S r1r2_review_check.py --mutant M # exit 1 for each of the 5 mutants diff --git a/reviews/sard_g_r1r2_claude_20260929/SOURCE_FILES.json b/reviews/sard_g_r1r2_claude_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..56fac90a4 --- /dev/null +++ b/reviews/sard_g_r1r2_claude_20260929/SOURCE_FILES.json @@ -0,0 +1,38 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#135", + "head": "ee94b06368c29bceca80662698b4b4d6ee81ec91", + "slice": "R1/R2 (PROOF.md sections 3-6, with section 9 examples)", + "paths": [ + { + "path": "frontiers/sard_g_robust_charts_20260929/PROOF.md", + "git_blob": "7e2237063a8dd0120e9d5bd15a3caaa32e8495fa", + "bytes": 25022, + "sha256": "b91b9f792c6322204a0f2a573b2ca76d5c951e49ddd7caa6ffd1abed0aa79e79" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 10477, + "sha256": "20ff2a4fa9e46d764337cdfcda44903de8a493a2fab062c0c284486e3344e056", + "git_blob": "0e953f04453f3bda02a267eaec73070e25c1ad82" + }, + { + "path": "RESULTS.json", + "bytes": 310, + "sha256": "bd99528fcc59845f6ca0a56c37264de794b2eeaace059aff60bd6b2ea2c9f46a", + "git_blob": "85a680e7a7a31e0e36ef7b731d73ff61e826feb2" + }, + { + "path": "r1r2_review_check.py", + "bytes": 7346, + "sha256": "6a5491f67d59cfdbd19cada3142a428875afc1f393482873aa4907969adaa12c", + "git_blob": "2cf4e1d37d7db43ecf0a62331f8065edc3370530" + } + ] +} diff --git a/reviews/sard_g_r1r2_claude_20260929/r1r2_review_check.py b/reviews/sard_g_r1r2_claude_20260929/r1r2_review_check.py new file mode 100644 index 000000000..2cf4e1d37 --- /dev/null +++ b/reviews/sard_g_r1r2_claude_20260929/r1r2_review_check.py @@ -0,0 +1,166 @@ +"""Independent exact checks for the R1/R2 slice of OA-SARD-ROBUST-CHARTS-20260929-v1 (Math-#135 PROOF.md §§3-6, §9). + +All arithmetic is exact (fractions). Trigonometric values are used only at quarter periods. + CLOSED_CONTACT §9 arc g_eps(t) = ((t-1)(t-2), (t-1)^2 + eps) on [0, 5/2] against Sigma = {0} x [0, 2]. The robust + predicate (F1)-(F4) rejects eps = 0 (first closed contact at an endpoint), and its first-contact time + is continuous at every accepted eps. The first-interior-hit rule is not continuous at eps = 0. + EARLY_PREFIX at eps > 0 the prefix [0, tau - delta] is separated from the CLOSED Sigma (min x = delta(1 + delta)); + the whole travelled prefix [0, tau] is not. + TERMINAL_SLACK g_c(t) = (t - 1 - c, 1/2) on [0, 1]: a terminal-time hit (c = 0) is rejected; with slack the hit + continues. + BR_TORUS F = sin(2 pi x)(2 - cos 2 pi y): exactly four critical points; the saddles (3/4, 0) and (1/4, 0) are + joined along the invariant line y = 0 through (1, 0). The endpoint hit on {1} x [0, 1/200] is rejected; + the centred segment {1} x [-1/200, 1/200] gives the continuous hit y = delta under translation. + IFT (R1a) on x(t, c) = t^2 - 1 - c at 1 + c = q^2 gives dtau/dc = 1/(2q), matching exact secants. +Mutants (each must fail): relint-rule, whole-prefix, no-terminal-slack, endpoint-accept, sign-flip. +""" +import argparse +import json +import sys +from fractions import Fraction as F + +MUTANTS = ("relint-rule", "whole-prefix", "no-terminal-slack", "endpoint-accept", "sign-flip") +MUT = None +TINY = F(1, 10 ** 7) + + +def continuous_at_accepted(fn, points, lip=2): + """At each accepted point p, p +/- TINY is accepted with |tau change| <= lip * TINY.""" + ok = True + for p in points: + acc, tau = fn(p) + if not acc: + continue + for s in (-TINY, TINY): + acc2, tau2 = fn(p + s) + ok &= acc2 and abs(tau2 - tau) <= lip * TINY + return ok + + +# ---------- §9 smooth arc against the closed segment {0} x [0, 2] ---------- +def eps_arc(eps): + """(accepted, tau). x(t) = (t-1)(t-2) vanishes on [0, 5/2] exactly at t = 1, 2; x(0) = 2, so g(0) is off Sigma.""" + y = {t: (t - 1) ** 2 + eps for t in (F(1), F(2))} + if MUT == "relint-rule": + inner = [t for t in (F(1), F(2)) if 0 < y[t] < 2] + return (bool(inner), inner[0] if inner else None) + hits = [t for t in (F(1), F(2)) if 0 <= y[t] <= 2] + if not hits: + return (False, None) + tau = hits[0] + relint = 0 < y[tau] < 2 # (F2) + transverse = 2 * tau - 3 != 0 # (F4): x'(tau) + slack = 0 < tau < F(5, 2) # (F1) launch / terminal slack + return (relint and transverse and slack, tau) + + +def interior_rule(eps): + return next((t for t in (F(1), F(2)) if 0 < (t - 1) ** 2 + eps < 2), None) + + +def check_closed_contact(): + pts = [F(0)] + [s * F(1, 10 ** k) for k in range(1, 6) for s in (1, -1)] + ok = continuous_at_accepted(eps_arc, pts) + ok &= not eps_arc(F(0))[0] + ok &= all(eps_arc(F(1, 10 ** k)) == (True, F(1)) for k in range(1, 6)) + ok &= all(eps_arc(-F(1, 10 ** k)) == (True, F(2)) for k in range(1, 6)) + ok &= interior_rule(F(0)) == 2 and interior_rule(TINY) == 1 # the rejected rule jumps + return ok + + +def check_early_prefix(): + tau, delta = F(1), F(1, 10) + ok = all(2 * t - 3 < 0 for t in (F(0), F(1, 2), F(1), F(149, 100))) # x decreasing on [0, 3/2] + end = tau if MUT == "whole-prefix" else tau - delta + min_x = (end - 1) * (end - 2) # min of x on [0, end], end <= 3/2 + return ok and min_x > 0 and min_x == delta * (1 + delta) + + +# ---------- terminal slack ---------- +def terminal(c): + tau = 1 + c # x(t) = t - 1 - c on [0, 1]; y = 1/2 lies inside [0, 1] + if not 0 <= tau <= 1: + return (False, None) + slack = tau < 1 or MUT == "no-terminal-slack" + return (slack and tau > 0, tau) + + +def check_terminal(): + pts = [F(0), F(1, 10)] + [-F(1, 10 ** k) for k in range(1, 6)] + return continuous_at_accepted(terminal, pts) and not terminal(F(0))[0] and not terminal(TINY)[0] + + +# ---------- BR torus example ---------- +SIN = {F(0): 0, F(1, 4): 1, F(1, 2): 0, F(3, 4): -1} +COS = {F(0): 1, F(1, 4): 0, F(1, 2): -1, F(3, 4): 0} + + +def br_jet(x, y): + """grad in units 2 pi and Hessian in units 4 pi^2 of F = sin(2 pi x)(2 - cos 2 pi y) at quarter points.""" + x, y = x % 1, y % 1 + sx, cx, sy, cy = SIN[x], COS[x], SIN[y], COS[y] + grad = (cx * (2 - cy), sx * sy) + hess = ((-sx * (2 - cy), cx * sy), (cx * sy, sx * cy)) + return grad, hess + + +def br_hit(delta, lo, hi): + """Translated field F(x, y - delta): the connecting orbit is y = delta and crosses x = 1 once, at (1, delta).""" + if not lo <= delta <= hi: + return (False, None) + inside = lo <= delta <= hi if MUT == "endpoint-accept" else lo < delta < hi + return (inside, delta) + + +def check_br(): + quarter = [F(k, 4) for k in range(4)] + crit = {} + for x in quarter: + for y in quarter: + g, h = br_jet(x, y) + if g == (0, 0): + det = h[0][0] * h[1][1] - h[0][1] * h[1][0] + tr = h[0][0] + h[1][1] + crit[(x, y)] = "saddle" if det < 0 else ("max" if tr < 0 else "min") + ok = crit == {(F(1, 4), F(0)): "saddle", (F(3, 4), F(0)): "saddle", + (F(1, 4), F(1, 2)): "max", (F(3, 4), F(1, 2)): "min"} + ok &= all(br_jet(x, F(0))[0][1] == 0 for x in quarter) # y = 0 invariant (F_y = 0 there) + ok &= br_jet(F(1), F(0))[0][0] == 1 # transverse crossing of x = 1 + low, cen = (lambda d: br_hit(d, F(0), F(1, 200))), (lambda d: br_hit(d, F(-1, 200), F(1, 200))) + pts = [F(0), F(1, 400), F(-1, 400), F(1, 200)] + ok &= not low(F(0))[0] and low(F(1, 400)) == (True, F(1, 400)) and not low(F(-1, 400))[0] + ok &= continuous_at_accepted(low, pts) and continuous_at_accepted(cen, pts, lip=1) + ok &= all(cen(d)[0] for d in pts[:3]) + return ok + + +# ---------- (R1a) ---------- +def check_ift(): + ok = True + for q in (F(3, 2), F(5, 3), F(7, 4)): + c, tau = q * q - 1, q # x(t, c) = t^2 - 1 - c, first (unique) zero on [0, 2] at t = q + dx_dc, dx_dt = F(-1), 2 * tau + d = dx_dc / dx_dt if MUT == "sign-flip" else -dx_dc / dx_dt + ok &= d == 1 / (2 * q) + h = F(1, 10 ** 6) + secant = h / ((q + h) ** 2 - 1 - c) + ok &= abs(secant - d) <= h + return ok + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = {"CLOSED_CONTACT": check_closed_contact(), "EARLY_PREFIX": check_early_prefix(), + "TERMINAL_SLACK": check_terminal(), "BR_TORUS": check_br(), "IFT": check_ift()} + passed = all(checks.values()) and len(checks) == 5 + print(json.dumps({"object": "CLAUDE-REVIEW-SARD-R1R2-20260929-v1", "checks": checks, "passed": passed, + "scope": "exact finite controls of the boundary examples only; R1/R2 are reviewed in REVIEW.md"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main())