From 9f2f79bb7a4510417090e77cae14471e1eaf9e18 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 20 Oct 2026 06:53:30 -0500 Subject: [PATCH 1/2] Formalize regular and interior closed-superlevel neighborhood bases (C297) Consume the frozen C296 scalar chart, preserve relative subtype topology, and add a scoped hosted build/kernel/axiom/negative-control verifier. Source and execution evidence retain their distinct scope; no scientific promotion. --- .github/workflows/c297-regular-superlevel.yml | 71 ++ .../HOSTED_SOURCE_MANIFEST.json | 44 ++ .../README.md | 109 +++ .../SOURCE_SCOPE.md | 141 ++++ .../c297_hosted_verify.py | 506 ++++++++++++++ ...483d8a878afe5eaa72f1ea629f0ca5a29760f.lean | 133 ++++ .../development/TEST_FINAL.stderr | 21 + .../development/TEST_FINAL.stdout | 4 + .../development/TEST_FINAL_OPTIMIZED.stderr | 21 + .../development/TEST_FINAL_OPTIMIZED.stdout | 4 + .../development/TEST_WRAPPED_RED.stderr | 34 + .../development/TEST_WRAPPED_RED.stdout | 4 + ...d0d7b7f271fdfc3db377cdb093f7e356f946d.lean | 135 ++++ .../development/linux-candidate1.md | 96 +++ .../development/linux-candidate2.md | 51 ++ .../development/linux-candidate3.md | 45 ++ .../native-candidate1-timeout.json | 30 + .../WithoutCoordinateIdentity.lean | 24 + .../WithoutRegularOrInterior.lean | 22 + .../project/Lifetime.lean | 634 ++++++++++++++++++ .../project/RegularPointChart.lean | 64 ++ .../project/RegularSuperlevel.lean | 140 ++++ .../project/RegularSuperlevelAxiomAudit.lean | 62 ++ .../project/RegularSuperlevelLiteral.lean | 55 ++ .../ANALYTIC_CONTROL_AND_PRELIM_REVIEW.md | 132 ++++ .../reviews/CANDIDATE3_SOURCE_REVIEW.md | 162 +++++ .../HOSTED_ENGINEERING_SOURCE_REVIEW.md | 45 ++ .../reviews/PROJECTION_IDENTITIES.json | 32 + .../test_c297_hosted_verify.py | 193 ++++++ 29 files changed, 3014 insertions(+) create mode 100644 .github/workflows/c297-regular-superlevel.yml create mode 100644 frontiers/regular_superlevel_geometry_20261020/HOSTED_SOURCE_MANIFEST.json create mode 100644 frontiers/regular_superlevel_geometry_20261020/README.md create mode 100644 frontiers/regular_superlevel_geometry_20261020/SOURCE_SCOPE.md create mode 100644 frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/0758454e88cb02ad56483face96483d8a878afe5eaa72f1ea629f0ca5a29760f.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL.stderr create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL.stdout create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL_OPTIMIZED.stderr create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL_OPTIMIZED.stdout create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_WRAPPED_RED.stderr create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_WRAPPED_RED.stdout create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/b5733777504470cc1a2edfff780d0d7b7f271fdfc3db377cdb093f7e356f946d.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/linux-candidate1.md create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/linux-candidate2.md create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/linux-candidate3.md create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/native-candidate1-timeout.json create mode 100644 frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutCoordinateIdentity.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutRegularOrInterior.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/project/Lifetime.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/project/RegularPointChart.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevel.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevelAxiomAudit.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevelLiteral.lean create mode 100644 frontiers/regular_superlevel_geometry_20261020/reviews/ANALYTIC_CONTROL_AND_PRELIM_REVIEW.md create mode 100644 frontiers/regular_superlevel_geometry_20261020/reviews/CANDIDATE3_SOURCE_REVIEW.md create mode 100644 frontiers/regular_superlevel_geometry_20261020/reviews/HOSTED_ENGINEERING_SOURCE_REVIEW.md create mode 100644 frontiers/regular_superlevel_geometry_20261020/reviews/PROJECTION_IDENTITIES.json create mode 100644 frontiers/regular_superlevel_geometry_20261020/test_c297_hosted_verify.py diff --git a/.github/workflows/c297-regular-superlevel.yml b/.github/workflows/c297-regular-superlevel.yml new file mode 100644 index 000000000..1201e225e --- /dev/null +++ b/.github/workflows/c297-regular-superlevel.yml @@ -0,0 +1,71 @@ +name: C297 regular superlevel geometry (hosted Lean, no scientific promotion) +'on': + pull_request: + paths: + - 'frontiers/regular_superlevel_geometry_20261020/**' + - '.github/workflows/c297-regular-superlevel.yml' + - 'formal/lean-toolchain' + - 'formal/lakefile.toml' + - 'formal/lake-manifest.json' + - 'specifications/lean_statements_20261010/Specifications/Lifetime.lean' + push: + branches: [main] + paths: + - 'frontiers/regular_superlevel_geometry_20261020/**' + - '.github/workflows/c297-regular-superlevel.yml' + - 'formal/lean-toolchain' + - 'formal/lakefile.toml' + - 'formal/lake-manifest.json' + - 'specifications/lean_statements_20261010/Specifications/Lifetime.lean' + workflow_dispatch: +permissions: + contents: read +concurrency: + group: c297-${{ github.event_name == 'pull_request' && github.event.pull_request.number || github.run_id }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} +jobs: + c297-hosted-formal: + name: c297-hosted-formal + runs-on: ubuntu-24.04 + timeout-minutes: 205 + env: + LEAN_NUM_THREADS: '2' + # Exact frozen five-module and two-control source manifest. + C297_MANIFEST_SHA256: 'c339a9d1ca5b9ef70f8d581ea0760f11922aba2cd16cbeeb7aba02092b476e94' + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + fetch-depth: 1 + - name: Bind frozen source manifest and verify engineering failure controls + timeout-minutes: 5 + run: | + python3 -B -S frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py source --manifest-sha256 "$C297_MANIFEST_SHA256" + python3 -B -S -m unittest discover -s frontiers/regular_superlevel_geometry_20261020 -p test_c297_hosted_verify.py -v + python3 -B -O -S -m unittest discover -s frontiers/regular_superlevel_geometry_20261020 -p test_c297_hosted_verify.py -v + - name: Install pinned Lean and retrieve dependency cache + timeout-minutes: 15 + uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865 + with: + lake-package-directory: formal + auto-config: 'false' + build: 'false' + test: 'false' + lint: 'false' + use-mathlib-cache: 'true' + use-github-cache: 'false' + - name: Fresh five-module build, four kernel checks, complete audit and two controls + timeout-minutes: 180 + run: | + cd formal + lake env python3 -B -S ../frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py execute --manifest-sha256 "$C297_MANIFEST_SHA256" + - name: Retain exact C297 tested-run sources, objects, streams and failure receipts + if: always() + timeout-minutes: 5 + uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 + with: + name: c297-hosted-${{ github.run_id }}-${{ github.run_attempt }} + path: .lake/c297-hosted-evidence/ + include-hidden-files: true + if-no-files-found: warn + retention-days: 90 diff --git a/frontiers/regular_superlevel_geometry_20261020/HOSTED_SOURCE_MANIFEST.json b/frontiers/regular_superlevel_geometry_20261020/HOSTED_SOURCE_MANIFEST.json new file mode 100644 index 000000000..445e44ffc --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/HOSTED_SOURCE_MANIFEST.json @@ -0,0 +1,44 @@ +{ + "files": { + "negative-project/WithoutCoordinateIdentity.lean": { + "bytes": 950, + "sha256": "167d0afb49457303a61fac6927784e4f0157ed5725739903bf5e33224974b081" + }, + "negative-project/WithoutRegularOrInterior.lean": { + "bytes": 838, + "sha256": "d3c12e33718a00be343d0e2b3cbbd9a1cdf08e8a2062eb3bfeb7026fb47a543d" + }, + "project/Lifetime.lean": { + "bytes": 51383, + "sha256": "90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6" + }, + "project/RegularPointChart.lean": { + "bytes": 2767, + "sha256": "5568c8d6e03f7064cd5924ebe2814ae746100505ae31789d5c975902528f9fa2" + }, + "project/RegularSuperlevel.lean": { + "bytes": 6405, + "sha256": "0db6ce3ea7358a59c089680d774a6806f0fb747c24d9828850377458156e2f02" + }, + "project/RegularSuperlevelAxiomAudit.lean": { + "bytes": 3248, + "sha256": "807de09540b9f7f4f4e14c3408f1f82cb08b1e4232c68c04da5a2355cec02f9e" + }, + "project/RegularSuperlevelLiteral.lean": { + "bytes": 2299, + "sha256": "334759063a3ae58b42b8cd4a45e3bfd6f3a31b668d18526aa6fdcb5ea65c13d3" + } + }, + "schema_version": 1, + "scientific_effect": "NONE", + "source_origins": { + "Lifetime": { + "commit": "8c226134ac0a0169dbb43311082e5353ed5c922c", + "path": "specifications/lean_statements_20261010/Specifications/Lifetime.lean" + }, + "RegularPointChart": { + "commit": "72edcf5b93be45c29f2d10a26f7d8e861a48f528", + "path": "frontiers/regular_point_chart_20261020/RegularPointChart.lean" + } + } +} diff --git a/frontiers/regular_superlevel_geometry_20261020/README.md b/frontiers/regular_superlevel_geometry_20261020/README.md new file mode 100644 index 000000000..26e8802e9 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/README.md @@ -0,0 +1,109 @@ +# Regular-point geometry of closed superlevels + +This packet develops the local topology needed to connect scalar regular-point +charts to closed-superlevel path attainment. Its intended result is a +path-connected neighborhood basis at a prescribed point of the actual closed +superlevel, when that point is regular or lies strictly above the level. + +**Status as of the 2026-10-20 11:42:05 UTC execution report: topology candidate 3 +passed its Linux build and standard named-module kernel replay.** +This covers the six-declaration `RegularSuperlevel` module. Compilation and kernel +verification of the literal consumer, the complete axiom census, both negative +controls, and combined packet verification remain pending. Scientific effect +remains **NONE**. + +For a natural dimension `d`, the literal source is +`E d = EuclideanSpace ℝ (Fin d)`. Given `g : E d → ℝ` and `a : ℝ`, let +`S = {y : E d // a ≤ g y}`. The two public declarations in +`RegularSuperlevelLiteral.lean`, in namespace `TorusRegularSuperlevel`, have the +following scope: + +| Declaration | Assumptions at `x : S` | Intended conclusion | +|---|---|---| +| `closed_superlevel_regular_basis` | `IsSmooth d g` and `¬ IsCriticalPoint d g x.val` | The neighborhood filter of `x` in `S` has a basis of path-connected sets. | +| `closed_superlevel_path_connected_basis` | `IsSmooth d g` and `a < g x.val ∨ ¬ IsCriticalPoint d g x.val` | The same pointwise neighborhood basis. | + +Here `IsSmooth d g` means `∀ n : ℕ, ContDiff ℝ n g`, and literal criticality +means `fderiv ℝ g x.val = 0`. The public statements assume neither a chart nor +local path connectivity of the closed superlevel. The separate +`closed_superlevel_interior_basis` theorem needs only `Continuous g` and +`a < g x.val`; it includes critical points strictly above the level. + +The exact conclusion is + +```lean +(𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => + V ∈ 𝓝 x ∧ IsPathConnected V) + id +``` + +The filter is on the closed-superlevel subtype. For example, with `g(t) = t` +and `a = 0`, the sets `[0, ε)` are path-connected relative neighborhoods of +zero in `[0, ∞)`. They are not ambient neighborhoods of zero in `ℝ`. The packet's +interfaces preserve this distinction. + +The topology module contains six supporting declarations, including the +strict-interior result. It restricts a supplied chart to corresponding relative +source and target neighborhoods, obtains local path connectivity of the model +halfspace from convexity, and transports the resulting basis into `S`. +The two literal consumers obtain their chart from the separately owned C296 +module. The source inventory and exact assumptions are listed in +[SOURCE_SCOPE.md](SOURCE_SCOPE.md). + +The C296 chart remains attributed to **Research Task Watch**. This packet consumes +the [owner-released chart source at commit +`72edcf5b93be45c29f2d10a26f7d8e861a48f528`](https://github.com/d6g8k5htny-coder/Math-/blob/72edcf5b93be45c29f2d10a26f7d8e861a48f528/frontiers/regular_point_chart_20261020/RegularPointChart.lean), +2,767 bytes, SHA-256 +`5568c8d6e03f7064cd5924ebe2814ae746100505ae31789d5c975902528f9fa2`. +Its model factor is the kernel of the actual derivative. The chart's construction, +branch, and tests retain their original ownership; this packet implements their +relative-topology consumer. See the +[C296 owner release](https://github.com/d6g8k5htny-coder/Math-/pull/488#issuecomment-6289952847). + +Execution evidence currently records: + +| Attempt | Observed result | +|---|---| +| Candidate 1, native Darwin | Timed out after 600.061 seconds during observed import reads; no compiler diagnostic or object. | +| [Candidate 1, Claude S Linux execution](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6289663934) | Return code 1 after 48 seconds: three elaboration errors in two declarations, plus four style warnings. No object or kernel replay. | +| [Candidate 2, Claude S Linux execution](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6289854822) | Return code 1 after 47 seconds: one remaining type-inference error. No object or kernel replay. | +| [Candidate 3, Claude S Linux result](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6290047895), following the [exact-source request](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6290009856) | Build return code 0 with warnings treated as errors and empty streams, 12.5 seconds. Standard `leanchecker -v RegularSuperlevel` return code 0, 10.0 seconds. The exact 6,405-byte source remained unchanged. | + +The successful phases were executed by Anthropic Claude, session +`session_01S16677s1SGeAJmN3QMz4ip` (Claude S), on Linux x86_64. +The kernel phase replayed the named topology module against its imported +environment; it was not a `--fresh` dependency-closure replay. The report did not +execute the literal consumer, an axiom census, or the negative controls, and did +not review the mathematics or chart-consumer fit. The C297 source author read +this execution report and did not execute these Linux phases. + +The two negative interface controls deliberately omit, respectively, the +regular-or-strict-interior premise and the chart coordinate identity. They are +intended to reject an unsaturated theorem application after its dependencies +compile. They are not mathematical counterexamples, and an import, syntax, or +resource failure would not establish their intended outcome. + +A separate paper-only analytical control uses +`g(t) = exp(-1/t²) sin(1/t)` for `t ≠ 0`, with `g(0) = 0`. +This function is smooth and infinitely flat at zero. Alternating positive and +negative intervals accumulate at zero, preventing a path-connected relative +neighborhood of zero in `{t | 0 ≤ g(t)}`. It shows why smoothness alone cannot +replace the regular-or-interior condition for arbitrary smooth functions. The +example is non-Morse and does not refute the smooth Morse target. It has not been +formalized or executed as a Lean counterexample. + +Critical points on the boundary level remain outside the present result. +Deriving their local geometry from literal Morse data, transporting the +pointwise result through the actual torus quotient, and proving full closed-level +local path connectivity remain open. The complete ordinary-H0 finite-bar +adapter, exhaustive once-counted bar correspondence, elder pairing, and the +stochastic obligations also remain open. No numerical constants, normalizers, +field laws, or orders of limits are changed by this packet. + +The C297 source author is OpenAI Codex `/root/adapter_feasibility_c292`, +coordinated by OpenAI Codex `/root` for Dylan Roy. Preliminary nonauthor source +review was performed by OpenAI Codex `/root/c292_geometry_review`, with prior +source and proof-shape exposure: same provider, organizational independence 0, +human review 0. Claude S's Linux reports are separately attributed execution +evidence, not mathematical approval. Dylan Roy's personal reading is pending. diff --git a/frontiers/regular_superlevel_geometry_20261020/SOURCE_SCOPE.md b/frontiers/regular_superlevel_geometry_20261020/SOURCE_SCOPE.md new file mode 100644 index 000000000..7824a4f3f --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/SOURCE_SCOPE.md @@ -0,0 +1,141 @@ +# Source identity and mathematical scope + +This document describes the current C297 source candidates and their dependency +boundary. As of the 2026-10-20 11:42:05 UTC report, Claude S's Linux execution +passed compilation and standard named-module kernel replay for topology candidate +3. The literal consumer's compilation and kernel verification, complete axiom +audit, executed interface controls, combined packet verification, and final +acceptance remain pending. Source identities and preliminary source review do not +substitute for those outstanding outcomes. + +The library pin is Mathlib +`d13f23b723b8a846827a245b89c10fc7d3f11612`, with Lean 4.34.1. +The project input `Lifetime.lean` supplies the literal Euclidean space, +smoothness, and criticality definitions. The separately owned C296 source +supplies the regular scalar chart. + +| Source | Bytes | SHA-256 | +|---|---:|---| +| `Lifetime.lean` | 51,383 | `90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6` | +| C296 `RegularPointChart.lean` | 2,767 | `5568c8d6e03f7064cd5924ebe2814ae746100505ae31789d5c975902528f9fa2` | +| C297 `RegularSuperlevel.lean`, candidate 3 | 6,405 | `0db6ce3ea7358a59c089680d774a6806f0fb747c24d9828850377458156e2f02` | +| C297 `RegularSuperlevelLiteral.lean` | 2,299 | `334759063a3ae58b42b8cd4a45e3bfd6f3a31b668d18526aa6fdcb5ea65c13d3` | + +The C296 dependency is fixed to +[commit `72edcf5b93be45c29f2d10a26f7d8e861a48f528`](https://github.com/d6g8k5htny-coder/Math-/blob/72edcf5b93be45c29f2d10a26f7d8e861a48f528/frontiers/regular_point_chart_20261020/RegularPointChart.lean), +released by its Research Task Watch owner. Its chart source is byte-identical to +the earlier interface copy used while preparing the consumer. C297 consumes the +released source with attribution; it does not take ownership of the chart, +its branch, or its tests. + +The local mathematical objects are unchanged: + +```lean +E d = EuclideanSpace ℝ (Fin d) +IsSmooth d g = ∀ n : ℕ, ContDiff ℝ n g +IsCriticalPoint d g x = (fderiv ℝ g x = 0) +``` + +The dimension is any `d : ℕ`; the level is any `a : ℝ`. +Each point is explicitly a member of the actual closed-superlevel subtype +`{y : E d // a ≤ g y}`. The local Euclidean statements require no period, random +field, coefficient field, or limiting operation. This absence does not supply +any quotient or stochastic theorem. + +There are six explicit declarations in the topology layer, all in namespace +`TorusRegularSuperlevel`: + +| Declaration | Exact role and boundary | +|---|---| +| `path_connected_basis_of_openEmbedding` | Transfers the domain's path-connected neighborhood basis to the image of a point under an open embedding. It does not conclude global LPC of the codomain. | +| `path_connected_basis_of_open` | Transfers a basis from an LPC open neighborhood to its point in the ambient space. | +| `relative_chart_homeomorph` | Defines the homeomorphism between `{y : S // y.val ∈ p.source}` and `{z : T // z.val ∈ p.target}`, assuming membership equivalence on the chart source. | +| `path_connected_basis_of_relative_chart` | Derives the basis in `S` at a point in the chart source, using LPC of the corresponding model subset `T`. | +| `closed_superlevel_basis_of_chart` | Supplies the preceding helper with the convex halfspace `{z : ℝ × F | a ≤ z.fst}` and proves its LPC. It requires the actual chart, source membership, and first-coordinate identity on the source. | +| `closed_superlevel_interior_basis` | Derives the basis at a point strictly above the level from `Continuous g` alone. | + +The generic chart theorem allows any real normed-space model factor `F`. +Completeness or finite dimensionality of `F` is not an additional topology +hypothesis. The literal consumer instantiates it with +`F = (fderiv ℝ g x.val).ker`. + +The two literal declarations are: + +```lean +theorem closed_superlevel_regular_basis + {d : ℕ} {g : E d → ℝ} + (hsmooth : IsSmooth d g) + (a : ℝ) (x : {y : E d // a ≤ g y}) + (hregular : ¬ IsCriticalPoint d g x.val) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => + V ∈ 𝓝 x ∧ IsPathConnected V) id + +theorem closed_superlevel_path_connected_basis + {d : ℕ} {g : E d → ℝ} + (hsmooth : IsSmooth d g) + (a : ℝ) (x : {y : E d // a ≤ g y}) + (hx : a < g x.val ∨ ¬ IsCriticalPoint d g x.val) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => + V ∈ 𝓝 x ∧ IsPathConnected V) id +``` + +These are the source interfaces awaiting completed verification. Neither accepts +a desired path, a supplied chart, a finite event list, or LPC of the closed +superlevel as a public premise. The regular branch obtains the chart from C296's +`regularPointChart`, source membership from `mem_regularPointChart_source`, +and the coordinate identity from `regularPointChart_fst`. The interior branch +uses the continuous strict superlevel as an open neighborhood. + +The final neighborhood filter in every closed-superlevel conclusion is on the +subtype. The intermediate chart intersections are open relative to their source +and target subsets. Ambient openness of a closed halfspace is never required. +Chart inverse transport is restricted to its actual target. + +The following distinctions remain necessary when interpreting evidence: + +- The observed native candidate-1 run reached its 600-second bound with no + diagnostic or object; process sampling showed import reading. +- [Claude S's candidate-1 execution](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6289663934) + reached elaboration and failed after 48 seconds. The author corrected the + basis witness construction, explicit subtype membership, and style warnings. +- [Claude S's candidate-2 execution](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6289854822) + failed after 47 seconds on the restricted identity map's inferred source and + topology. Candidate 3 makes those types explicit. +- The [candidate-3 execution request](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6290009856) + was followed by the [actual Linux result](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6290047895): + topology build return code 0 under warnings-as-errors in 12.5 seconds, then + standard `leanchecker -v RegularSuperlevel` return code 0 in 10.0 seconds. + The exact 6,405-byte source with SHA-256 + `0db6ce3ea7358a59c089680d774a6806f0fb747c24d9828850377458156e2f02` + remained unchanged. The executor was Anthropic Claude, session + `session_01S16677s1SGeAJmN3QMz4ip` (Claude S). This was execution-only evidence + for the six-declaration topology module, with no `--fresh` replay, literal + consumer execution, complete axiom census, negative-control execution, or + mathematical review. The C297 author read the report and did not run those + Linux phases. +- Preliminary OpenAI nonauthor source review is same-provider and source-exposed, + with organizational independence 0 and human review 0. It is not final + acceptance or a kernel result. +- The two deliberately incomplete theorem invocations are interface controls. + Their intended missing-premise errors must be distinguished from unrelated + syntax, import, or resource failures. +- The smooth oscillatory example discussed in the README is a paper-only + non-Morse control. It is not a formal counterexample or a counterexample to + the smooth Morse target. + +The remaining mathematical obligations include critical-boundary Morse geometry, +transport through the actual torus quotient, and LPC of the entire closed +critical-death superlevel. A per-point result restricted to regular or interior +points does not discharge those obligations. Strict death drop, the full +ordinary-H0 finite-bar adapter, the all-small-bars converse, regional shrinking +collisions, exhaustive once-counted bars, and actual elder pairing also remain +open. No branch-adjacency or local trap assertion is promoted to a pairing. + +The stochastic field, probability assumptions, numerical constants, density +normalizers, and orders of limits are unchanged. Scientific effect is NONE. +The source author is OpenAI Codex `/root/adapter_feasibility_c292`, coordinated +by OpenAI Codex `/root` for Dylan Roy. The separately attributed C296 owner and +Claude S executor retain their respective roles. Dylan Roy's personal reading +is pending. diff --git a/frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py b/frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py new file mode 100644 index 000000000..518053213 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py @@ -0,0 +1,506 @@ +#!/usr/bin/env python3 +"""C297 scoped hosted verification; no scientific promotion or human review. + +Run from the existing pinned formal/ Lake environment. Sources are pinned by an +explicit manifest digest in the dedicated workflow. Every attempt retains exact +streams and a receipt before any failure is raised. No retry is performed. +""" +import argparse +from datetime import datetime, timezone +import hashlib +import json +import os +from pathlib import Path +import platform +import re +import shutil +import signal +import subprocess +import time + +PREFIX = 'frontiers/regular_superlevel_geometry_20261020' +WORKFLOW = '.github/workflows/c297-regular-superlevel.yml' +MANIFEST = 'HOSTED_SOURCE_MANIFEST.json' +MODULES = ('Lifetime', 'RegularPointChart', 'RegularSuperlevel', + 'RegularSuperlevelLiteral', 'RegularSuperlevelAxiomAudit') +REPLAY_MODULES = MODULES[1:] +AUDIT_MODULES = MODULES[:4] +NEGATIVES = ('WithoutRegularOrInterior', 'WithoutCoordinateIdentity') +ALLOWED_AXIOMS = {'propext', 'Classical.choice', 'Quot.sound'} +REQUIRED = tuple('UniversalLaw.Spec.Lifetime.' + x for x in ( + 'IsSmooth', 'IsCriticalPoint', 'regularPointDerivative_range_eq_top', + 'regularPointHasStrictFDerivAt', 'regularPointChart', 'regularPointChart_fst', + 'regularPointChart_self', 'mem_regularPointChart_source', + 'mem_regularPointChart_target')) + tuple('TorusRegularSuperlevel.' + x for x in ( + 'path_connected_basis_of_openEmbedding', 'path_connected_basis_of_open', + 'relative_chart_homeomorph', 'path_connected_basis_of_relative_chart', + 'closed_superlevel_basis_of_chart', 'closed_superlevel_interior_basis', + 'closed_superlevel_regular_basis', 'closed_superlevel_path_connected_basis')) +MATHLIB_PIN = 'd13f23b723b8a846827a245b89c10fc7d3f11612' +LEAN_VERSION = '4.34.1' +PACKAGE_PINS = { + 'plausible': '118aa17ee84656b8bd727fef7c458ee8c833385c', + 'LeanSearchClient': 'ddf04cf3949fa556442341e87d47f9f6e6074707', + 'importGraph': 'e928b72544873815af278d38681b31c0293588e3', + 'proofwidgets': '106ff4fafc74ef4ac99d81dbf3ab399118f497a5', + 'aesop': '355695d523e41d0554926416cba2a2b3544fbbc9', + 'Qq': '6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259', + 'batteries': 'f2effa3d803fda822b1f97b806c47cf2adfbcbc2', + 'Cli': 'e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204', + 'mathlib': MATHLIB_PIN, +} + + +def now(): + return datetime.now(timezone.utc).isoformat() + + +def identity(path): + data = Path(path).read_bytes() + return {'bytes': len(data), 'sha256': hashlib.sha256(data).hexdigest()} + + +def safe_source(path, root): + path, root = Path(path).absolute(), Path(root).absolute() + if not path.is_relative_to(root): + raise RuntimeError(f'source outside repository: {path}') + parts = path.relative_to(root).parts + for n in range(1, len(parts) + 1): + if root.joinpath(*parts[:n]).is_symlink(): + raise RuntimeError(f'symlinked source: {path}') + if not path.is_file(): + raise RuntimeError(f'source missing or not regular: {path}') + + +def verify_file(path, expected, root): + safe_source(path, root) + if (set(expected) != {'bytes', 'sha256'} or + type(expected['bytes']) is not int or expected['bytes'] < 1 or + not re.fullmatch('[0-9a-f]{64}', expected['sha256'])): + raise RuntimeError(f'invalid expected source identity: {path}') + actual = identity(path) + if actual != expected: + raise RuntimeError(f'source identity mismatch: {path}: {actual}') + return actual + + +def verify_sources(root, manifest_sha256): + root = Path(root) + packet = root / PREFIX + path = packet / MANIFEST + safe_source(path, root) + if not re.fullmatch('[0-9a-f]{64}', manifest_sha256): + raise RuntimeError('explicit frozen manifest SHA-256 required') + if identity(path)['sha256'] != manifest_sha256: + raise RuntimeError('frozen source manifest identity mismatch') + manifest = json.loads(path.read_text()) + if manifest.get('schema_version') != 1 or manifest.get('scientific_effect') != 'NONE': + raise RuntimeError('invalid C297 manifest schema or scientific-effect field') + expected = {f'project/{m}.lean' for m in MODULES} | { + f'negative-project/{m}.lean' for m in NEGATIVES} + if set(manifest.get('files', {})) != expected: + raise RuntimeError('manifest must bind exactly five modules and two controls') + sources = {rel: verify_file(packet / rel, spec, root) + for rel, spec in manifest['files'].items()} + origins = manifest.get('source_origins', {}) + if set(origins) != {'Lifetime', 'RegularPointChart'}: + raise RuntimeError('both frozen input source origins are required') + for name, origin in origins.items(): + if (not isinstance(origin, dict) or not re.fullmatch('[0-9a-f]{40}', origin.get('commit', '')) + or not isinstance(origin.get('path'), str) or not origin['path'] + or Path(origin['path']).is_absolute() or '..' in Path(origin['path']).parts): + raise RuntimeError(f'invalid input source origin: {name}') + upstream = root / 'specifications/lean_statements_20261010/Specifications/Lifetime.lean' + verify_file(upstream, manifest['files']['project/Lifetime.lean'], root) + config = {} + for rel in ('formal/lean-toolchain', 'formal/lakefile.toml', 'formal/lake-manifest.json'): + safe_source(root / rel, root) + config[rel] = identity(root / rel) + if (root / 'formal/lean-toolchain').read_text().strip() != 'leanprover/lean4:v' + LEAN_VERSION: + raise RuntimeError('Lean toolchain pin changed') + if f'rev = "{MATHLIB_PIN}"' not in (root / 'formal/lakefile.toml').read_text(): + raise RuntimeError('Lake mathlib pin changed') + lock = json.loads((root / 'formal/lake-manifest.json').read_text()) + if {p['name']: p['rev'] for p in lock['packages']} != PACKAGE_PINS: + raise RuntimeError('dependency lock pins changed') + support = {} + for rel in (WORKFLOW, PREFIX + '/c297_hosted_verify.py', + PREFIX + '/test_c297_hosted_verify.py'): + safe_source(root / rel, root) + support[rel] = identity(root / rel) + return {'manifest': identity(path), 'files': sources, 'source_origins': origins, + 'source_origin_limit': 'Remote origin byte equality is a separate owner custody check.', + 'formal_config': config, 'support_files': support, 'dependency_pins': PACKAGE_PINS} + + +def audit_records(output): + """Join Lean's wrapped AXIOMS arrays; reject interrupted or truncated records.""" + pending = None + for line in output.splitlines(): + if pending is not None: + if 'SUPERLEVEL_AUDIT_' in line: + raise RuntimeError('audit declaration interrupted before closing axiom list') + pending += ' ' + line.strip() + if ']' in line: + yield pending + pending = None + continue + if 'SUPERLEVEL_AUDIT_' not in line: + continue + marker = line[line.index('SUPERLEVEL_AUDIT_'):].strip() + if marker.startswith('SUPERLEVEL_AUDIT_PROGRESS '): + continue + if marker.startswith('SUPERLEVEL_AUDIT_DECL ') and 'AXIOMS [' in marker and ']' not in marker: + pending = marker + continue + yield marker + if pending is not None: + raise RuntimeError('truncated audit axiom list') + + +def validate_audit(output, modules=AUDIT_MODULES, required=REQUIRED): + """Read every module-origin record, not just a total or public-name sample.""" + counts, names, current, seen = {}, {}, None, set() + total = None + for marker in audit_records(output): + m = re.fullmatch(r'SUPERLEVEL_AUDIT_MODULE (\S+) COUNT (\d+)', marker) + if m: + current, count = m.group(1), int(m.group(2)) + if total is not None or current not in modules or current in counts or count < 1: + raise RuntimeError('invalid or duplicate audit module census') + counts[current], names[current] = count, [] + continue + m = re.fullmatch(r'SUPERLEVEL_AUDIT_DECL (\S+) AXIOMS \[([^\[\]]*)\]', marker) + if m: + name, raw_axioms = m.groups() + axioms = {s.strip() for s in raw_axioms.split(',') if s.strip()} + if current is None or total is not None or name in seen or not axioms <= ALLOWED_AXIOMS: + raise RuntimeError('invalid, repeated or forbidden audit declaration') + names[current].append(name) + seen.add(name) + continue + m = re.fullmatch(r'SUPERLEVEL_AUDIT_STANDARD_ONLY_PASS COUNT (\d+)', marker) + if m and total is None: + total = int(m.group(1)) + continue + raise RuntimeError(f'unrecognized or repeated audit marker: {marker}') + if (tuple(counts) != tuple(modules) or total != len(seen) or total != sum(counts.values()) + or any(len(names[m]) != counts[m] for m in counts) + or not set(required) <= seen): + raise RuntimeError('incomplete audit census or missing required target') + return {'module_counts': counts, 'declaration_count': total, + 'required_targets': list(required), 'allowed_axioms': sorted(ALLOWED_AXIOMS), + 'module_declarations': names} + + +def validate_negative(name, returncode, output): + flat = ' '.join(output.split()) + forbidden = ('unknown identifier', 'unknown module', 'file not found', 'no such file', + 'memory_exception', 'out of memory', 'unexpected token', 'unsolved goals', + 'maximum recursion', 'maximum heartbeats', 'failed to', 'panic', 'sorry') + if (returncode != 1 or output.count('error:') != 1 or 'error: Type mismatch' not in flat + or 'has type' not in flat or 'but is expected to have type' not in flat + or 'HasBasis' not in flat or '→' not in flat + or any(x in flat.lower() for x in forbidden)): + raise RuntimeError('negative control failed for an unrelated reason') + if name == 'WithoutRegularOrInterior': + ok = ('closed_superlevel_path_connected_basis hsmooth a x' in flat + and re.search(r'a\s*<\s*g\s', flat) and '∨' in flat and '¬' in flat + and 'IsCriticalPoint d g' in flat) + elif name == 'WithoutCoordinateIdentity': + ok = ('closed_superlevel_basis_of_chart a x p hx' in flat and '∀' in flat + and 'p.source' in flat and re.search(r'\(p y\)\.(?:fst|1)\s*=\s*g y', flat)) + else: + raise RuntimeError('unknown negative control') + if not ok: + raise RuntimeError('negative control did not reject its intended missing premise') + + +def save_report(evidence, report): + (evidence / 'RESULT.json').write_text(json.dumps(report, indent=2, sort_keys=True) + '\n') + + +def save_phase(evidence, report, record): + (evidence / (record['name'] + '.receipt.json')).write_text( + json.dumps(record, indent=2, sort_keys=True) + '\n') + save_report(evidence, report) + + +def object_inventory(build): + result = {} + for path in sorted(Path(build).iterdir()): + safe_source(path, build) + result[path.name] = identity(path) + return result + + +def validate_objects(before, after, build_module=None): + if any(after.get(name) != spec for name, spec in before.items()): + raise RuntimeError('previous local input object changed or disappeared') + additions = set(after) - set(before) + if build_module is None: + if additions: + raise RuntimeError('non-build phase added an unexpected local object') + return + allowed = {build_module + suffix for suffix in + ('.olean', '.olean.private', '.olean.server', '.ilean', '.ir')} + if build_module + '.olean' not in additions or not additions <= allowed: + raise RuntimeError('build must add only its own target object outputs') + + +def run_phase(name, args, cwd, env, evidence, report, expected_success=True, + timeout=900, build_dir=None, build_module=None): + """Persist raw streams, per-phase receipt, and aggregate receipt before raise.""" + if not re.fullmatch('[A-Za-z0-9_-]+', name): + raise RuntimeError('unsafe phase name') + evidence = Path(evidence) + out_path, err_path = evidence / (name + '.stdout'), evidence / (name + '.stderr') + start, utc_start = time.monotonic(), now() + timed_out, spawn_error, code = False, None, None + objects_before, objects_after, object_error = None, None, None + with out_path.open('xb') as stdout, err_path.open('xb') as stderr: + try: + if build_dir is not None: + objects_before = object_inventory(build_dir) + except (OSError, RuntimeError) as exc: + object_error = str(exc) + if object_error is None: + try: + proc = subprocess.Popen(args, cwd=cwd, env=env, stdout=stdout, stderr=stderr, + start_new_session=True) + try: + code = proc.wait(timeout=timeout) + except subprocess.TimeoutExpired: + timed_out = True + try: + os.killpg(proc.pid, signal.SIGTERM) + except ProcessLookupError: + pass + try: + code = proc.wait(timeout=5) + except subprocess.TimeoutExpired: + try: + os.killpg(proc.pid, signal.SIGKILL) + except ProcessLookupError: + pass + code = proc.wait(timeout=5) + except (OSError, subprocess.TimeoutExpired) as exc: + spawn_error = str(exc) + if build_dir is not None: + try: + objects_after = object_inventory(build_dir) + if object_error is None: + validate_objects(objects_before, objects_after, build_module) + except (OSError, RuntimeError) as exc: + object_error = str(exc) + valid = (not timed_out and spawn_error is None and object_error is None and + (code == 0 if expected_success else code == 1)) + record = {'name': name, 'command': list(args), 'cwd': str(cwd), + 'started_at': utc_start, 'finished_at': now(), + 'duration_seconds': round(time.monotonic() - start, 6), + 'timeout_seconds': timeout, 'timed_out': timed_out, + 'spawn_error': spawn_error, 'exit_code': code, + 'stdout_sha256': identity(out_path)['sha256'], 'stdout_bytes': out_path.stat().st_size, + 'stderr_sha256': identity(err_path)['sha256'], 'stderr_bytes': err_path.stat().st_size, + 'objects_before': objects_before, 'objects_after': objects_after, + 'object_validation_error': object_error, + 'status': 'PASS' if valid else 'FAIL'} + report['phase_results'].append(record) + save_phase(evidence, report, record) + print(f'C297 {name}: exit={code} timeout={timed_out} seconds={record["duration_seconds"]}', flush=True) + if not valid: + raise RuntimeError(f'C297 {name} unexpected exit: {code}; timed_out={timed_out}; ' + f'spawn_error={spawn_error}; object_error={object_error}') + output = out_path.read_bytes().decode('utf8', 'replace') + '\n' + err_path.read_bytes().decode('utf8', 'replace') + return record, output, code + + +def git(root, *args): + return subprocess.check_output(['git', *args], cwd=root, text=True, timeout=30).strip() + + +def verify_packages(root): + result = {} + for name, expected in PACKAGE_PINS.items(): + path = root / 'formal/.lake/packages' / name + actual = git(path, 'rev-parse', 'HEAD') + if actual != expected or git(path, 'status', '--porcelain', '--untracked-files=no'): + raise RuntimeError(f'installed dependency mismatch or tracked change: {name}') + result[name] = actual + return result + + +def hosted_context(root): + keys = ('GITHUB_SHA', 'GITHUB_RUN_ID', 'GITHUB_RUN_ATTEMPT', 'GITHUB_REPOSITORY', + 'GITHUB_EVENT_NAME', 'GITHUB_WORKFLOW', 'GITHUB_JOB') + if any(not os.environ.get(k) for k in keys): + raise RuntimeError('actual GitHub execution context required') + if os.environ['GITHUB_REPOSITORY'] != 'd6g8k5htny-coder/Math-': + raise RuntimeError('wrong repository') + head = git(root, 'rev-parse', 'HEAD') + if head != os.environ['GITHUB_SHA']: + raise RuntimeError('tested checkout does not match GITHUB_SHA') + context = {k.lower(): os.environ[k] for k in keys} + context['tested_commit'] = head + context['tested_tree'] = git(root, 'rev-parse', 'HEAD^{tree}') + context['tested_parents'] = git(root, 'show', '-s', '--format=%P', 'HEAD').split() + event_path = Path(os.environ.get('GITHUB_EVENT_PATH', '/nonexistent')) + if event_path.is_file(): + event = json.loads(event_path.read_text()) + if 'pull_request' in event: + context['pull_request'] = { + 'number': event['number'], 'head_sha': event['pull_request']['head']['sha'], + 'base_sha': event['pull_request']['base']['sha']} + context['executor'] = 'GitHub-hosted runner executing C297 verification code' + context['human_review_credit'] = 0 + return context + + +def source_only(root, digest): + evidence = root / '.lake/c297-hosted-evidence' + evidence.mkdir(parents=True, exist_ok=False) + report = {'status': 'HOLD_SOURCE_PREFLIGHT', 'scientific_effect': 'NONE', + 'phase_results': [], 'started_at': now()} + save_report(evidence, report) + try: + report['context'] = hosted_context(root) + report['source_identity'] = verify_sources(root, digest) + snapshots = evidence / 'source-snapshot' + for relative in report['source_identity']['files']: + dest = snapshots / relative + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(root / PREFIX / relative, dest) + shutil.copyfile(root / PREFIX / MANIFEST, evidence / MANIFEST) + for relative in report['source_identity']['support_files']: + dest = snapshots / 'repository' / relative + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(root / relative, dest) + report['status'] = 'PASS_SOURCE_PREFLIGHT_ONLY' + except BaseException as exc: + report['status'], report['failure'] = 'HOLD_SOURCE_PREFLIGHT_FAILED', repr(exc) + raise + finally: + save_report(evidence, report) + + +def execute(root, digest): + packet, formal = root / PREFIX, root / 'formal' + evidence = root / '.lake/c297-hosted-evidence' + report = json.loads((evidence / 'RESULT.json').read_text()) + if report['status'] != 'PASS_SOURCE_PREFLIGHT_ONLY' or report['phase_results']: + raise RuntimeError('exact unused source preflight required; no automatic retry') + build = evidence / 'objects' + build.mkdir(exist_ok=False) + report.update(status='HOLD_NOT_COMPLETED', started_execution_at=now(), + memory_limit='-M14000', threads=2, phase_timeout_seconds=900, + memory_limit_reason='Explicit Linux execution budget; not a claim that C297 requires this amount.', + verification_scope='Five fresh local objects; four standard named-module kernel replays; full four-module axiom census; two omitted-premise interface controls.', + replay_limit='Not a --fresh replay or rebuild of the full dependency closure.') + save_report(evidence, report) + try: + context = hosted_context(root) + if context != report['context']: + raise RuntimeError('execution context changed since source preflight') + source_before = verify_sources(root, digest) + if source_before != report['source_identity']: + raise RuntimeError('inputs changed since source preflight') + report['packages_before'] = verify_packages(root) + env = dict(os.environ) + env['LEAN_PATH'] = str(build) + os.pathsep + env.get('LEAN_PATH', '') + env['LEAN_NUM_THREADS'] = '2' + launcher = shutil.which('lean') + if launcher is None: + raise RuntimeError('missing Lean launcher') + launcher = Path(launcher).resolve() + report['lean_launcher'] = {'path': str(launcher), **identity(launcher)} + # Resolve the toolchain prefix through the selected launcher, then execute + # the measured toolchain binaries directly; an elan shim is not the runtime. + _, prefix_output, _ = run_phase('runtime-print-prefix', + [str(launcher), '--print-prefix'], formal, env, evidence, report, timeout=30) + prefix = Path(prefix_output.strip()) + if not prefix.is_absolute() or not prefix.is_dir(): + raise RuntimeError('Lean did not return an existing absolute toolchain prefix') + runtimes = {} + for executable in ('lean', 'leanchecker'): + binary = (prefix / 'bin' / executable).resolve() + if not binary.is_file() or not os.access(binary, os.X_OK): + raise RuntimeError(f'missing toolchain runtime: {executable}') + runtimes[executable] = {'path': str(binary), **identity(binary)} + report['runtimes'] = runtimes + report['machine'] = {'platform': platform.platform(), 'machine': platform.machine(), + 'python': platform.python_version()} + _, version, _ = run_phase('runtime-version', [runtimes['lean']['path'], '--version'], + formal, env, evidence, report, timeout=30) + if 'version ' + LEAN_VERSION not in version: + raise RuntimeError('wrong Lean runtime version') + report['lean_version_output'] = version + for module in MODULES: + args = [runtimes['lean']['path'], '-j2', '-M14000'] + if module != 'Lifetime': + args += ['-DwarningAsError=true'] + args += ['-o', str(build / (module + '.olean')), + str(packet / 'project' / (module + '.lean'))] + rec, output, _ = run_phase('build-' + module, args, packet / 'project', env, evidence, report, + build_dir=build, build_module=module) + obj = build / (module + '.olean') + safe_source(obj, evidence) + rec['object'] = identity(obj) + if module == 'RegularSuperlevelAxiomAudit': + report['audit'] = validate_audit(output) + if verify_sources(root, digest) != source_before: + raise RuntimeError('inputs changed during build') + save_phase(evidence, report, rec) + built_objects = object_inventory(build) + expected_main = {m + '.olean' for m in MODULES} + allowed_outputs = {m + suffix for m in MODULES for suffix in + ('.olean', '.olean.private', '.olean.server', '.ilean', '.ir')} + if not expected_main <= set(built_objects) or not set(built_objects) <= allowed_outputs: + raise RuntimeError('unexpected complete final object set') + report['objects_after_builds'] = built_objects + save_report(evidence, report) + for module in REPLAY_MODULES: + run_phase('kernel-' + module, [runtimes['leanchecker']['path'], '-v', module], + packet / 'project', env, evidence, report, build_dir=build) + for name in NEGATIVES: + rec, output, code = run_phase('negative-' + name, + [runtimes['lean']['path'], '-j2', '-M14000', str(packet / 'negative-project' / (name + '.lean'))], + packet / 'negative-project', env, evidence, report, expected_success=False, + build_dir=build) + validate_negative(name, code, output) + rec['intended_missing_premise_rejection'] = True + save_phase(evidence, report, rec) + report['packages_after'] = verify_packages(root) + report['source_identity_after'] = verify_sources(root, digest) + if report['source_identity_after'] != source_before: + raise RuntimeError('inputs changed during verification') + for executable, spec in runtimes.items(): + if identity(spec['path']) != {k: spec[k] for k in ('bytes', 'sha256')}: + raise RuntimeError(f'runtime changed: {executable}') + report['objects'] = object_inventory(build) + if report['objects'] != built_objects: + raise RuntimeError('local objects changed during kernel or negative phases') + report['status'] = 'PASS_HOSTED_C297_EXACT_TARGETS' + report['completed_at'] = now() + print('C297_HOSTED_FORMAL_PASS: scoped formal execution only; scientific effect NONE.', flush=True) + except BaseException as exc: + report['status'], report['failure'] = 'HOLD_NOT_COMPLETED', repr(exc) + raise + finally: + save_report(evidence, report) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('mode', choices=('source', 'execute')) + parser.add_argument('--manifest-sha256', required=True) + args = parser.parse_args() + # Published location is exactly frontiers//c297_hosted_verify.py. + root = Path(__file__).resolve().parents[2] + if args.mode == 'source': + source_only(root, args.manifest_sha256) + else: + execute(root, args.manifest_sha256) + + +if __name__ == '__main__': + main() diff --git a/frontiers/regular_superlevel_geometry_20261020/development/0758454e88cb02ad56483face96483d8a878afe5eaa72f1ea629f0ca5a29760f.lean b/frontiers/regular_superlevel_geometry_20261020/development/0758454e88cb02ad56483face96483d8a878afe5eaa72f1ea629f0ca5a29760f.lean new file mode 100644 index 000000000..2b528b9bc --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/0758454e88cb02ad56483face96483d8a878afe5eaa72f1ea629f0ca5a29760f.lean @@ -0,0 +1,133 @@ +import Lifetime + +/-! +Relative topology for closed scalar superlevels. + +The chart-input theorem below is a reusable topology adapter. It does not construct +a chart from a nonzero derivative: that literal scalar-chart obligation is separately +owned. No critical-point Morse chart or global closed-level LPC is asserted here. +-/ + +open Set Filter Topology +open UniversalLaw.Spec.Lifetime + +namespace TorusRegularSuperlevel + +/-- An open embedding carries a path-connected neighborhood basis to its image point. -/ +theorem path_connected_basis_of_openEmbedding + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + [LocallyPathConnectedSpace X] {e : X → Y} + (he : IsOpenEmbedding e) (x : X) : + (𝓝 (e x)).HasBasis + (fun V : Set Y => V ∈ 𝓝 (e x) ∧ IsPathConnected V) id := by + rw [hasBasis_self] + intro U hU + have hpre : e ⁻¹' U ∈ 𝓝 x := + he.continuous.continuousAt.preimage_mem_nhds hU + obtain ⟨V, ⟨hV, hpath⟩, hVU⟩ := (path_connected_basis x).mem_iff.mp hpre + refine ⟨e '' V, ⟨he.image_mem_nhds.mpr hV, hpath.image he.continuous⟩, ?_⟩ + exact image_subset_iff.mpr hVU + +/-- An LPC open neighborhood supplies the required basis in the ambient space. -/ +theorem path_connected_basis_of_open + {X : Type*} [TopologicalSpace X] {U : Set X} + (hU : IsOpen U) [LocallyPathConnectedSpace U] {x : X} (hx : x ∈ U) : + (𝓝 x).HasBasis (fun V : Set X => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + exact path_connected_basis_of_openEmbedding hU.isOpenEmbedding_subtypeVal ⟨x, hx⟩ + +/-- Restrict a chart to two corresponding subsets, using their relative open +source and target. Neither subset is required to be open in its original ambient space. -/ +def relative_chart_homeomorph + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + (p : OpenPartialHomeomorph X Y) (S : Set X) (T : Set Y) + (hmem : ∀ y ∈ p.source, y ∈ S ↔ p y ∈ T) : + {y : S // y.val ∈ p.source} ≃ₜ {z : T // z.val ∈ p.target} where + toFun y := ⟨⟨p y.val.val, (hmem y.val.val y.property).mp y.val.property⟩, + p.map_source y.property⟩ + invFun z := ⟨⟨p.symm z.val.val, + (hmem (p.symm z.val.val) (p.map_target z.property)).mpr + (by rw [p.right_inv z.property]; exact z.val.property)⟩, + p.map_target z.property⟩ + left_inv y := by + apply Subtype.ext + apply Subtype.ext + exact p.left_inv y.property + right_inv z := by + apply Subtype.ext + apply Subtype.ext + exact p.right_inv z.property + continuous_toFun := by + apply Continuous.subtype_mk + apply Continuous.subtype_mk + exact p.continuousOn.comp_continuous + (continuous_subtype_val.comp continuous_subtype_val) (fun y => y.property) + continuous_invFun := by + apply Continuous.subtype_mk + apply Continuous.subtype_mk + exact p.continuousOn_symm.comp_continuous + (continuous_subtype_val.comp continuous_subtype_val) (fun z => z.property) + +/-- Relative chart transport derives a neighborhood basis in the source subset +from LPC of the model subset. This helper is consumed with a proved convex halfspace. -/ +theorem path_connected_basis_of_relative_chart + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + (p : OpenPartialHomeomorph X Y) (S : Set X) (T : Set Y) + [LocallyPathConnectedSpace T] + (hmem : ∀ y ∈ p.source, y ∈ S ↔ p y ∈ T) + (x : S) (hx : x.val ∈ p.source) : + (𝓝 x).HasBasis (fun V : Set S => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let U : Set S := {y | y.val ∈ p.source} + let V : Set T := {z | z.val ∈ p.target} + have hU : IsOpen U := p.open_source.preimage continuous_subtype_val + have hV : IsOpen V := p.open_target.preimage continuous_subtype_val + letI : LocallyPathConnectedSpace V := hV.locallyPathConnectedSpace + let h : U ≃ₜ V := relative_chart_homeomorph p S T hmem + letI : LocallyPathConnectedSpace U := h.symm.locallyPathConnectedSpace + exact path_connected_basis_of_open hU hx + +/-- A scalar chart supplies the actual closed-superlevel neighborhood basis. + +The coordinate identity is needed only on the chart source. This theorem proves +the relative-topology step; the separately owned literal regular-point constructor +must supply `p`, `hx`, and `hcoord` before a noncritical-point corollary is claimed. -/ +theorem closed_superlevel_basis_of_chart + {d : ℕ} {g : E d → ℝ} {F : Type*} + [NormedAddCommGroup F] [NormedSpace ℝ F] + (a : ℝ) (x : {y : E d // a ≤ g y}) + (p : OpenPartialHomeomorph (E d) (ℝ × F)) + (hx : x.val ∈ p.source) + (hcoord : ∀ y ∈ p.source, (p y).fst = g y) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let H : Set (ℝ × F) := {z | a ≤ z.fst} + have hconvex : Convex ℝ H := by + intro u hu v hv s t hs ht hst + change a ≤ s • u.fst + t • v.fst + calc + a = s • a + t • a := (Convex.combo_self hst a).symm + _ ≤ s • u.fst + t • v.fst := + add_le_add (smul_le_smul_of_nonneg_left hu hs) + (smul_le_smul_of_nonneg_left hv ht) + letI : LocallyPathConnectedSpace H := hconvex.locallyPathConnectedSpace + apply path_connected_basis_of_relative_chart p {y | a ≤ g y} H _ x hx + intro y hy + change a ≤ g y ↔ a ≤ (p y).fst + rw [hcoord y hy] + +/-- A point strictly above the level has a path-connected neighborhood basis in +the closed superlevel, with continuity alone and no regularity assumption. -/ +theorem closed_superlevel_interior_basis + {d : ℕ} {g : E d → ℝ} (hg : Continuous g) + (a : ℝ) (x : {y : E d // a ≤ g y}) (hx : a < g x.val) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let S : Set (E d) := {y | a ≤ g y} + let U : Set (E d) := {y | a < g y} + have hU : IsOpen U := isOpen_lt continuous_const hg + letI : LocallyPathConnectedSpace U := hU.locallyPathConnectedSpace + let e : U → S := fun y => ⟨y.val, le_of_lt y.property⟩ + have he : IsOpenEmbedding e := by + exact IsOpenEmbedding.id.restrict (fun y hy => le_of_lt hy) hU + exact path_connected_basis_of_openEmbedding he ⟨x.val, hx⟩ + +end TorusRegularSuperlevel diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL.stderr b/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL.stderr new file mode 100644 index 000000000..89231fb15 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL.stderr @@ -0,0 +1,21 @@ +test_amended_phase_receipt_matches_aggregate (test_c297_hosted_verify.HostedVerifierTests) +Semantic/object metadata must not exist only in the aggregate receipt. ... ok +test_audit_cannot_omit_required_target_or_hide_axiom (test_c297_hosted_verify.HostedVerifierTests) +Count-only validation would accept a substituted target or sorryAx. ... ok +test_build_allows_only_its_own_outputs (test_c297_hosted_verify.HostedVerifierTests) +A build may add its target object, not an unrelated replacement. ... ok +test_failed_phase_receipt_and_exact_streams_survive_abort (test_c297_hosted_verify.HostedVerifierTests) +Raising before persistence would discard the actual failing phase. ... ok +test_fake_negative_or_import_failure_cannot_pass (test_c297_hosted_verify.HostedVerifierTests) +Exit-only or theorem-name-only validation accepts the wrong rejection. ... ok +test_modified_source_bytes_are_rejected (test_c297_hosted_verify.HostedVerifierTests) +Dropping size/hash verification would accept the modified file. ... ok +test_phase_rejects_imported_object_mutation (test_c297_hosted_verify.HostedVerifierTests) +A successful compiler process may not alter a prior input object. ... ok +test_timeout_preserves_partial_stream_and_receipt (test_c297_hosted_verify.HostedVerifierTests) +Timeout handling must not discard the child output or phase result. ... ok + +---------------------------------------------------------------------- +Ran 8 tests in 0.187s + +OK diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL.stdout b/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL.stdout new file mode 100644 index 000000000..51b20db4b --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL.stdout @@ -0,0 +1,4 @@ +C297 valid-phase: exit=0 timeout=False seconds=0.023972 +C297 deliberate-failure: exit=7 timeout=False seconds=0.021278 +C297 deliberate-object-mutation: exit=0 timeout=False seconds=0.022951 +C297 deliberate-timeout: exit=-15 timeout=True seconds=0.104077 diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL_OPTIMIZED.stderr b/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL_OPTIMIZED.stderr new file mode 100644 index 000000000..19786ca53 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL_OPTIMIZED.stderr @@ -0,0 +1,21 @@ +test_amended_phase_receipt_matches_aggregate (test_c297_hosted_verify.HostedVerifierTests) +Semantic/object metadata must not exist only in the aggregate receipt. ... ok +test_audit_cannot_omit_required_target_or_hide_axiom (test_c297_hosted_verify.HostedVerifierTests) +Count-only validation would accept a substituted target or sorryAx. ... ok +test_build_allows_only_its_own_outputs (test_c297_hosted_verify.HostedVerifierTests) +A build may add its target object, not an unrelated replacement. ... ok +test_failed_phase_receipt_and_exact_streams_survive_abort (test_c297_hosted_verify.HostedVerifierTests) +Raising before persistence would discard the actual failing phase. ... ok +test_fake_negative_or_import_failure_cannot_pass (test_c297_hosted_verify.HostedVerifierTests) +Exit-only or theorem-name-only validation accepts the wrong rejection. ... ok +test_modified_source_bytes_are_rejected (test_c297_hosted_verify.HostedVerifierTests) +Dropping size/hash verification would accept the modified file. ... ok +test_phase_rejects_imported_object_mutation (test_c297_hosted_verify.HostedVerifierTests) +A successful compiler process may not alter a prior input object. ... ok +test_timeout_preserves_partial_stream_and_receipt (test_c297_hosted_verify.HostedVerifierTests) +Timeout handling must not discard the child output or phase result. ... ok + +---------------------------------------------------------------------- +Ran 8 tests in 0.189s + +OK diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL_OPTIMIZED.stdout b/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL_OPTIMIZED.stdout new file mode 100644 index 000000000..46b8373d1 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_FINAL_OPTIMIZED.stdout @@ -0,0 +1,4 @@ +C297 valid-phase: exit=0 timeout=False seconds=0.021434 +C297 deliberate-failure: exit=7 timeout=False seconds=0.020063 +C297 deliberate-object-mutation: exit=0 timeout=False seconds=0.023834 +C297 deliberate-timeout: exit=-15 timeout=True seconds=0.107555 diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_WRAPPED_RED.stderr b/frontiers/regular_superlevel_geometry_20261020/development/TEST_WRAPPED_RED.stderr new file mode 100644 index 000000000..434d99cbe --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_WRAPPED_RED.stderr @@ -0,0 +1,34 @@ +test_amended_phase_receipt_matches_aggregate (test_c297_hosted_verify.HostedVerifierTests) +Semantic/object metadata must not exist only in the aggregate receipt. ... ok +test_audit_cannot_omit_required_target_or_hide_axiom (test_c297_hosted_verify.HostedVerifierTests) +Count-only validation would accept a substituted target or sorryAx. ... ok +test_build_allows_only_its_own_outputs (test_c297_hosted_verify.HostedVerifierTests) +A build may add its target object, not an unrelated replacement. ... ok +test_failed_phase_receipt_and_exact_streams_survive_abort (test_c297_hosted_verify.HostedVerifierTests) +Raising before persistence would discard the actual failing phase. ... ok +test_fake_negative_or_import_failure_cannot_pass (test_c297_hosted_verify.HostedVerifierTests) +Exit-only or theorem-name-only validation accepts the wrong rejection. ... ok +test_modified_source_bytes_are_rejected (test_c297_hosted_verify.HostedVerifierTests) +Dropping size/hash verification would accept the modified file. ... ok +test_phase_rejects_imported_object_mutation (test_c297_hosted_verify.HostedVerifierTests) +A successful compiler process may not alter a prior input object. ... ok +test_pinned_lean_multiline_axiom_records (test_c297_hosted_verify.HostedVerifierTests) +Actual pinned Lean wraps the unchanged Lifetime axiom arrays. ... ERROR +test_timeout_preserves_partial_stream_and_receipt (test_c297_hosted_verify.HostedVerifierTests) +Timeout handling must not discard the child output or phase result. ... ok + +====================================================================== +ERROR: test_pinned_lean_multiline_axiom_records (test_c297_hosted_verify.HostedVerifierTests) +Actual pinned Lean wraps the unchanged Lifetime axiom arrays. +---------------------------------------------------------------------- +Traceback (most recent call last): + File "$C297_ROOT/hosted/test_c297_hosted_verify.py", line 70, in test_pinned_lean_multiline_axiom_records + self.assertEqual(v.validate_audit(proper, **args)['declaration_count'], 1) + File "$C297_ROOT/hosted/c297_hosted_verify.py", line 164, in validate_audit + raise RuntimeError(f'unrecognized or repeated audit marker: {marker}') +RuntimeError: unrecognized or repeated audit marker: SUPERLEVEL_AUDIT_DECL UniversalLaw.Spec.Lifetime.IsUnrestrictedLeadingCoefficient AXIOMS [propext, + +---------------------------------------------------------------------- +Ran 9 tests in 0.212s + +FAILED (errors=1) diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_WRAPPED_RED.stdout b/frontiers/regular_superlevel_geometry_20261020/development/TEST_WRAPPED_RED.stdout new file mode 100644 index 000000000..c726fc8fe --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_WRAPPED_RED.stdout @@ -0,0 +1,4 @@ +C297 valid-phase: exit=0 timeout=False seconds=0.024216 +C297 deliberate-failure: exit=7 timeout=False seconds=0.020853 +C297 deliberate-object-mutation: exit=0 timeout=False seconds=0.037492 +C297 deliberate-timeout: exit=-15 timeout=True seconds=0.110072 diff --git a/frontiers/regular_superlevel_geometry_20261020/development/b5733777504470cc1a2edfff780d0d7b7f271fdfc3db377cdb093f7e356f946d.lean b/frontiers/regular_superlevel_geometry_20261020/development/b5733777504470cc1a2edfff780d0d7b7f271fdfc3db377cdb093f7e356f946d.lean new file mode 100644 index 000000000..c5fd520ad --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/b5733777504470cc1a2edfff780d0d7b7f271fdfc3db377cdb093f7e356f946d.lean @@ -0,0 +1,135 @@ +import Lifetime + +/-! +Relative topology for closed scalar superlevels. + +The chart-input theorem below is a reusable topology adapter. It does not construct +a chart from a nonzero derivative: that literal scalar-chart obligation is separately +owned. No critical-point Morse chart or global closed-level LPC is asserted here. +-/ + +open Set Filter Topology +open UniversalLaw.Spec.Lifetime + +namespace TorusRegularSuperlevel + +/-- An open embedding carries a path-connected neighborhood basis to its image point. -/ +theorem path_connected_basis_of_openEmbedding + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + [LocallyPathConnectedSpace X] {e : X → Y} + (he : IsOpenEmbedding e) (x : X) : + (𝓝 (e x)).HasBasis + (fun V : Set Y => V ∈ 𝓝 (e x) ∧ IsPathConnected V) id := by + rw [hasBasis_self] + intro U hU + have hpre : e ⁻¹' U ∈ 𝓝 x := + he.continuous.continuousAt.preimage_mem_nhds hU + obtain ⟨V, ⟨hV, hpath⟩, hVU⟩ := (path_connected_basis x).mem_iff.mp hpre + refine ⟨e '' V, he.image_mem_nhds.mpr hV, hpath.image he.continuous, ?_⟩ + exact image_subset_iff.mpr hVU + +/-- An LPC open neighborhood supplies the required basis in the ambient space. -/ +theorem path_connected_basis_of_open + {X : Type*} [TopologicalSpace X] {U : Set X} + (hU : IsOpen U) [LocallyPathConnectedSpace U] {x : X} (hx : x ∈ U) : + (𝓝 x).HasBasis (fun V : Set X => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + exact path_connected_basis_of_openEmbedding hU.isOpenEmbedding_subtypeVal ⟨x, hx⟩ + +/-- Restrict a chart to two corresponding subsets, using their relative open +source and target. Neither subset is required to be open in its original ambient space. -/ +def relative_chart_homeomorph + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + (p : OpenPartialHomeomorph X Y) (S : Set X) (T : Set Y) + (hmem : ∀ y ∈ p.source, y ∈ S ↔ p y ∈ T) : + {y : S // y.val ∈ p.source} ≃ₜ {z : T // z.val ∈ p.target} where + toFun y := ⟨⟨p y.val.val, (hmem y.val.val y.property).mp y.val.property⟩, + p.map_source y.property⟩ + invFun z := ⟨⟨p.symm z.val.val, + (hmem (p.symm z.val.val) (p.map_target z.property)).mpr + (by rw [p.right_inv z.property]; exact z.val.property)⟩, + p.map_target z.property⟩ + left_inv y := by + apply Subtype.ext + apply Subtype.ext + exact p.left_inv y.property + right_inv z := by + apply Subtype.ext + apply Subtype.ext + exact p.right_inv z.property + continuous_toFun := by + apply Continuous.subtype_mk + apply Continuous.subtype_mk + exact p.continuousOn.comp_continuous + (continuous_subtype_val.comp continuous_subtype_val) (fun y => y.property) + continuous_invFun := by + apply Continuous.subtype_mk + apply Continuous.subtype_mk + exact p.continuousOn_symm.comp_continuous + (continuous_subtype_val.comp continuous_subtype_val) (fun z => z.property) + +/-- Relative chart transport derives a neighborhood basis in the source subset +from LPC of the model subset. This helper is consumed with a proved convex halfspace. -/ +theorem path_connected_basis_of_relative_chart + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + (p : OpenPartialHomeomorph X Y) (S : Set X) (T : Set Y) + [LocallyPathConnectedSpace T] + (hmem : ∀ y ∈ p.source, y ∈ S ↔ p y ∈ T) + (x : S) (hx : x.val ∈ p.source) : + (𝓝 x).HasBasis (fun V : Set S => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let U : Set S := {y | y.val ∈ p.source} + let V : Set T := {z | z.val ∈ p.target} + have hU : IsOpen U := p.open_source.preimage continuous_subtype_val + have hV : IsOpen V := p.open_target.preimage continuous_subtype_val + let : LocallyPathConnectedSpace V := hV.locallyPathConnectedSpace + let h : U ≃ₜ V := relative_chart_homeomorph p S T hmem + let : LocallyPathConnectedSpace U := h.symm.locallyPathConnectedSpace + exact path_connected_basis_of_open hU hx + +/-- A scalar chart supplies the actual closed-superlevel neighborhood basis. + +The coordinate identity is needed only on the chart source. This theorem proves +the relative-topology step; the separately owned literal regular-point constructor +must supply `p`, `hx`, and `hcoord` before a noncritical-point corollary is claimed. -/ +theorem closed_superlevel_basis_of_chart + {d : ℕ} {g : E d → ℝ} {F : Type*} + [NormedAddCommGroup F] [NormedSpace ℝ F] + (a : ℝ) (x : {y : E d // a ≤ g y}) + (p : OpenPartialHomeomorph (E d) (ℝ × F)) + (hx : x.val ∈ p.source) + (hcoord : ∀ y ∈ p.source, (p y).fst = g y) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let H : Set (ℝ × F) := {z | a ≤ z.fst} + have hconvex : Convex ℝ H := by + intro u hu v hv s t hs ht hst + change a ≤ s • u.fst + t • v.fst + calc + a = s • a + t • a := (Convex.combo_self hst a).symm + _ ≤ s • u.fst + t • v.fst := + add_le_add (smul_le_smul_of_nonneg_left hu hs) + (smul_le_smul_of_nonneg_left hv ht) + let : LocallyPathConnectedSpace H := hconvex.locallyPathConnectedSpace + apply path_connected_basis_of_relative_chart p {y | a ≤ g y} H _ x hx + intro y hy + change a ≤ g y ↔ a ≤ (p y).fst + rw [hcoord y hy] + +/-- A point strictly above the level has a path-connected neighborhood basis in +the closed superlevel, with continuity alone and no regularity assumption. -/ +theorem closed_superlevel_interior_basis + {d : ℕ} {g : E d → ℝ} (hg : Continuous g) + (a : ℝ) (x : {y : E d // a ≤ g y}) (hx : a < g x.val) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let S : Set (E d) := {y | a ≤ g y} + let U : Set (E d) := {y | a < g y} + have hU : IsOpen U := isOpen_lt continuous_const hg + let : LocallyPathConnectedSpace U := hU.locallyPathConnectedSpace + let e : U → S := fun y => ⟨y.val, by + change a ≤ g y.val + exact le_of_lt (show a < g y.val from y.property)⟩ + have he : IsOpenEmbedding e := by + exact IsOpenEmbedding.id.restrict (fun y hy => le_of_lt hy) hU + exact path_connected_basis_of_openEmbedding he ⟨x.val, hx⟩ + +end TorusRegularSuperlevel diff --git a/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate1.md b/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate1.md new file mode 100644 index 000000000..143d7213d --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate1.md @@ -0,0 +1,96 @@ +**RESULT (data only): the compile FAILS, rc 1, in 48 s, with 3 errors in 2 of the 6 declarations. No object was produced, so the `leanchecker` step did not run. This releases my pickup [6289611672](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6289611672).** Anthropic Claude, session `session_01S16677s1SGeAJmN3QMz4ip` (Claude S), for the C297 request [6289589748](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6289589748). Credit 0. Scientific effect NONE. + +**What ran.** One attempt in a new isolated directory, with no retry and no edit. +- Command: `$LEAN_RUNTIME/bin/lean -j2 -M14000 -o $ISO/build/RegularSuperlevel.olean $ISO/project/RegularSuperlevel.lean`, run in `$ISO/project`. +- `LEAN_PATH`: `$ISO/build`, then the 8 pinned package build directories. `LEAN_NUM_THREADS=2`. The cap was 900 s. +- Executables: `lean` `e8baaa71…5d5550`, `leanchecker` `ccef1bfe…696fcbe`. Mathlib `d13f23b7` and its 8 packages are built from source. +- Inputs: source `0758454e…a29760f`, 6,173 B, and `Lifetime.olean` `b3e14c29…`. Both have the same hashes after the run. + +**Outcome.** +- rc 1, no timeout, 48.0 s wall time, peak RSS 6.28 GiB. +- Stderr is empty. Stdout is 2,626 B, SHA-256 `466574b2…ed209`. With my local directory projected to `$ISO`, it is 2,087 B, SHA-256 `8b828f78…5db45`, reproduced in full below. +- No `RegularSuperlevel.olean` was written. Unlike the Darwin attempt, the imports finished and elaboration reached all six declarations. + +**The errors, read against Mathlib `d13f23b7`.** These describe what the compiler reports; they are not a fix and not a review of the mathematics. +1. **`path_connected_basis_of_openEmbedding`, 28:18 and 29:2.** + - After `rw [hasBasis_self]`, the goal is `∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t` (`Mathlib/Order/Filter/Bases/Basic.lean:330–331`). + - So after the witness, the anonymous constructor expects three flat parts: membership, then `IsPathConnected`, then the subset. + - Line 28 nests membership and `IsPathConnected` together. The 29:2 message confirms the shape: the remaining `?_` is `IsPathConnected (e '' V) ∧ e '' V ⊆ U`. +2. **`closed_superlevel_interior_basis`, 128:36.** + - The proof part of `⟨y.val, le_of_lt y.property⟩` is expected to have type `↑y ∈ S`, where `S` is `let`-bound. + - The elaborator does not unfold it to the `?a ≤ ?b` that `le_of_lt` produces. + - No later error was reported in this declaration. Because of error recovery, that is not evidence the rest is correct. + +**What the clean declarations do and do not show.** +- `path_connected_basis_of_open`, `relative_chart_homeomorph`, `path_connected_basis_of_relative_chart` and `closed_superlevel_basis_of_chart` gave no errors. +- The only other messages are `linter.style.haveILetI` warnings at lines 83, 85, 111 and 127. +- However, Lean adds a declaration that failed to elaborate with `sorryAx`. Three of those four depend on `path_connected_basis_of_openEmbedding`, directly or transitively. So their clean elaboration does not make them sorry-free. + +**Limits.** +- Execution only, under these pins on Linux. I did not review the mathematics or check its fit with the C296 chart interface. +- I did not test `-M4096`. +- No source was edited and nothing was retried. + +**Availability.** If the C297 author posts an amended candidate with its exact bytes and hash, I can run it the same way under a new pickup. + +**RELEASE.** I hold nothing on C297 or #487. + +
Full stdout, local directory projected to $ISO (2,087 B, SHA-256 8b828f78…5db45) + +```text +$ISO/project/RegularSuperlevel.lean:28:18: error: Invalid `⟨...⟩` notation: The expected type `(𝓝 (e x)).1 (e '' V)` is not an inductive type + +Note: This notation can only be used when the expected type is an inductive type with a single constructor +$ISO/project/RegularSuperlevel.lean:29:2: error: Type mismatch + image_subset_iff.mpr hVU +has type + e '' id V ⊆ U +but is expected to have type + IsPathConnected (e '' V) ∧ e '' V ⊆ U +$ISO/project/RegularSuperlevel.lean:83:2: warning: Try this: + letI̵ + +The goal is a proposition, so `let` is preferred over `letI`. +The difference between `let` and `letI` is that `letI` inlines the value. +But this is not relevant for proofs because of proof irrelevance. + +Note: This linter can be disabled with `set_option linter.style.haveILetI false` +$ISO/project/RegularSuperlevel.lean:85:2: warning: Try this: + letI̵ + +The goal is a proposition, so `let` is preferred over `letI`. +The difference between `let` and `letI` is that `letI` inlines the value. +But this is not relevant for proofs because of proof irrelevance. + +Note: This linter can be disabled with `set_option linter.style.haveILetI false` +$ISO/project/RegularSuperlevel.lean:111:2: warning: Try this: + letI̵ + +The goal is a proposition, so `let` is preferred over `letI`. +The difference between `let` and `letI` is that `letI` inlines the value. +But this is not relevant for proofs because of proof irrelevance. + +Note: This linter can be disabled with `set_option linter.style.haveILetI false` +$ISO/project/RegularSuperlevel.lean:127:2: warning: Try this: + letI̵ + +The goal is a proposition, so `let` is preferred over `letI`. +The difference between `let` and `letI` is that `letI` inlines the value. +But this is not relevant for proofs because of proof irrelevance. + +Note: This linter can be disabled with `set_option linter.style.haveILetI false` +$ISO/project/RegularSuperlevel.lean:128:36: error: Application type mismatch: The argument + le_of_lt ?m.78 +has type + ?m.74 ≤ ?m.75 +but is expected to have type + ↑y ∈ S +in the application + ⟨↑y, ⋯⟩ +``` + +
+ + +--- +_Generated by [Claude Code](https://claude.ai/code)_ diff --git a/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate2.md b/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate2.md new file mode 100644 index 000000000..2baaf3e98 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate2.md @@ -0,0 +1,51 @@ +**RESULT (data only): candidate 2 FAILS to compile, rc 1, in 47.0 s, with exactly one error, in `closed_superlevel_interior_basis`. No object was produced, so the `leanchecker` step did not run. This releases my pickup [6289816152](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6289816152).** Anthropic Claude, session `session_01S16677s1SGeAJmN3QMz4ip` (Claude S), for request [6289752268](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6289752268). Credit 0. Scientific effect NONE. + +**Identities (full SHA-256).** +- Source `RegularSuperlevel.lean`, 6,225 B: `b5733777504470cc1a2edfff780d0d7b7f271fdfc3db377cdb093f7e356f946d`. It is the same after the run. +- Import `Lifetime.olean`: `b3e14c2951b452222ca0c7b1448458cf785225971da704e4e3e6f0cc93107da4`, from `Lifetime.lean` `90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6`. It is the same after the run. +- `lean`: `e8baaa71855a616dc351028f3ad2200051b0671f423a1696a100e809302d5550`. `leanchecker`: `ccef1bfe9bfeecea65137d94a69033c1a89f360711f50fa3178e7ba3e696fcbe`. +- Stdout, native: 372 B, `6c6b62012dbaefc5402d359fa44c1885a426c5b89b9e3b30456291e3b7468d89`. +- Stdout, projected: 295 B, `48df07a396adecc54ebed2f24c8660da62c8576ee4708f4e77b7ed0e977f5b24`. The only difference is that the native stream has my isolated directory's absolute path where the projected text has `$ISO`, once. I publish the projected text, since the native path is a private local path. +- Stderr: 0 B, `e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855`. +- Object: none. + +**Run.** `$LEAN_RUNTIME/bin/lean -j2 -M14000 -DwarningAsError=true -o $ISO/build/RegularSuperlevel.olean $ISO/project/RegularSuperlevel.lean`, run in `$ISO/project`, with the same `LEAN_PATH` as candidate 1. No timeout against the 900 s cap; peak RSS 6.27 GiB. There was one attempt, with no edit or retry. + +**Full stdout (projected):** +```text +$ISO/project/RegularSuperlevel.lean:132:64: error: Application type mismatch: The argument + hU +has type + IsOpen U +but is expected to have type + IsOpen[?m.104] fun y => Preorder.toLT.1 ?m.115 (id y) +in the application + IsOpenEmbedding.restrict IsOpenEmbedding.id (fun y hy => le_of_lt hy) hU +``` + +**Reading of the error, against Mathlib `d13f23b7`.** This is diagnostics only, not a fix or a review. +- At line 132, `Topology.IsOpenEmbedding.restrict` has the signature `(hf : IsOpenEmbedding f) {s : Set X} {t : Set Y} (H : s.MapsTo f t) (hs : IsOpen s)`, in `Mathlib/Topology/Constructions.lean:586–588`. +- The implicit `s` was elaborated from the `MapsTo` lambda `fun y hy => le_of_lt hy`, not from `U`. The message shows the resulting set `fun y => Preorder.toLT.1 ?m.115 (id y)`, with an unresolved topology instance `?m.104`. So `hU : IsOpen U` does not fit. +- This error sits after the line-128 error that candidate 1 reported. As I cautioned then, that error's recovery left this one unreported. + +**The other declarations.** +- Lines 28, 83, 85, 111 and 127–130 now produce no messages. +- Because warnings were errors, there were none at all. +- No message names any of the other five declarations, and none of the five depends on `closed_superlevel_interior_basis`. +- Without an object, no kernel check ran on any declaration. + +
Compact JSON receipt (2,289 B including final newline, SHA-256 d4ff44232c383499271993c476775911d7d619f74df6aa81a5042044e0467309) + +```json +{"cwd":"$ISO/project","edits":0,"env":{"LEAN_NUM_THREADS":"2","PATH":"$LEAN_RUNTIME/bin:/usr/bin:/bin:/usr/sbin:/sbin"},"executor":"Anthropic Claude session_01S16677s1SGeAJmN3QMz4ip","identities":{"Lifetime.lean":"90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6","Lifetime.olean":"b3e14c2951b452222ca0c7b1448458cf785225971da704e4e3e6f0cc93107da4","RegularSuperlevel.lean":"b5733777504470cc1a2edfff780d0d7b7f271fdfc3db377cdb093f7e356f946d","RegularSuperlevel.lean_bytes":6225,"lean":"e8baaa71855a616dc351028f3ad2200051b0671f423a1696a100e809302d5550","leanchecker":"ccef1bfe9bfeecea65137d94a69033c1a89f360711f50fa3178e7ba3e696fcbe"},"lean_path":["$ISO/build","$PINNED_PROJECT/.lake/packages/plausible/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/LeanSearchClient/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/importGraph/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/proofwidgets/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/aesop/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/Qq/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/batteries/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/mathlib/.lake/build/lib/lean"],"lifetime_olean_after_sha256":"b3e14c2951b452222ca0c7b1448458cf785225971da704e4e3e6f0cc93107da4","phases":[{"cap_s":900,"command":["$LEAN_RUNTIME/bin/lean","-j2","-M14000","-DwarningAsError=true","-o","$ISO/build/RegularSuperlevel.olean","$ISO/project/RegularSuperlevel.lean"],"object":null,"peak_rss_kib":6577592,"phase":"build","rc":1,"started_utc":"2026-10-20T11:28:07.469515+00:00","stderr_bytes":0,"stderr_sha256":"e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855","stdout_native_bytes":372,"stdout_native_sha256":"6c6b62012dbaefc5402d359fa44c1885a426c5b89b9e3b30456291e3b7468d89","stdout_projected_bytes":295,"stdout_projected_sha256":"48df07a396adecc54ebed2f24c8660da62c8576ee4708f4e77b7ed0e977f5b24","timeout":false,"wall_s":47.0},{"phase":"kernel","ran":false,"reason":"build rc 1, no object"}],"pickup":6289816152,"platform":"Linux x86_64","request":6289752268,"retries":0,"source_after_sha256":"b5733777504470cc1a2edfff780d0d7b7f271fdfc3db377cdb093f7e356f946d","toolchain":"Lean 4.34.1; Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612 + 8 pinned packages built from source"} +``` + +
+ +**Availability.** I can run a candidate 3 the same way, under a new pickup, if asked within the parent claim. + +**RELEASE.** I hold nothing on C297 or #487. + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ diff --git a/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate3.md b/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate3.md new file mode 100644 index 000000000..c4fc7495a --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/linux-candidate3.md @@ -0,0 +1,45 @@ +**RESULT (data only): candidate 3 compiles and kernel-checks. Build rc 0 under `-DwarningAsError=true`, with empty streams. Then `leanchecker -v RegularSuperlevel` rc 0. This releases my pickup [6290023089](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6290023089).** Anthropic Claude, session `session_01S16677s1SGeAJmN3QMz4ip` (Claude S), for request [6290009856](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6290009856). Credit 0. Scientific effect NONE. + +**Identities (full SHA-256).** +- Source `RegularSuperlevel.lean`, 6,405 B: `0db6ce3ea7358a59c089680d774a6806f0fb747c24d9828850377458156e2f02`. It is the same after both phases. +- Import `Lifetime.olean`: `b3e14c2951b452222ca0c7b1448458cf785225971da704e4e3e6f0cc93107da4`, from `Lifetime.lean` `90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6`. It is the same after both phases. +- `lean`: `e8baaa71855a616dc351028f3ad2200051b0671f423a1696a100e809302d5550`. `leanchecker`: `ccef1bfe9bfeecea65137d94a69033c1a89f360711f50fa3178e7ba3e696fcbe`. +- **Object `RegularSuperlevel.olean`**: 208,992 B, `cffe26cd70fb2b8e2ddf965562a794745a1358bc22e012a85953578d14220526`. It is the same after the kernel phase. + +**Phase 1, build.** +- Command: `$LEAN_RUNTIME/bin/lean -j2 -M14000 -DwarningAsError=true -o $ISO/build/RegularSuperlevel.olean $ISO/project/RegularSuperlevel.lean`, run in `$ISO/project` with the same `LEAN_PATH` as before. +- rc 0, no timeout, 12.5 s against the 900 s cap, peak RSS 6.40 GiB. +- Stdout and stderr are both 0 B, `e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855`. Since Lean reports any use of `sorry` as a warning, rc 0 under warnings-as-errors means no declaration elaborated with `sorry`. + +**Phase 2, kernel.** +- Command: `$LEAN_RUNTIME/bin/leanchecker -v RegularSuperlevel`, a standard named-module replay against the imported environment, not `--fresh`. +- rc 0, no timeout, 10.0 s, peak RSS 5.84 GiB. +- Stdout is 28 B, `92c0c414a888780c0722d6767245b01bd449841486bdd45f93f47c116fe57b0b`. It contains no local path, so native and projected bytes are the same. In full: + ```text + replaying RegularSuperlevel + ``` +- Stderr is 0 B, `e3b0c442…`. + +**Also checked.** A text scan of the source finds none of the tokens `sorry`, `admit`, `axiom`, `native_decide`, `implemented_by`, `extern`, `unsafe` or `opaque`. That is a text check, not an axiom census. + +**Limits.** +- No axiom census was run, since it was not requested. No `--fresh` replay. +- The object hash is Linux evidence only. I make no claim about Darwin or hosted object bytes. +- I did not review the mathematics. I did not check its fit with the C296 chart at `72edcf5b` or with the literal consumer. +- The wall time is much shorter than for candidates 1 and 2 (47–48 s), probably because of a warm file cache. That is not a performance claim. + +
Compact JSON receipt (2,864 B including final newline, SHA-256 3f479a7fc32198389acb8d9db23f913495a5357b1ae1e56cd39e6107074e9ef0) + +```json +{"cwd":"$ISO/project","edits":0,"env":{"LEAN_NUM_THREADS":"2","PATH":"$LEAN_RUNTIME/bin:/usr/bin:/bin:/usr/sbin:/sbin"},"executor":"Anthropic Claude session_01S16677s1SGeAJmN3QMz4ip","identities":{"Lifetime.lean":"90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6","Lifetime.olean":"b3e14c2951b452222ca0c7b1448458cf785225971da704e4e3e6f0cc93107da4","RegularSuperlevel.lean":"0db6ce3ea7358a59c089680d774a6806f0fb747c24d9828850377458156e2f02","RegularSuperlevel.lean_bytes":6405,"lean":"e8baaa71855a616dc351028f3ad2200051b0671f423a1696a100e809302d5550","leanchecker":"ccef1bfe9bfeecea65137d94a69033c1a89f360711f50fa3178e7ba3e696fcbe"},"lean_path":["$ISO/build","$PINNED_PROJECT/.lake/packages/plausible/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/LeanSearchClient/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/importGraph/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/proofwidgets/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/aesop/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/Qq/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/batteries/.lake/build/lib/lean","$PINNED_PROJECT/.lake/packages/mathlib/.lake/build/lib/lean"],"lifetime_olean_after_sha256":"b3e14c2951b452222ca0c7b1448458cf785225971da704e4e3e6f0cc93107da4","phases":[{"cap_s":900,"command":["$LEAN_RUNTIME/bin/lean","-j2","-M14000","-DwarningAsError=true","-o","$ISO/build/RegularSuperlevel.olean","$ISO/project/RegularSuperlevel.lean"],"object":"$ISO/build/RegularSuperlevel.olean","object_bytes":208992,"object_sha256":"cffe26cd70fb2b8e2ddf965562a794745a1358bc22e012a85953578d14220526","peak_rss_kib":6715900,"phase":"build","rc":0,"started_utc":"2026-10-20T11:40:47.252903+00:00","stderr_bytes":0,"stderr_sha256":"e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855","stdout_bytes":0,"stdout_sha256":"e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855","timeout":false,"wall_s":12.5},{"cap_s":900,"command":["$LEAN_RUNTIME/bin/leanchecker","-v","RegularSuperlevel"],"object_sha256_after":"cffe26cd70fb2b8e2ddf965562a794745a1358bc22e012a85953578d14220526","peak_rss_kib":6125856,"phase":"kernel","rc":0,"scope":"standard named-module replay against imported environment; not --fresh","started_utc":"2026-10-20T11:40:59.767709+00:00","stderr_bytes":0,"stderr_sha256":"e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855","stdout_bytes":28,"stdout_projection":"none needed (no local path in stream)","stdout_sha256":"92c0c414a888780c0722d6767245b01bd449841486bdd45f93f47c116fe57b0b","timeout":false,"wall_s":10.0}],"pickup":6290023089,"platform":"Linux x86_64","request":6290009856,"retries":0,"source_after_sha256":"0db6ce3ea7358a59c089680d774a6806f0fb747c24d9828850377458156e2f02","toolchain":"Lean 4.34.1; Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612 + 8 pinned packages built from source"} +``` + +
+ +**Availability.** If asked, I can do a separate pickup for a Linux `#print axioms` census of the six declarations, or a replay of the C297 consumer once its exact bytes exist. + +**RELEASE.** I hold nothing on C297 or #487. The isolated directories for all three candidates are retained. + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ diff --git a/frontiers/regular_superlevel_geometry_20261020/development/native-candidate1-timeout.json b/frontiers/regular_superlevel_geometry_20261020/development/native-candidate1-timeout.json new file mode 100644 index 000000000..2a1aea279 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/native-candidate1-timeout.json @@ -0,0 +1,30 @@ +{ + "source": "RegularSuperlevel.lean", + "source_sha256": "0758454e88cb02ad56483face96483d8a878afe5eaa72f1ea629f0ca5a29760f", + "started_utc": "2026-10-20T11:02:55.466480+00:00", + "command": [ + "$DARWIN_LEAN_RUNTIME/bin/lean", + "-j2", + "-M4096", + "-o", + "$C297_ROOT/build/RegularSuperlevel.olean", + "$C297_ROOT/project/RegularSuperlevel.lean" + ], + "source_snapshot": "source-attempts/RegularSuperlevel/0758454e88cb02ad56483face96483d8a878afe5eaa72f1ea629f0ca5a29760f.lean", + "timeout_seconds": 600, + "threads": 2, + "wrapper_pid": 70729, + "child_pid": 70732, + "returncode": -15, + "timed_out": true, + "seconds": 600.061396125, + "ended_utc": "2026-10-20T11:12:55.539940+00:00", + "source_unchanged": true, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "public_projection": { + "original_bytes": 1174, + "original_sha256": "aa5917b0135820231992dab3f7be1f075c9d34be61260e5905d2bb1ca8dea14b", + "scope": "Native C297 and Darwin runtime path prefixes only replaced with placeholders." + } +} diff --git a/frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutCoordinateIdentity.lean b/frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutCoordinateIdentity.lean new file mode 100644 index 000000000..cb3575107 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutCoordinateIdentity.lean @@ -0,0 +1,24 @@ +import RegularSuperlevel + +/-! +Intentionally ill-typed interface control; not a theorem or a counterexample. + +After the actual imported module compiles, the invocation below must be rejected: +it supplies the chart and source-membership proof but omits the final coordinate +identity on the chart source. The resulting function cannot inhabit the requested +neighborhood-basis proposition. Import or syntax failure does not satisfy this +control. This draft has not been executed. +-/ + +open Set Filter Topology +open UniversalLaw.Spec.Lifetime + +example {d : ℕ} {g : E d → ℝ} {F : Type*} + [NormedAddCommGroup F] [NormedSpace ℝ F] + (a : ℝ) (x : {y : E d // a ≤ g y}) + (p : OpenPartialHomeomorph (E d) (ℝ × F)) + (hx : x.val ∈ p.source) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => + V ∈ 𝓝 x ∧ IsPathConnected V) id := by + exact TorusRegularSuperlevel.closed_superlevel_basis_of_chart a x p hx diff --git a/frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutRegularOrInterior.lean b/frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutRegularOrInterior.lean new file mode 100644 index 000000000..02028d249 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutRegularOrInterior.lean @@ -0,0 +1,22 @@ +import RegularSuperlevelLiteral + +/-! +Intentionally ill-typed interface control; not a theorem or a counterexample. + +After the actual imported modules compile, the invocation below must be rejected: +it supplies all preceding arguments but omits the final regular-or-strict-interior +premise. The resulting function cannot inhabit the requested neighborhood-basis +proposition. Import or syntax failure does not satisfy this control. +This draft has not been executed. +-/ + +open Set Filter Topology +open UniversalLaw.Spec.Lifetime + +example {d : ℕ} {g : E d → ℝ} + (hsmooth : IsSmooth d g) + (a : ℝ) (x : {y : E d // a ≤ g y}) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => + V ∈ 𝓝 x ∧ IsPathConnected V) id := by + exact TorusRegularSuperlevel.closed_superlevel_path_connected_basis hsmooth a x diff --git a/frontiers/regular_superlevel_geometry_20261020/project/Lifetime.lean b/frontiers/regular_superlevel_geometry_20261020/project/Lifetime.lean new file mode 100644 index 000000000..f2508f7f2 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/project/Lifetime.lean @@ -0,0 +1,634 @@ +import Mathlib + +/-! +# Lifetime-track statements: parent Theorems A, B, C, the bounded remainder R and the +# planar elder lower bound / density gap (statements only) + +Scientific effect: NONE. Formal progress of every declaration here: `specified`. +Organizational-independence credit of this transcription: 0 (Anthropic / Claude). + +This module states, as `Prop`-valued definitions, the shapes of the parent lifetime +results (1.1), (1.2), (1.3) of UNIFORM_MATRIX_CAP_AND_LIFETIME.md, of the bounded +remainder (R1) of LIFETIME_REMAINDER.md, and of the planar lower bound (E2), the +two-sided rate (E4) and the compact-window density gap (E11) of +ELDER_LOWER_AND_DENSITY_GAP.md. Every statement is parametrised by interface objects +(the Gaussian field, the superlevel-bar / elder-partner relation, and the typed pair law +probability `p_r(b,k,R)`); it is a statement about whatever objects satisfy those +interfaces, and the identification of those objects with the objects of the source texts +is not part of the statement. + +This module is self-contained: it imports only Mathlib and re-declares, verbatim up to +the namespace, the shared objects of `Specifications/Field.lean` (covariance, field +interface, critical points, Hessian inertia, pairs, superlevel bars, density versions). +The duplication is deliberate at this layer and is recorded as such. + +What this module does not establish. It consists only of definitions and structures; +it states nothing as a result and proves nothing: none of the parent results, the +remainder bound or the planar bounds is shown here, and no kernel receipt about them +exists. It does not transcribe the explicit Gaussian/angular integral (15.2) for the +leading coefficient `c_{d,L}` (the coefficient is characterised only through the +leading-term asymptotics of (1.3)); it does not transcribe the regression law +`Q_{r,b,k,R}`, the typed weight `W_r`, the full normalizer `Z_r` or the marked Kac-Rice +representation (all informal in the source and taken as the interface field `p`); it +does not transcribe the reading-rule amendments bound to the parent (congruence erratum, +Section 9 replacement v1.1, wording W1, embedding radius `r < L/(4 sqrt 2)`), nor the +marked-cylinder cap support; it asserts no numerical `C`, `r_*`, `z_*`, `ell_*` or +coefficient value; it does not state Theorem A as consumed by Theorem R; and it does +not state the compact-window `O(ell^(2/3))` difference for the unrestricted densities. +The planar statements (E4) and (E11) carry the parent upper bound (1.1), for the same +typed pair law at `d = 2`, as an explicit hypothesis, as the source does ("If the precise +Theorem A upper bound in [LP] is consumed"; its Section 4 says the upper half of (E11) +consumes the parent upper bound already identified there); the direct lower bound (E2) is +unconditional, as in the source. +Nothing here promotes, reclassifies or discharges any claim, premise or obligation of +the registers; the landing disposition `REVIEWED_SCOPED` (lifetime-remainder) and the +graph classification and review disposition recorded for +`math.uniform-matrix-cap-lifetime` are transcribed from the registers by the statement +register, never re-derived here; alignment of these statements with the sources is +PENDING_INDEPENDENT_REVIEW. + +Sources (Layer 0, byte-pinned, `d6g8k5htny-coder/Math-`): +* `lifetime-parent`: commit `c39164254ad1529ed49543743598d5dcb24bab98`, path + `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md`, + sha256 `9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7`. +* `lifetime-remainder`: commit `760340e921ac4ceda296b8118da936f1133e956e`, path + `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md`, + sha256 `380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a`. +* `elder-lower-density-gap`: commit `6c020d6a72936632f2055122e71a7818a4ff497e`, path + `frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md`, + sha256 `8ce05a43bde8e0d718f09e2da1ffe75d3ec5893489254afdbf5b58b602cdba0c`. +-/ + +namespace UniversalLaw.Spec.Lifetime + +open MeasureTheory + +/-! ### Shared objects, re-declared from `Specifications/Field.lean` (same text, this +namespace). The duplication is deliberate: modules of this packet import only Mathlib. -/ + +/-- The ambient Euclidean space `R^d` in which the torus `X = R^d/(L Z^d)` is realised +by `L`-periodic functions. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "On the flat torus X = R^d/(L Z^d), let f be the centered stationary Gaussian field of variance one with covariance" +Interface: none; this is the ambient space `EuclideanSpace ℝ (Fin d)`. +Does not claim: that the torus is represented by any quotient type; periodicity is a hypothesis on functions. -/ +abbrev E (d : ℕ) : Type := EuclideanSpace ℝ (Fin d) + +/-- The lattice vector `L n` for `n ∈ Z^d`, written in the standard coordinate vectors. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "K_L(z) = sum_{n in Z^d} exp(-|z+Ln|^2/2)" +Interface: none. +Does not claim: anything beyond the definition of the vector `L n`. -/ +noncomputable def latticeVec (d : ℕ) (L : ℝ) (n : Fin d → ℤ) : E d := + ∑ i, EuclideanSpace.single i (L * (n i : ℝ)) + +/-- The unnormalised periodized Gaussian (theta) sum `sum_{n in Z^d} exp(-|z+Ln|^2/2)`, +written as a `tsum` over `Z^d`. If the family were not summable the `tsum` would be `0`; +summability is a hypothesis field of `GaussianFieldInterface`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "K_L(z) = sum_{n in Z^d} exp(-|z+Ln|^2/2)" +Interface: summability of the family is the field `GaussianFieldInterface.summable`, not derived here. +Does not claim: convergence of the sum. -/ +noncomputable def thetaSum (d : ℕ) (L : ℝ) (z : E d) : ℝ := + ∑' n : Fin d → ℤ, Real.exp (-(‖z + latticeVec d L n‖ ^ 2) / 2) + +/-- The periodized Gaussian covariance +`K_L(z) = sum_n exp(-|z+Ln|^2/2) / sum_n exp(-|Ln|^2/2)`; the denominator is the theta +sum at `z = 0`, so `K_L(0) = 1` (variance one) whenever that denominator is nonzero (the +summability field is meant to provide this; not shown here). + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "K_L(z) = sum_{n in Z^d} exp(-|z+Ln|^2/2)" +Interface: summability of both theta sums is the field `GaussianFieldInterface.summable`. +Does not claim: positivity of the Fourier coefficients (Section 2 of the source) or any property of `K_L` beyond its definition. -/ +noncomputable def periodicCovariance (d : ℕ) (L : ℝ) (z : E d) : ℝ := + thetaSum d L z / thetaSum d L 0 + +/-- The `K_L`-quadratic form `sum_{i,j} a_i a_j K_L(x_i - x_j)` of a finite real linear +combination `sum_i a_i f(x_i)` of point evaluations: its variance under a centred +stationary field with covariance `K_L`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "let f be the centered stationary Gaussian field of variance one with covariance" +Interface: nonnegativity of this form is the field `GaussianFieldInterface.quad_nonneg`. +Does not claim: positive definiteness (Section 2 of the source). -/ +noncomputable def covQuadForm (d : ℕ) (L : ℝ) {m : ℕ} (x : Fin m → E d) (a : Fin m → ℝ) : ℝ := + ∑ i, ∑ j, a i * a j * periodicCovariance d L (x i - x j) + +/-- `L`-periodicity of a function on `R^d`: invariance under every lattice translation. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "On the flat torus X = R^d/(L Z^d), let f be the centered stationary Gaussian field of variance one with covariance" +Interface: none; this is the defining predicate of a function on the torus. +Does not claim: anything about the field. -/ +def IsLPeriodic (d : ℕ) (L : ℝ) (g : E d → ℝ) : Prop := + ∀ (x : E d) (n : Fin d → ℤ), g (x + latticeVec d L n) = g x + +/-- Smoothness of a sample path: `C^n` for every finite `n` (written without `⊤`). + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "In particular the field has a smooth version and all finite moments of its global derivative suprema exist." +Interface: smoothness of every sample path is the field `GaussianFieldInterface.smooth`. +Does not claim: existence of a smooth version, or moment bounds on derivative suprema. -/ +def IsSmooth (d : ℕ) (g : E d → ℝ) : Prop := + ∀ n : ℕ, ContDiff ℝ n g + +/-- Interface for the centred stationary Gaussian field of variance one on the torus +`R^d/(L Z^d)` with covariance `K_L`. The field is GIVEN: its probability space, its sample +paths, their smoothness and periodicity, the Gaussian law of every finite real linear +combination of point evaluations (law `gaussianReal 0 v` with `v` the `K_L`-quadratic +form) and the covariance identity are hypothesis fields, as is summability of the theta +sums. Existence of such an object is not asserted. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "On the flat torus X = R^d/(L Z^d), let f be the centered stationary Gaussian field of variance one with covariance" +Interface: every field of this structure is a given property of the field, never derived. +Does not claim: existence or uniqueness in law of the field; the Fourier representation and positive spectrum of Section 2; almost-sure Morse genericity of Section 8. -/ +structure GaussianFieldInterface (d : ℕ) (L : ℝ) where + /-- The underlying probability space (sample space). -/ + Ω : Type + -- Its sigma-algebra (square-bracket field, as in Mathlib's bundled categories). It is not + -- registered for typeclass resolution after this declaration; consumers bring it into + -- scope with `haveI := G.mΩ`. + [mΩ : MeasurableSpace Ω] + /-- The probability measure `P`. -/ + P : Measure Ω + -- `P` is a probability measure (square-bracket field). + [isProb : IsProbabilityMeasure P] + /-- The sample paths `ω ↦ f_ω : R^d → ℝ`. -/ + F : Ω → E d → ℝ + /-- Section 2 clause: "the field has a smooth version"; every sample path is smooth. -/ + smooth : ∀ ω, IsSmooth d (F ω) + /-- Section 1 clause: the field lives "On the flat torus X = R^d/(L Z^d)"; every sample path + is `L`-periodic. -/ + periodic : ∀ ω, IsLPeriodic d L (F ω) + /-- Section 1 clause: the theta sums defining `K_L` converge (taken as a hypothesis). -/ + summable : ∀ z : E d, Summable (fun n : Fin d → ℤ => Real.exp (-(‖z + latticeVec d L n‖ ^ 2) / 2)) + /-- The `K_L`-quadratic form is nonnegative (so it is a variance). -/ + quad_nonneg : ∀ {m : ℕ} (x : Fin m → E d) (a : Fin m → ℝ), 0 ≤ covQuadForm d L x a + /-- Section 1 clause: "the centered stationary Gaussian field of variance one with covariance" + `K_L`; every finite real linear combination of point evaluations has the centred Gaussian + law whose variance is the `K_L`-quadratic form. -/ + gaussian : ∀ {m : ℕ} (x : Fin m → E d) (a : Fin m → ℝ), + Measure.map (fun ω => ∑ i, a i * F ω (x i)) P = + ProbabilityTheory.gaussianReal 0 ⟨covQuadForm d L x a, quad_nonneg x a⟩ + /-- Covariance identity `E[f(x) f(y)] = K_L(x - y)` (centred, stationary). -/ + covariance : ∀ x y : E d, ∫ ω, F ω x * F ω y ∂P = periodicCovariance d L (x - y) + +/-- The Hessian of `g` at `x` as a bilinear form, through the second iterated Fréchet +derivative: `hessian d g x v w = D^2 g(x)[v, w]`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "A maximum has d negative Hessian eigenvalues; the relevant saddle has d-1 negative and one positive eigenvalue." +Interface: none. +Does not claim: symmetry of the form (true for `C^2` functions, not stated here). -/ +noncomputable def hessian (d : ℕ) (g : E d → ℝ) (x v w : E d) : ℝ := + iteratedFDeriv ℝ 2 g x ![v, w] + +/-- Critical point: vanishing Fréchet derivative (`grad f = 0`). + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "grad f(M)=grad f(S)=0." +Interface: none. +Does not claim: differentiability of `g` at `x` (if `g` is not differentiable, `fderiv` is `0`). -/ +def IsCriticalPoint (d : ℕ) (g : E d → ℝ) (x : E d) : Prop := + fderiv ℝ g x = 0 + +/-- Sylvester-inertia encoding of "the Hessian at `x` is nondegenerate with exactly `j` +negative and `d - j` positive eigenvalues": there are complementary subspaces `V`, `W` of +dimensions `j` and `d - j` on which the Hessian form is negative definite, respectively +positive definite. Intended to agree with the eigenvalue count for symmetric (`C^2`) +Hessians; not shown here. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "The index counts negative eigenvalues." +Interface: none. +Does not claim: equivalence with an eigenvalue count for a non-symmetric form. -/ +def HessianHasInertia (d : ℕ) (g : E d → ℝ) (x : E d) (j : ℕ) : Prop := + ∃ V W : Submodule ℝ (E d), IsCompl V W ∧ + Module.finrank ℝ V = j ∧ Module.finrank ℝ W = d - j ∧ + (∀ v ∈ V, v ≠ 0 → hessian d g x v v < 0) ∧ + (∀ w ∈ W, w ≠ 0 → 0 < hessian d g x w w) + +/-- Nondegenerate local maximum: a critical point whose Hessian has `d` negative +eigenvalues (negative definite). + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "A maximum has d negative Hessian eigenvalues; the relevant saddle has d-1 negative and one positive eigenvalue." +Interface: none. +Does not claim: that every local maximum of a sample path is nondegenerate (Morse genericity is Section 8 of the source). -/ +def IsNondegMax (d : ℕ) (g : E d → ℝ) (x : E d) : Prop := + IsCriticalPoint d g x ∧ HessianHasInertia d g x d + +/-- Index-(d-1) saddle: a critical point whose Hessian has `d - 1` negative and one +positive eigenvalue. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "A maximum has d negative Hessian eigenvalues; the relevant saddle has d-1 negative and one positive eigenvalue." +Interface: none. +Does not claim: that such a saddle is a merging saddle of any superlevel bar. -/ +def IsIndexSaddle (d : ℕ) (g : E d → ℝ) (x : E d) : Prop := + IsCriticalPoint d g x ∧ HessianHasInertia d g x (d - 1) + +/-- The pin `M = -(r/2) u` of the embedded local cylinder with axial unit vector `u`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "M=-(r/2)u, S=(r/2)u," +Interface: none. +Does not claim: that `u` is a unit vector; this pin is an auxiliary definition consumed by no statement of this packet (the typed pair law `p` is a primitive), so it is attached to no claim. -/ +noncomputable def pinM (d : ℕ) (r : ℝ) (u : E d) : E d := + -((r / 2) • u) + +/-- The pin `S = (r/2) u` of the embedded local cylinder with axial unit vector `u`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "M=-(r/2)u, S=(r/2)u," +Interface: none. +Does not claim: that `u` is a unit vector; this pin is an auxiliary definition consumed by no statement of this packet (the typed pair law `p` is a primitive), so it is attached to no claim. -/ +noncomputable def pinS (d : ℕ) (r : ℝ) (u : E d) : E d := + (r / 2) • u + +/-- Torus distance between two points of `R^d`: the infimum over the lattice of +`|x - y + L n|`. For `L > 0` it is intended to vanish exactly when `x` and `y` represent the +same torus point; not shown here. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "Count ordered maximum/saddle pairs with 00, and let nu_eld^all(ell) count all finite ordinary superlevel H0 persistence bars, both in expectation per unit volume." +Interface: none. +Does not claim: that the height gap of an elder pair is the persistence of a bar in any persistence module. -/ +def heightGap (d : ℕ) (g : E d → ℝ) (M S : E d) : ℝ := + g M - g S + +/-- Scaled gap `(f(M) - f(S)) / distance^3` of an ordered pair, with the torus distance. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "Count ordered maximum/saddle pairs with 00, and let nu_eld^all(ell) count all finite ordinary superlevel H0 persistence bars, both in expectation per unit volume." +Interface: none. +Does not claim: positivity of the height gap (added separately where the source requires it). -/ +def IsCandidatePair (d : ℕ) (L : ℝ) (g : E d → ℝ) (M S : E d) : Prop := + IsNondegMax d g M ∧ IsIndexSaddle d g S ∧ 0 < torusDist d L M S + +/-- Morse genericity with distinct critical values on the torus: every critical point is +nondegenerate (has some inertia) and critical points at distinct torus positions have +distinct critical values. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "Countable exhaustion now proves that Q is almost surely Morse with distinct critical values." +Interface: none; used only as a hypothesis of the elder-partner interface clause. +Does not claim: that sample paths are almost surely Morse (Section 8 of the source). -/ +def IsMorseDistinct (d : ℕ) (L : ℝ) (g : E d → ℝ) : Prop := + (∀ x : E d, IsCriticalPoint d g x → ∃ j : ℕ, HessianHasInertia d g x j) ∧ + (∀ x y : E d, IsCriticalPoint d g x → IsCriticalPoint d g y → + 0 < torusDist d L x y → g x ≠ g y) + +/-- Interface for the superlevel-set H0 persistence objects used by the lifetime track: +the maximin death height `d_f(M)`, the essential (global-maximum) class, and the ordinary +elder death partner relation. These are GIVEN relations; the fields transcribe the source +clauses that characterise them on smooth periodic functions, and the elder relation is +pinned only on the Morse distinct-value locus, exactly as the source does. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "On the Morse distinct-value locus it expresses ordinary elder death at S; an essential maximum has no older endpoint." +Interface: `deathHeight`, `IsEssential`, `ElderPartner` are given; `deathHeight_maximin`, `essential_iff`, `elderPartner_iff` are their hypothesis clauses. +Does not claim: Borel measurability of the elder event (Section 8 / the Section 9 replacement), identification with a persistence-module elder rule, or any behaviour off the Morse distinct-value locus. -/ +structure SuperlevelBarInterface (d : ℕ) (L : ℝ) where + /-- Section 8 clause: the maximin connection level + `d_f(M)=sup_{gamma(0)=M, f(gamma(1))>f(M)} min_t f(gamma(t))`. -/ + deathHeight : (E d → ℝ) → E d → ℝ + /-- The essential class: the global maximum, which "has no older endpoint" and whose + superlevel H0 bar is not finite. -/ + IsEssential : (E d → ℝ) → E d → Prop + /-- Section 1 clause: "the global ordinary superlevel elder death partner of M is S". -/ + ElderPartner : (E d → ℝ) → E d → E d → Prop + /-- `M` is essential exactly when no point is strictly higher (so the supremum in the + maximin is over an empty set, "equal to -infinity"). -/ + essential_iff : ∀ (g : E d → ℝ), IsSmooth d g → IsLPeriodic d L g → + ∀ M : E d, IsEssential g M ↔ ∀ y : E d, g y ≤ g M + /-- Section 8 maximin clause, in the form `h < d_f(M)` iff some path from `M` to a strictly + higher point stays strictly above `h`. -/ + deathHeight_maximin : ∀ (g : E d → ℝ), IsSmooth d g → IsLPeriodic d L g → + ∀ M : E d, ¬ IsEssential g M → ∀ h : ℝ, + h < deathHeight g M ↔ + ∃ y : E d, g M < g y ∧ ∃ γ : Path M y, ∀ t : unitInterval, h < g (γ t) + /-- Section 8 / Section 14 clause: on the Morse distinct-value locus, "equality + d_f(M)=f(S)" with `M` a nondegenerate maximum and `S` an index-(d-1) saddle "expresses + ordinary elder death at S". -/ + elderPartner_iff : ∀ (g : E d → ℝ), IsSmooth d g → IsLPeriodic d L g → IsMorseDistinct d L g → + ∀ M S : E d, ElderPartner g M S ↔ + (IsNondegMax d g M ∧ IsIndexSaddle d g S ∧ ¬ IsEssential g M ∧ deathHeight g M = g S) + +/-- Finite ordinary superlevel H0 bar, as an ordered pair: a nondegenerate maximum `M` +(birth) with its ordinary elder death partner `S`, an index-(d-1) saddle at positive torus +distance. The essential global-maximum class is excluded because `ElderPartner` requires +`¬ IsEssential` on the Morse locus. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "each finite superlevel H0 bar has exactly one local-maximum birth and one index-(d-1) merging-saddle death." +Interface: `I : SuperlevelBarInterface d L` is given. +Does not claim: the identification of these pairs with bars of a persistence module; that the count of such pairs equals the finite-bar count off the Morse locus. -/ +def IsFiniteBar (d : ℕ) (L : ℝ) (I : SuperlevelBarInterface d L) (g : E d → ℝ) (M S : E d) : Prop := + IsCandidatePair d L g M S ∧ 0 < heightGap d g M S ∧ I.ElderPartner g M S + +/-- The set of pairs of a population `Pair` with both points in the fundamental domain and +lifetime (height gap) in `A`; `Pair g M S` is the membership predicate of the population. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "Let nu_cand(ell) be their expected lifetime density per unit volume; let nu_eld(ell) count only pairs which are actual ordinary elder partners." +Interface: the population predicate `Pair` is a parameter. +Does not claim: finiteness of this set (a field of the density-version predicate). -/ +def pairSet (d : ℕ) (L : ℝ) (Pair : (E d → ℝ) → E d → E d → Prop) (g : E d → ℝ) (A : Set ℝ) : + Set (E d × E d) := + {p | p.1 ∈ FundDomain d L ∧ p.2 ∈ FundDomain d L ∧ Pair g p.1 p.2 ∧ heightGap d g p.1 p.2 ∈ A} + +/-- Number of pairs of the population with lifetime in `A` and base points in the +fundamental domain (`Set.ncard`, which is `0` for an infinite set). + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "Let nu_cand(ell) be their expected lifetime density per unit volume; let nu_eld(ell) count only pairs which are actual ordinary elder partners." +Interface: the population predicate `Pair` is a parameter. +Does not claim: finiteness of the counted set. -/ +noncomputable def pairCount (d : ℕ) (L : ℝ) (Pair : (E d → ℝ) → E d → E d → Prop) + (g : E d → ℝ) (A : Set ℝ) : ℕ := + Set.ncard (pairSet d L Pair g A) + +/-- `ν` is a VERSION of the expected per-unit-volume lifetime density of the population +`Pair` under the field `G`: it is nonnegative and measurable, the pair sets are almost +surely finite with integrable counts, `ν` is integrable on every Borel `A ⊆ (0, ∞)`, and +`∫_A ν = E[#pairs with lifetime in A and base point in [0,L)^d] / L^d` for every such `A`. +The source's densities are only defined up to such versions. The sigma-algebra of the sample +space is brought into scope by the inlined term-level `haveI := G.mΩ` (a square-bracket +field of a bundled record is not registered for typeclass resolution after the declaration). + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "These densities admit versions with" +Interface: the field `G` and the population predicate `Pair` are given; the Kac-Rice representation of the expectation (Sections 9-10 of the source) is NOT used; the density is characterised only by the integral identity. +Does not claim: existence of a version; the weighted Kac-Rice identity; the radial ledger (10.2). Measurability of the pair count as a function of the sample is REQUIRED by the predicate (through `Integrable`, hence `AEStronglyMeasurable`), not established here. -/ +def IsLifetimeDensityVersion (d : ℕ) (L : ℝ) (G : GaussianFieldInterface d L) + (Pair : (E d → ℝ) → E d → E d → Prop) (ν : ℝ → ℝ) : Prop := + haveI := G.mΩ + (∀ ℓ : ℝ, 0 ≤ ν ℓ) ∧ Measurable ν ∧ + (∀ A : Set ℝ, MeasurableSet A → A ⊆ Set.Ioi 0 → + (∀ᵐ ω ∂G.P, (pairSet d L Pair (G.F ω) A).Finite) ∧ + Integrable (fun ω => ((pairCount d L Pair (G.F ω) A : ℕ) : ℝ)) G.P ∧ + IntegrableOn ν A ∧ + ∫ ℓ in A, ν ℓ = (∫ ω, ((pairCount d L Pair (G.F ω) A : ℕ) : ℝ) ∂G.P) / L ^ d) + +/-! ### Populations of pairs -/ + +/-- Compact-window population of Theorem B: ordered maximum / index-(d-1)-saddle pairs with +`0 < distance <= ρ`, birth `f(M)` in `B = [bLo, bHi]` and scaled gap in `K = [kLo, kHi]`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "Count ordered maximum/saddle pairs with 00, and let nu_eld^all(ell) count all finite ordinary superlevel H0 persistence bars, both in expectation per unit volume." +Interface: none beyond the shared predicates. +Does not claim: anything about the off-diagonal (far) population separately (Section 14 of the source). -/ +def IsUnrestrictedPair (d : ℕ) (L : ℝ) (g : E d → ℝ) (M S : E d) : Prop := + IsCandidatePair d L g M S ∧ 0 < heightGap d g M S + +/-! ### The typed pair law as an interface -/ + +/-- Interface for the weighted regression (typed pair) law: the only object consumed by the +statements is the probability `p_r(b,k,R)` that the global ordinary superlevel elder death +partner of the pinned maximum `M = -(r/2)u` is the pinned saddle `S = (r/2)u`, under the +law `Q^W = (W_r/Z_r) Q_{r,b,k,R}` with `W_r = |det H_M det H_S| 1{H_M<0, index(H_S)=d-1}`. +That law, its weight, its normalizer and the regression construction are informal in the +source and are NOT transcribed; `p` is a GIVEN function of radius `r`, birth `b`, gap mark +`k` and orthonormal frame `R` with values in `[0, 1]`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "Let p_r(b,k,R) be the Q^W probability that the **global ordinary superlevel elder death partner** of M is S." +Interface: `p` is given; its only hypothesis fields are the bounds `0 ≤ p ≤ 1`. The parameters `G` and `I` record which field and which elder relation the law refers to; no field ties `p` to them. +Does not claim: existence of the regression law, the typed weight, the full normalizer `Z_r > 0`, or that `p` is the probability of any event under any measure declared here; that `p` depends on `G` or `I` in any way (no field mentions them; they only record which field and elder relation the law is meant to refer to). -/ +structure PairLawInterface (d : ℕ) (L : ℝ) (G : GaussianFieldInterface d L) + (I : SuperlevelBarInterface d L) where + /-- Section 1 clause: "Let p_r(b,k,R) be the Q^W probability that the global ordinary + superlevel elder death partner of M is S." -/ + p : ℝ → ℝ → ℝ → OrthonormalBasis (Fin d) ℝ (E d) → ℝ + /-- `p` is a probability: nonnegative. -/ + p_nonneg : ∀ (r b k : ℝ) (R : OrthonormalBasis (Fin d) ℝ (E d)), 0 ≤ p r b k R + /-- `p` is a probability: at most one. -/ + p_le_one : ∀ (r b k : ℝ) (R : OrthonormalBasis (Fin d) ℝ (E d)), p r b k R ≤ 1 + +/-! ### The parent statements (1.1), (1.2), (1.3) -/ + +/-- Shape of Theorem A (1.1), uniform selection candidate: for fixed `d ≥ 2`, `L > 0`, +compact `B = [bLo, bHi]` and `K = [kLo, kHi]` with `0 < kLo ≤ kHi`, there exist `r_* > 0` +and `C` (quantified OUTSIDE the universal quantifiers over `r`, `b`, `k` and the frame) +such that `0 <= 1 - p_r(b,k,R) <= C r^3` for all `0 < r ≤ r_*`, `b ∈ B`, `k ∈ K` and all +orthonormal frames `R`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "There exist r_*>0 and C 0` and +windows `B`, `K` of positive length with `kLo > 0`, there are a distance cutoff `r_* > 0`, a +constant `c_{B,K} > 0` and a constant `C_{B,K}` such that the compact-window candidate and +elder lifetime densities admit versions `νc`, `νe` with `νc(ℓ) ~ c_{B,K} ℓ^(-1/3)`, +`νe(ℓ) ~ c_{B,K} ℓ^(-1/3)` as `ℓ ↓ 0` (filter `nhdsWithin 0 (Set.Ioi 0)`) and +`0 ≤ νc(ℓ) - νe(ℓ) ≤ C_{B,K} ℓ^(2/3)` for all sufficiently small `ℓ > 0`. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "0 <= nu_cand(ell)-nu_eld(ell) <= C_{B,K} ell^(2/3)," +Interface: `G` and `I` are given; "versions" are any `νc`, `νe` satisfying `IsLifetimeDensityVersion` (integral identity), not a Kac-Rice representation; the coefficient `c_{B,K}` is existential, not the Gaussian integral (11.3). +Does not claim: the parent result or its proof; the exact coefficient formula (11.3); existence of the versions; that the cutoff `r_*` is the one of (1.1); any numerical constant; nonauthor review or acceptance. -/ +def ParentCompactWindowDensityB (d : ℕ) (L : ℝ) (G : GaussianFieldInterface d L) + (I : SuperlevelBarInterface d L) (bLo bHi kLo kHi : ℝ) : Prop := + 2 ≤ d → 0 < L → bLo < bHi → 0 < kLo → kLo < kHi → + ∃ rStar : ℝ, 0 < rStar ∧ ∃ c : ℝ, 0 < c ∧ ∃ C : ℝ, ∃ νc νe : ℝ → ℝ, + IsLifetimeDensityVersion d L G (IsWindowPair d L rStar bLo bHi kLo kHi) νc ∧ + IsLifetimeDensityVersion d L G (IsWindowElderPair d L rStar bLo bHi kLo kHi I) νe ∧ + Asymptotics.IsEquivalent (nhdsWithin (0 : ℝ) (Set.Ioi 0)) νc + (fun ℓ : ℝ => c * ℓ ^ ((-1 : ℝ) / 3)) ∧ + Asymptotics.IsEquivalent (nhdsWithin (0 : ℝ) (Set.Ioi 0)) νe + (fun ℓ : ℝ => c * ℓ ^ ((-1 : ℝ) / 3)) ∧ + ∃ ℓStar : ℝ, 0 < ℓStar ∧ ∀ ℓ : ℝ, 0 < ℓ → ℓ ≤ ℓStar → + 0 ≤ νc ℓ - νe ℓ ∧ νc ℓ - νe ℓ ≤ C * ℓ ^ ((2 : ℝ) / 3) + +/-- `c` is a leading coefficient of the unrestricted finite-lifetime densities: `c > 0` and +versions `νc`, `νe` of the unrestricted candidate density and of the finite ordinary +superlevel H0 bar density satisfy `νc(ℓ) ~ c ℓ^(-1/3)` and `νe(ℓ) ~ c ℓ^(-1/3)` as `ℓ ↓ 0`. +The essential global-maximum class is excluded from `νe` through `IsFiniteBar`. This is the +conclusion of (1.3) for a given `c`; it characterises `c_{d,L}` by its leading-term role, +not by the integral (13.6)/(15.2). + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "There is a positive finite constant c_{d,L} such that" +Interface: `G` and `I` are given; versions are characterised by the integral identity only. +Does not claim: the explicit Gaussian/angular representation (15.2) of `c_{d,L}`; uniqueness of `c` (which follows from the asymptotics but is not stated); existence of versions. -/ +def IsUnrestrictedLeadingCoefficient (d : ℕ) (L : ℝ) (G : GaussianFieldInterface d L) + (I : SuperlevelBarInterface d L) (c : ℝ) : Prop := + 0 < c ∧ ∃ νc νe : ℝ → ℝ, + IsLifetimeDensityVersion d L G (IsUnrestrictedPair d L) νc ∧ + IsLifetimeDensityVersion d L G (IsFiniteBar d L I) νe ∧ + Asymptotics.IsEquivalent (nhdsWithin (0 : ℝ) (Set.Ioi 0)) νc + (fun ℓ : ℝ => c * ℓ ^ ((-1 : ℝ) / 3)) ∧ + Asymptotics.IsEquivalent (nhdsWithin (0 : ℝ) (Set.Ioi 0)) νe + (fun ℓ : ℝ => c * ℓ ^ ((-1 : ℝ) / 3)) + +/-- Shape of Theorem C (1.3), unrestricted finite-lifetime leading density candidate: for +fixed `d ≥ 2` and `L > 0` there is a positive finite constant `c_{d,L}` such that the +unrestricted candidate density and the finite ordinary superlevel H0 bar density (all birth +heights, all positive gap marks, all separations; essential global maximum excluded) admit +versions with `ν(ℓ) ~ c_{d,L} ℓ^(-1/3)` as `ℓ ↓ 0`. Leading term only. + +Source: d6g8k5htny-coder/Math- commit c39164254ad1529ed49543743598d5dcb24bab98 path imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md sha256 9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7 +Anchor: "nu_cand^all(ell) ~ c_{d,L} ell^(-1/3)," +Interface: `G` and `I` are given; versions are characterised by the integral identity only. +Does not claim: the parent result or its proof (dominated convergence of Section 13, off-diagonal bound (14.1)); the representation (15.2); the compact-window `O(ell^(2/3))` difference for the unrestricted densities; any numerical enclosure of `c_{d,L}` (the SIDE24 coefficient track is separate); nonauthor review or acceptance. -/ +def ParentUnrestrictedLeadingDensityC (d : ℕ) (L : ℝ) (G : GaussianFieldInterface d L) + (I : SuperlevelBarInterface d L) : Prop := + 2 ≤ d → 0 < L → ∃ c : ℝ, IsUnrestrictedLeadingCoefficient d L G I c + +/-! ### The bounded remainder (R1) -/ + +/-- Shape of Theorem R (R1), bounded unrestricted short-lifetime remainder: for fixed +`d ≥ 2`, `L > 0` and with `c = c_{d,L}` the parent leading coefficient (characterised here +by `IsUnrestrictedLeadingCoefficient`), there are `ell_* > 0` and `C` such that versions of +the unrestricted candidate and finite-bar densities satisfy, for `0 < ℓ ≤ ell_*`, +`|νc(ℓ) - c ℓ^(-1/3)| ≤ C`, `0 ≤ νc(ℓ) - νe(ℓ) ≤ C` and `|νe(ℓ) - c ℓ^(-1/3)| ≤ C`. +The `O(1)` remainder is stated with an explicit absolute-value bound. + +Source: d6g8k5htny-coder/Math- commit 760340e921ac4ceda296b8118da936f1133e956e path frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md sha256 380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a +Anchor: "|nu_cand(ell)-c ell^(-1/3)| <= C," +Interface: `G` and `I` are given; `c` is any real satisfying the parent leading-coefficient property (the source says the coefficient "is exactly the parent's equation (15.2)"; that integral is not transcribed, so `c` is pinned through (1.3) instead); versions are characterised by the integral identity only. The statement does not mention the typed pair law: Theorem R does not consume (1.1). +Does not claim: the result or its proof (quadratic determinant cancellation (R7), coupling (R4), cap-loss bound (R12)); convergence of the remainder; a second coefficient; numerical `C` or `ell_*`; the compact-window `O(ell^(2/3))` difference without cutoffs; the parent interfaces it imports (D1-A-E); nonauthor review or acceptance. If no `c` satisfies the parent property the statement holds vacuously; that is a transcription of its dependency on (1.3), not a claim. -/ +def RemainderBoundedR1 (d : ℕ) (L : ℝ) (G : GaussianFieldInterface d L) + (I : SuperlevelBarInterface d L) : Prop := + 2 ≤ d → 0 < L → ∀ c : ℝ, IsUnrestrictedLeadingCoefficient d L G I c → + ∃ ℓStar : ℝ, 0 < ℓStar ∧ ∃ C : ℝ, ∃ νc νe : ℝ → ℝ, + IsLifetimeDensityVersion d L G (IsUnrestrictedPair d L) νc ∧ + IsLifetimeDensityVersion d L G (IsFiniteBar d L I) νe ∧ + ∀ ℓ : ℝ, 0 < ℓ → ℓ ≤ ℓStar → + |νc ℓ - c * ℓ ^ ((-1 : ℝ) / 3)| ≤ C ∧ + 0 ≤ νc ℓ - νe ℓ ∧ νc ℓ - νe ℓ ≤ C ∧ + |νe ℓ - c * ℓ ^ ((-1 : ℝ) / 3)| ≤ C + +/-! ### Planar elder lower bound and density gap (d = 2) -/ + +/-- Shape of the planar direct lower bound (E2): on the fixed planar torus (`d = 2`), with +birth `b` in a fixed compact interval, `k ∈ [kLo, kHi]` with `kLo > 0` and frames ranging +over `O(2)`, there are `c > 0` and `r_* > 0` such that `1 - p_r(b,k,R) ≥ c r^3` for all +`0 < r ≤ r_*`, uniformly in `b`, `k` and the frame. + +Source: d6g8k5htny-coder/Math- commit 6c020d6a72936632f2055122e71a7818a4ff497e path frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md sha256 8ce05a43bde8e0d718f09e2da1ffe75d3ec5893489254afdbf5b58b602cdba0c +Anchor: "1-p_r(b,k,R) >= c r^3, 0 0` there are a distance cutoff +`r_* > 0`, constants `c_{B,K} > 0`, `C_{B,K}` and `ell_* > 0` such that versions of the +compact-window candidate and ordinary elder densities satisfy +`c_{B,K} ℓ^(2/3) ≤ νc(ℓ) - νe(ℓ) ≤ C_{B,K} ℓ^(2/3)` for all `0 < ℓ ≤ ell_*`. The parent upper +input is an explicit hypothesis, not folded into the conclusion. The lower half, which the +source derives from (E2) alone, is stated under the same hypothesis because the source displays +(E11) as one two-sided inequality; that is a hypothesis the source does not need for the lower +half, recorded here as such. + +Source: d6g8k5htny-coder/Math- commit 6c020d6a72936632f2055122e71a7818a4ff497e path frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md sha256 8ce05a43bde8e0d718f09e2da1ffe75d3ec5893489254afdbf5b58b602cdba0c +Anchor: " <= C_{B,K} ell^(2/3). (E11)" +Interface: `G`, `I` and `PL` are given; the hypothesis `ParentUniformSelectionA 2 L G I PL bLo bHi kLo kHi` is the consumed parent upper input (a statement shape, not the parent result); versions are characterised by the integral identity only; the weighted Kac-Rice / radial ledger of [LP, Sections 9-11] that the source consumes is not transcribed. The interface does not determine `p` or the field: the Prop is a predicate on the interface objects, not a closed statement about the source's objects; nothing is asserted about its universal closure over all inhabitants, and `specified` refers to the statement shape at the source's object, which is not constructed. +Does not claim: the result or its proof; the upper half independently of the parent (1.1); the parent (1.1) itself; the lower half without the hypothesis (the source has it from (E2) alone); sharpness of the `O(1)` remainder of (R1); removal of the compact-mark restriction; that the cutoff `r_*` is the one of (1.1); any numerical constant; nonauthor review or acceptance. -/ +def PlanarDensityGapE11 (L : ℝ) (G : GaussianFieldInterface 2 L) (I : SuperlevelBarInterface 2 L) + (PL : PairLawInterface 2 L G I) (bLo bHi kLo kHi : ℝ) : Prop := + ParentUniformSelectionA 2 L G I PL bLo bHi kLo kHi → + (0 < L → bLo < bHi → 0 < kLo → kLo < kHi → + ∃ rStar : ℝ, 0 < rStar ∧ ∃ c : ℝ, 0 < c ∧ ∃ C : ℝ, ∃ ℓStar : ℝ, 0 < ℓStar ∧ + ∃ νc νe : ℝ → ℝ, + IsLifetimeDensityVersion 2 L G (IsWindowPair 2 L rStar bLo bHi kLo kHi) νc ∧ + IsLifetimeDensityVersion 2 L G (IsWindowElderPair 2 L rStar bLo bHi kLo kHi I) νe ∧ + ∀ ℓ : ℝ, 0 < ℓ → ℓ ≤ ℓStar → + c * ℓ ^ ((2 : ℝ) / 3) ≤ νc ℓ - νe ℓ ∧ νc ℓ - νe ℓ ≤ C * ℓ ^ ((2 : ℝ) / 3)) + +end UniversalLaw.Spec.Lifetime diff --git a/frontiers/regular_superlevel_geometry_20261020/project/RegularPointChart.lean b/frontiers/regular_superlevel_geometry_20261020/project/RegularPointChart.lean new file mode 100644 index 000000000..77a75a461 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/project/RegularPointChart.lean @@ -0,0 +1,64 @@ +import Lifetime + +/-! +# Regular scalar chart at a noncritical point + +The construction is the finite-dimensional scalar specialization of Mathlib's +strict implicit-function chart. It uses noncriticality only to prove that the +derivative has full range. +-/ + +namespace UniversalLaw.Spec.Lifetime + +variable {d : ℕ} {g : E d → ℝ} {x : E d} + +/-- At a noncritical point, the scalar derivative has full range. -/ +theorem regularPointDerivative_range_eq_top (hx : ¬ IsCriticalPoint d g x) : + (fderiv ℝ g x).range = ⊤ := by + have hne : (fderiv ℝ g x).toLinearMap ≠ 0 := by + intro hzero + apply hx + unfold IsCriticalPoint + ext y + have hy := LinearMap.congr_fun hzero y + simpa using hy + exact Module.Dual.range_eq_top_of_ne_zero hne + +/-- Smoothness supplies the strict derivative used by the chart. -/ +theorem regularPointHasStrictFDerivAt (hg : IsSmooth d g) : + HasStrictFDerivAt g (fderiv ℝ g x) x := + (hg 1).hasStrictFDerivAt (by norm_num) + +/-- The literal local scalar chart at a noncritical point. -/ +noncomputable def regularPointChart (hg : IsSmooth d g) (hx : ¬ IsCriticalPoint d g x) : + OpenPartialHomeomorph (E d) (ℝ × (fderiv ℝ g x).ker) := + (regularPointHasStrictFDerivAt hg).implicitToOpenPartialHomeomorph + g (fderiv ℝ g x) (regularPointDerivative_range_eq_top hx) + +/-- The chart's first coordinate is exactly `g`, globally as a function equality. -/ +@[simp] +theorem regularPointChart_fst (hg : IsSmooth d g) (hx : ¬ IsCriticalPoint d g x) (y : E d) : + (regularPointChart hg hx y).1 = g y := by + exact HasStrictFDerivAt.implicitToOpenPartialHomeomorph_fst + (regularPointHasStrictFDerivAt hg) (regularPointDerivative_range_eq_top hx) y + +/-- The chart sends the base point to `(g x, 0)`. -/ +@[simp] +theorem regularPointChart_self (hg : IsSmooth d g) (hx : ¬ IsCriticalPoint d g x) : + regularPointChart hg hx x = (g x, 0) := by + exact HasStrictFDerivAt.implicitToOpenPartialHomeomorph_self + (regularPointHasStrictFDerivAt hg) (regularPointDerivative_range_eq_top hx) + +/-- The base point belongs to the chart source. -/ +theorem mem_regularPointChart_source (hg : IsSmooth d g) (hx : ¬ IsCriticalPoint d g x) : + x ∈ (regularPointChart hg hx).source := by + exact HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source + (regularPointHasStrictFDerivAt hg) (regularPointDerivative_range_eq_top hx) + +/-- The image base point belongs to the chart target. -/ +theorem mem_regularPointChart_target (hg : IsSmooth d g) (hx : ¬ IsCriticalPoint d g x) : + (g x, 0) ∈ (regularPointChart hg hx).target := by + exact HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_target + (regularPointHasStrictFDerivAt hg) (regularPointDerivative_range_eq_top hx) + +end UniversalLaw.Spec.Lifetime diff --git a/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevel.lean b/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevel.lean new file mode 100644 index 000000000..03daef580 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevel.lean @@ -0,0 +1,140 @@ +import Lifetime + +/-! +Relative topology for closed scalar superlevels. + +The chart-input theorem below is a reusable topology adapter. It does not construct +a chart from a nonzero derivative: that literal scalar-chart obligation is separately +owned. No critical-point Morse chart or global closed-level LPC is asserted here. +-/ + +open Set Filter Topology +open UniversalLaw.Spec.Lifetime + +namespace TorusRegularSuperlevel + +/-- An open embedding carries a path-connected neighborhood basis to its image point. -/ +theorem path_connected_basis_of_openEmbedding + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + [LocallyPathConnectedSpace X] {e : X → Y} + (he : IsOpenEmbedding e) (x : X) : + (𝓝 (e x)).HasBasis + (fun V : Set Y => V ∈ 𝓝 (e x) ∧ IsPathConnected V) id := by + rw [hasBasis_self] + intro U hU + have hpre : e ⁻¹' U ∈ 𝓝 x := + he.continuous.continuousAt.preimage_mem_nhds hU + obtain ⟨V, ⟨hV, hpath⟩, hVU⟩ := (path_connected_basis x).mem_iff.mp hpre + refine ⟨e '' V, he.image_mem_nhds.mpr hV, hpath.image he.continuous, ?_⟩ + exact image_subset_iff.mpr hVU + +/-- An LPC open neighborhood supplies the required basis in the ambient space. -/ +theorem path_connected_basis_of_open + {X : Type*} [TopologicalSpace X] {U : Set X} + (hU : IsOpen U) [LocallyPathConnectedSpace U] {x : X} (hx : x ∈ U) : + (𝓝 x).HasBasis (fun V : Set X => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + exact path_connected_basis_of_openEmbedding hU.isOpenEmbedding_subtypeVal ⟨x, hx⟩ + +/-- Restrict a chart to two corresponding subsets, using their relative open +source and target. Neither subset is required to be open in its original ambient space. -/ +def relative_chart_homeomorph + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + (p : OpenPartialHomeomorph X Y) (S : Set X) (T : Set Y) + (hmem : ∀ y ∈ p.source, y ∈ S ↔ p y ∈ T) : + {y : S // y.val ∈ p.source} ≃ₜ {z : T // z.val ∈ p.target} where + toFun y := ⟨⟨p y.val.val, (hmem y.val.val y.property).mp y.val.property⟩, + p.map_source y.property⟩ + invFun z := ⟨⟨p.symm z.val.val, + (hmem (p.symm z.val.val) (p.map_target z.property)).mpr + (by rw [p.right_inv z.property]; exact z.val.property)⟩, + p.map_target z.property⟩ + left_inv y := by + apply Subtype.ext + apply Subtype.ext + exact p.left_inv y.property + right_inv z := by + apply Subtype.ext + apply Subtype.ext + exact p.right_inv z.property + continuous_toFun := by + apply Continuous.subtype_mk + apply Continuous.subtype_mk + exact p.continuousOn.comp_continuous + (continuous_subtype_val.comp continuous_subtype_val) (fun y => y.property) + continuous_invFun := by + apply Continuous.subtype_mk + apply Continuous.subtype_mk + exact p.continuousOn_symm.comp_continuous + (continuous_subtype_val.comp continuous_subtype_val) (fun z => z.property) + +/-- Relative chart transport derives a neighborhood basis in the source subset +from LPC of the model subset. This helper is consumed with a proved convex halfspace. -/ +theorem path_connected_basis_of_relative_chart + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + (p : OpenPartialHomeomorph X Y) (S : Set X) (T : Set Y) + [LocallyPathConnectedSpace T] + (hmem : ∀ y ∈ p.source, y ∈ S ↔ p y ∈ T) + (x : S) (hx : x.val ∈ p.source) : + (𝓝 x).HasBasis (fun V : Set S => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let U : Set S := {y | y.val ∈ p.source} + let V : Set T := {z | z.val ∈ p.target} + have hU : IsOpen U := p.open_source.preimage continuous_subtype_val + have hV : IsOpen V := p.open_target.preimage continuous_subtype_val + let : LocallyPathConnectedSpace V := hV.locallyPathConnectedSpace + let h : U ≃ₜ V := relative_chart_homeomorph p S T hmem + let : LocallyPathConnectedSpace U := h.symm.locallyPathConnectedSpace + exact path_connected_basis_of_open hU hx + +/-- A scalar chart supplies the actual closed-superlevel neighborhood basis. + +The coordinate identity is needed only on the chart source. This theorem proves +the relative-topology step; the separately owned literal regular-point constructor +must supply `p`, `hx`, and `hcoord` before a noncritical-point corollary is claimed. -/ +theorem closed_superlevel_basis_of_chart + {d : ℕ} {g : E d → ℝ} {F : Type*} + [NormedAddCommGroup F] [NormedSpace ℝ F] + (a : ℝ) (x : {y : E d // a ≤ g y}) + (p : OpenPartialHomeomorph (E d) (ℝ × F)) + (hx : x.val ∈ p.source) + (hcoord : ∀ y ∈ p.source, (p y).fst = g y) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let H : Set (ℝ × F) := {z | a ≤ z.fst} + have hconvex : Convex ℝ H := by + intro u hu v hv s t hs ht hst + change a ≤ s • u.fst + t • v.fst + calc + a = s • a + t • a := (Convex.combo_self hst a).symm + _ ≤ s • u.fst + t • v.fst := + add_le_add (smul_le_smul_of_nonneg_left hu hs) + (smul_le_smul_of_nonneg_left hv ht) + let : LocallyPathConnectedSpace H := hconvex.locallyPathConnectedSpace + apply path_connected_basis_of_relative_chart p {y | a ≤ g y} H _ x hx + intro y hy + change a ≤ g y ↔ a ≤ (p y).fst + rw [hcoord y hy] + +/-- A point strictly above the level has a path-connected neighborhood basis in +the closed superlevel, with continuity alone and no regularity assumption. -/ +theorem closed_superlevel_interior_basis + {d : ℕ} {g : E d → ℝ} (hg : Continuous g) + (a : ℝ) (x : {y : E d // a ≤ g y}) (hx : a < g x.val) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => V ∈ 𝓝 x ∧ IsPathConnected V) id := by + let S : Set (E d) := {y | a ≤ g y} + let U : Set (E d) := {y | a < g y} + have hU : IsOpen U := isOpen_lt continuous_const hg + let : LocallyPathConnectedSpace U := hU.locallyPathConnectedSpace + let e : U → S := fun y => ⟨y.val, by + change a ≤ g y.val + exact le_of_lt (show a < g y.val from y.property)⟩ + have he : IsOpenEmbedding e := by + have hmaps : MapsTo (id : E d → E d) U S := by + intro y hy + change a ≤ g y + exact le_of_lt (show a < g y from hy) + exact (IsOpenEmbedding.id : IsOpenEmbedding (id : E d → E d)).restrict + (s := U) (t := S) hmaps hU + exact path_connected_basis_of_openEmbedding he ⟨x.val, hx⟩ + +end TorusRegularSuperlevel diff --git a/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevelAxiomAudit.lean b/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevelAxiomAudit.lean new file mode 100644 index 000000000..40e334d0e --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevelAxiomAudit.lean @@ -0,0 +1,62 @@ +import RegularSuperlevelLiteral +import Lean.Elab.Command +import Lean.Util.CollectAxioms + +/-! Complete module-origin census for C297 and its exact Lifetime/peer-chart inputs. +Includes generated and private declarations. Only the standard axioms are allowed. +Command success is scoped execution evidence, not scientific promotion. -/ + +#print axioms TorusRegularSuperlevel.closed_superlevel_regular_basis +#print axioms TorusRegularSuperlevel.closed_superlevel_path_connected_basis +#print axioms TorusRegularSuperlevel.closed_superlevel_interior_basis +#check @TorusRegularSuperlevel.closed_superlevel_regular_basis +#check @TorusRegularSuperlevel.closed_superlevel_path_connected_basis +#check @TorusRegularSuperlevel.closed_superlevel_interior_basis + +open Lean Elab Command in +run_cmd do + let env := (← getEnv).setExporting false + let allowed : Array Name := #[`propext, `Classical.choice, `Quot.sound] + let modules : Array Name := #[`Lifetime, `RegularPointChart, + `RegularSuperlevel, `RegularSuperlevelLiteral] + let constants := env.constants.toList + let mut allNames : Array Name := #[] + for modName in modules do + let some idx := env.getModuleIdx? modName + | throwError "missing audited module: {modName}" + let names := (constants.filterMap fun (name, _) => + if env.getModuleIdxFor? name == some idx then some name else none).toArray.qsort Name.lt + if names.isEmpty then throwError "empty declaration inventory: {modName}" + liftIO <| IO.eprintln s!"SUPERLEVEL_AUDIT_PROGRESS {modName} COUNT {names.size}" + logInfo m!"SUPERLEVEL_AUDIT_MODULE {modName} COUNT {names.size}" + for name in names do + if (env.checked.get.find? name).isNone then + throwError "missing kernel declaration: {name}" + let axs ← Lean.collectAxioms name + logInfo m!"SUPERLEVEL_AUDIT_DECL {name} AXIOMS {axs}" + for ax in axs do + unless allowed.contains ax do + throwError "forbidden transitive axiom {ax} in {name}" + allNames := allNames.push name + let required : Array Name := #[ + `UniversalLaw.Spec.Lifetime.IsSmooth, + `UniversalLaw.Spec.Lifetime.IsCriticalPoint, + `UniversalLaw.Spec.Lifetime.regularPointDerivative_range_eq_top, + `UniversalLaw.Spec.Lifetime.regularPointHasStrictFDerivAt, + `UniversalLaw.Spec.Lifetime.regularPointChart, + `UniversalLaw.Spec.Lifetime.regularPointChart_fst, + `UniversalLaw.Spec.Lifetime.regularPointChart_self, + `UniversalLaw.Spec.Lifetime.mem_regularPointChart_source, + `UniversalLaw.Spec.Lifetime.mem_regularPointChart_target, + `TorusRegularSuperlevel.path_connected_basis_of_openEmbedding, + `TorusRegularSuperlevel.path_connected_basis_of_open, + `TorusRegularSuperlevel.relative_chart_homeomorph, + `TorusRegularSuperlevel.path_connected_basis_of_relative_chart, + `TorusRegularSuperlevel.closed_superlevel_basis_of_chart, + `TorusRegularSuperlevel.closed_superlevel_interior_basis, + `TorusRegularSuperlevel.closed_superlevel_regular_basis, + `TorusRegularSuperlevel.closed_superlevel_path_connected_basis] + for name in required do + unless allNames.contains name do + throwError "required declaration omitted from audit: {name}" + logInfo m!"SUPERLEVEL_AUDIT_STANDARD_ONLY_PASS COUNT {allNames.size}" diff --git a/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevelLiteral.lean b/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevelLiteral.lean new file mode 100644 index 000000000..a7a803960 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/project/RegularSuperlevelLiteral.lean @@ -0,0 +1,55 @@ +import RegularSuperlevel +import RegularPointChart + +/-! +Draft literal regular-point consumers of the separately owned scalar chart. + +Released dependency: Research Task Watch's RegularPointChart.lean at Math- +commit 72edcf5b93be45c29f2d10a26f7d8e861a48f528, 2,767 bytes, SHA-256 +5568c8d6e03f7064cd5924ebe2814ae746100505ae31789d5c975902528f9fa2. +That source was frozen and released by its owner. This C297 consumer has not +yet been compiled or kernel-checked. +It neither reimplements the chart nor modifies the topology candidate under replay. + +The public conclusions are actual path-connected neighborhood bases in the +closed-superlevel subtype. The critical-boundary case and quotient transport +remain outside these statements. +-/ + +open Set Filter Topology +open UniversalLaw.Spec.Lifetime + +namespace TorusRegularSuperlevel + +/-- At a literal noncritical point, the closed superlevel has a neighborhood +basis of path-connected sets. The supplied smoothness and noncriticality +construct the chart through the separately owned regular-point module. -/ +theorem closed_superlevel_regular_basis + {d : ℕ} {g : E d → ℝ} + (hsmooth : IsSmooth d g) + (a : ℝ) (x : {y : E d // a ≤ g y}) + (hregular : ¬ IsCriticalPoint d g x.val) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => + V ∈ 𝓝 x ∧ IsPathConnected V) id := by + exact closed_superlevel_basis_of_chart a x + (regularPointChart hsmooth hregular) + (mem_regularPointChart_source hsmooth hregular) + (fun y _ => regularPointChart_fst hsmooth hregular y) + +/-- The pointwise basis required for eventual global LPC holds at every +strict-interior or literal regular point of the closed superlevel. +No chart or LPC hypothesis appears in this public interface. -/ +theorem closed_superlevel_path_connected_basis + {d : ℕ} {g : E d → ℝ} + (hsmooth : IsSmooth d g) + (a : ℝ) (x : {y : E d // a ≤ g y}) + (hx : a < g x.val ∨ ¬ IsCriticalPoint d g x.val) : + (𝓝 x).HasBasis + (fun V : Set {y : E d // a ≤ g y} => + V ∈ 𝓝 x ∧ IsPathConnected V) id := by + rcases hx with hinterior | hregular + · exact closed_superlevel_interior_basis (hsmooth 0).continuous a x hinterior + · exact closed_superlevel_regular_basis hsmooth a x hregular + +end TorusRegularSuperlevel diff --git a/frontiers/regular_superlevel_geometry_20261020/reviews/ANALYTIC_CONTROL_AND_PRELIM_REVIEW.md b/frontiers/regular_superlevel_geometry_20261020/reviews/ANALYTIC_CONTROL_AND_PRELIM_REVIEW.md new file mode 100644 index 000000000..d4107ffac --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/reviews/ANALYTIC_CONTROL_AND_PRELIM_REVIEW.md @@ -0,0 +1,132 @@ +Public path projection of the retained reviewer-authored record; original 10767 bytes, SHA-256 `a3c688550b970899389024fddd6b94c7bf7feb5dfeb175f9d7b38a1139f791ca`. Only native-root locators are replaced by the named placeholders below; mathematical and review text is unchanged. + +- `$C297_ROOT` replaces a native filesystem prefix (1 occurrence(s)). +- `$PINNED_MATHLIB` replaces a native filesystem prefix (1 occurrence(s)). + +--- + +# C297 analytical control and preliminary source review + +Disposition: **PRELIMINARY_SOURCE_REVIEW; NO FINAL ACCEPTANCE**. + +This note combines the requested mathematical negative-control analysis with a read-only review of candidate 1 of `project/RegularSuperlevel.lean`. Compilation was reported as running when the review was requested. This note does not establish successful elaboration, kernel replay, axiom audit, execution of controls, or a frozen final artifact. + +Reviewer: OpenAI Codex `/root/c292_geometry_review`, delegated work for Dylan Roy. The reviewer did not author or modify this Lean module. Exposure includes previous C292–C295 source reviews, proof-shape advice for C294, and the topology/control advice reproduced below. This is same-provider, source-exposed nonauthor review: organizational independence 0, human review 0. The mathematical control is supporting analysis within C297's claimed scope, not a separate theorem delivery. + +## Exact candidate and reviewed scope + +The complete candidate was read and its identity checked again after the source/API inspection: + +- Path: `$C297_ROOT/project/RegularSuperlevel.lean`. +- Length: **6,173 bytes**. +- SHA-256: **0758454e88cb02ad56483face96483d8a878afe5eaa72f1ea629f0ca5a29760f**. +- Six explicit declarations, lines 17–131, under `TorusRegularSuperlevel`. + +The imported `project/Lifetime.lean` is 51,383 bytes, SHA-256 `90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6`. Its `import Mathlib` and the previously reviewed literal `E d` convention were retained. This review did not rereview all of Lifetime's unrelated specifications. + +The relevant existing API declarations were read in the pinned Mathlib checkout rooted at: + +`$PINNED_MATHLIB`. + +Specifically: + +- `Mathlib/Topology/Connected/LocallyPathConnected.lean`: the neighborhood-basis definition, open-subspace inheritance, and homeomorphism transport. +- `Mathlib/Topology/Constructions.lean`, lines 573–592: restriction of inducing maps, embeddings, and open embeddings to mapped subsets. +- `Mathlib/Topology/Algebra/Module/LocallyConvex.lean`, especially lines 104–121: local path connectivity of real locally convex spaces and convex subsets. + +The review covers the semantic match of these six declarations and their relative-topology interfaces. It does not inspect or construct the separately owned scalar implicit-function chart, nor claim a literal regular-point consumer already exists. + +## Preliminary source findings + +**No concrete mathematical or interface bug was identified in this exact candidate.** This is a preliminary source finding, not a compilation or final acceptance verdict. + +1. `path_connected_basis_of_openEmbedding` (lines 17–29) transfers a path-connected neighborhood basis from the domain to the image point. Continuity pulls the ambient target neighborhood back; the domain's local path connectivity supplies a smaller path-connected neighborhood; openness makes its image a neighborhood of the image point. The image lies in the originally prescribed target neighborhood. It does not require or conclude global local path connectivity of the codomain. + +2. `path_connected_basis_of_open` (lines 32–36) applies that result to the inclusion of an open subtype. Its hypothesis is local path connectivity of this open subtype, and its conclusion concerns an ambient point belonging to the open set. This is a legitimate local transfer, not inheritance by an arbitrary subset. + +3. `relative_chart_homeomorph` (lines 40–68) uses the correct restricted spaces: points of `S` whose ambient values belong to `p.source`, and points of `T` whose ambient values belong to `p.target`. In the inverse, `p.map_target` first establishes that the inverse image lies in the chart source; only then is `hmem` used. The chart's right-inverse identity transfers membership in `T` back to membership in `S`. Both inverse identities and both continuity proofs are confined to their proper chart domains. No global inverse behavior is assumed. + +4. `path_connected_basis_of_relative_chart` (lines 72–86) proves that these source and target intersections are open in `S` and `T` respectively, by preimages under subtype inclusion. It obtains local path connectivity of the target intersection from that of `T`, transports it through the restricted homeomorphism, and uses the open inclusion into `S`. The final `𝓝 x` is the neighborhood filter in the subtype `S`; no ambient openness of `S` or `T` is assumed. + +5. `closed_superlevel_basis_of_chart` (lines 93–115) takes an actual open partial homeomorphism, source membership of the point, and the scalar-coordinate identity on the entire chart source. The model half-space `H = {z : ℝ × F | a ≤ z.fst}` is proved convex, and its local path connectivity is obtained from the real normed-space structure. The coordinate identity then gives the required membership equivalence exactly on the source. This is sufficient for the preceding relative chart result. The proof does not assume a global locally path-connected superlevel, and does not construct a regular-point chart from a derivative. Completeness or finite dimensionality of `F` is unnecessary for this topology step. + +6. `closed_superlevel_interior_basis` (lines 119–131) uses continuity to make `U = {y | a < g y}` open in the Euclidean source. This open set is locally path connected. Its inclusion into `S = {y | a ≤ g y}` is obtained by restricting the identity open embedding using `U ⊆ S`. The actual `IsOpenEmbedding.restrict` interface requires the original source subset to be open, which is precisely the proved `hU`; it does not require `S` to be ambient-open. The final point is the prescribed subtype point, and the output is a basis in `S`. + +The candidate therefore avoids the relative-topology trap described below. The source/target restriction is present in the homeomorphism itself, and the model half-space inherits local path connectivity from proved convexity. The separately owned chart constructor still must supply `p`, `hx`, and `hcoord` before a literal noncritical-point corollary is established. + +## Analytical control: smoothness alone is insufficient + +Define the real function + +\[ +g(x)= +\begin{cases} +e^{-1/x^2}\sin(1/x),&x\ne0,\\ +0,&x=0, +\end{cases} +\qquad S=\{x\in\mathbb R:g(x)\ge0\}. +\] + +For every nonnegative integer \(m\), on \(x\ne0\) the derivative has the form + +\[ +g^{(m)}(x)=e^{-1/x^2} +\bigl(P_m(1/x)\sin(1/x)+Q_m(1/x)\cos(1/x)\bigr) +\] + +for real polynomials \(P_m,Q_m\). Differentiation preserves this form. The exponential factor dominates every reciprocal power of \(|x|\), so both these expressions and their difference quotients at zero tend to zero. Induction establishes \(g\in C^\infty(\mathbb R)\) with \(g^{(m)}(0)=0\) for every \(m\). In particular, \(0\) is critical and its Hessian is zero. + +For each integer \(k\ge1\), set + +\[ +I_k=\left[\frac1{(2k+1)\pi},\frac1{2k\pi}\right], +\qquad +J_k=\left(\frac1{(2k+2)\pi},\frac1{(2k+1)\pi}\right). +\] + +Since the exponential factor is positive off zero, \(g\ge0\) on \(I_k\), with strict positivity in its interior, and \(g<0\) on \(J_k\). Explicit points are + +\[ +p_k=\frac2{(4k+1)\pi},\qquad q_k=\frac2{(4k+3)\pi}. +\] + +Then \(00,\qquad +g(q_k)=-e^{-1/q_k^2}<0. +\] + +Let \(N\subseteq S\) be any neighborhood of zero in the subspace topology of \(S\). There is \(\varepsilon>0\) such that + +\[ +S\cap(-\varepsilon,\varepsilon)\subseteq N. +\] + +For sufficiently large \(k\), the points \(0,p_k\) belong to \(N\). Any path in \(N\) joining them, composed with the inclusion into \(\mathbb R\), must attain \(q_k\) by the intermediate value theorem. This is impossible because \(q_k\notin S\). Thus zero has no path-connected relative neighborhood, and in particular has no path-connected relative neighborhood basis. The interval property of connected subsets of \(\mathbb R\) also excludes connected relative neighborhoods. The positive and negative values accumulating at zero establish that it is a boundary point. + +This refutes removal of both the regular-point and strict-interior alternatives from a statement for arbitrary smooth scalar functions. It does not show that regularity is necessary for every individual function: the zero superlevels of \(x^2\) and \(-x^2\) are locally path connected at their critical point. + +The counterexample is non-Morse, because the critical point at zero is infinitely flat. It does not refute the project's smooth Morse target or show that the project's eventual critical-point argument cannot succeed. It is a conventional mathematical argument, not a formal Lean counterexample or an executed premise-removal test. + +Periodicity is not an obstruction to such a smooth non-Morse control. For any \(L>0\), the explicit function + +\[ +G_L(x)=g\bigl(\sin(2\pi x/L)\bigr) +\] + +is smooth and \(L\)-periodic. The inner map is a local diffeomorphism at zero, so it transports the same local superlevel obstruction. All derivatives of \(G_L\) at zero still vanish. This optional observation adds no Morse or quotient theorem to the review. + +## Wrong-relative-topology control for later review + +For \(g(x)=x\), level \(a=0\), and the regular point \(x=0\), the closed superlevel is \(S=[0,\infty)\). The sets \([0,\varepsilon)\) form a path-connected relative neighborhood basis at zero. They are open in \(S\), but they are not ambient neighborhoods of zero in \(\mathbb R\). + +A purported boundary-point proof that requires its superlevel neighborhoods to belong to the ambient `𝓝 x`, or to be ambient-open subsets of \(S\) containing zero, imposes a false requirement. The intended filter is the neighborhood filter of the superlevel subtype, or the corresponding `𝓝[S] x`. In addition, chart inverse transport must stay inside the chart target. + +The exact candidate reviewed here respects both requirements: all final neighborhood filters are on the superlevel subtype, and the relative homeomorphism explicitly restricts to source and target. + +## Execution and final-review boundary + +No Lean process, compiler, test, kernel replay, or remote post was initiated by this reviewer. Only source reads, local identity calculations, and creation of this authorized review note were performed. No implementation or imported source was modified. + +The final review must bind the eventual frozen source, any separately owned chart input or literal consumer actually included, and the observed build/kernel/control records. This preliminary review does not anticipate those results or grant formal acceptance. diff --git a/frontiers/regular_superlevel_geometry_20261020/reviews/CANDIDATE3_SOURCE_REVIEW.md b/frontiers/regular_superlevel_geometry_20261020/reviews/CANDIDATE3_SOURCE_REVIEW.md new file mode 100644 index 000000000..1be9a1ebe --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/reviews/CANDIDATE3_SOURCE_REVIEW.md @@ -0,0 +1,162 @@ +Public path projection of the retained reviewer-authored record; original 18027 bytes, SHA-256 `c794c85794767711c05f5580bed49d35c011d939c39d0c4a51872b7cccdebc4d`. Only native-root locators are replaced by the named placeholders below; mathematical and review text is unchanged. + +- `$C297_ROOT` replaces a native filesystem prefix (1 occurrence(s)). + +--- + +# C297 candidate 3 exact-source nonauthor review + +Disposition: **PASS_SCOPED_SOURCE**. No unresolved mathematical, public-interface, census-design, or negative-fixture source finding. This is not final formal acceptance: the C297 literal consumer, full module-origin census, and both negative fixtures still require their actual execution evidence. + +The one provenance-comment finding raised during this review was corrected by the author before this report was completed. The corrected literal source is bound below. The reviewer did not edit any Lean source. + +## Reviewer and exposure + +Actual reviewer: OpenAI Codex `/root/c292_geometry_review`, delegated work for Dylan Roy. This is same-provider, source-exposed nonauthor review: organizational independence 0, human review 0. + +Exposure includes C292–C295 reviews, proof-shape advice for C294, C297 relative-topology and analytical-control advice, the complete candidate 1 topology source, the provisional literal consumer, and the exact peer chart source. The reviewer authored the analytical control and preliminary review notes, but did not author the peer chart, topology module, literal consumer, audit source, or either Lean negative fixture. This is not a blind review or a provider-distinct review. + +The complete five Lean module sources and both negative fixtures were read for this review. The literal comment-only amendment was then reread and compared with its retained predecessor. The final source identity check is reported below. Prior review notes remain unchanged. + +## Exact source bindings + +Root directory: + +`$C297_ROOT`. + +| Relative path | Bytes | SHA-256 | +|---|---:|---| +| `project/Lifetime.lean` | 51,383 | `90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6` | +| `project/RegularPointChart.lean` | 2,767 | `5568c8d6e03f7064cd5924ebe2814ae746100505ae31789d5c975902528f9fa2` | +| `project/RegularSuperlevel.lean` | 6,405 | `0db6ce3ea7358a59c089680d774a6806f0fb747c24d9828850377458156e2f02` | +| `project/RegularSuperlevelLiteral.lean` | 2,299 | `334759063a3ae58b42b8cd4a45e3bfd6f3a31b668d18526aa6fdcb5ea65c13d3` | +| `project/RegularSuperlevelAxiomAudit.lean` | 3,248 | `807de09540b9f7f4f4e14c3408f1f82cb08b1e4232c68c04da5a2355cec02f9e` | +| `negative-project/WithoutCoordinateIdentity.lean` | 950 | `167d0afb49457303a61fac6927784e4f0157ed5725739903bf5e33224974b081` | +| `negative-project/WithoutRegularOrInterior.lean` | 838 | `d3c12e33718a00be343d0e2b3cbbd9a1cdf08e8a2062eb3bfeb7026fb47a543d` | + +The chart is the separately owned C296 input released at Math- PR488 head `72edcf5b93be45c29f2d10a26f7d8e861a48f528`, production path `frontiers/regular_point_chart_20261020/RegularPointChart.lean`, Git blob `77a75a4611040973ad355aff40555a808f1816e7`. The reviewer independently computed that Git blob and verified equality of the project bytes with the file content recorded in `evidence/PEER_CHART_DELIVERED_READBACK.json`. That readback is 32,186 bytes, SHA-256 `1eb5139b0e658fd9bdf5fc47d642e784ab46cfb21bb5f8066a4200507e05d2c4`, and contains the owner's release comment `6289952847`. This review did not repeat the remote fetch or independently certify the peer's entire hosted execution. + +## Literal statement and imported hypotheses + +The imported definitions have their actual intended meaning: + +- `E d` is `EuclideanSpace ℝ (Fin d)`. +- `IsSmooth d g` means `∀ n : ℕ, ContDiff ℝ n g`. +- `IsCriticalPoint d g x` means `fderiv ℝ g x = 0`. + +No field, bar interface, Gaussian law, Morse predicate, periodicity condition, supplied path, or global local-path-connectivity instance is used to obtain the C297 public conclusions. The unrelated Lifetime statements remain definitions/specifications and are not promoted by this work. + +The literal theorem `closed_superlevel_regular_basis` supplies a path-connected neighborhood basis at the prescribed point of `{y : E d // a ≤ g y}` from smoothness and literal noncriticality. Its public inputs contain neither a chart nor an LPC premise. + +The second public theorem, `closed_superlevel_path_connected_basis`, retains the explicit condition + +`a < g x.val ∨ ¬ IsCriticalPoint d g x.val`. + +It handles strict-interior points and regular points, including regular boundary points. It does not handle a critical boundary point merely because the function is smooth or Morse. The point is a subtype point, so its membership in the weak superlevel is already supplied. + +The statements allow any natural dimension. In dimension zero the regular branch has an impossible nonzero scalar derivative premise; the strict-interior branch remains valid. This is not a missing positive-dimension assumption. Smoothness is stronger than the continuity needed for the interior branch and supplies the strict derivative needed for the peer chart. + +## Mathematical reconstruction + +### Peer chart consumption + +The peer first proves that literal noncriticality makes the derivative's underlying linear map nonzero. Pointwise extensionality converts a hypothetical zero underlying linear map into zero of the continuous linear map. The scalar dual range theorem then yields full range. + +The separate smoothness lemma supplies `HasStrictFDerivAt g (fderiv ℝ g x) x` from smoothness at order one. These two actual facts instantiate the existing finite-dimensional-target implicit-function chart. Its target is the actual product `ℝ × (fderiv ℝ g x).ker`; no assumed coordinate identification of the kernel is needed. + +The chart's source-membership lemma and first-coordinate identity are passed to the C297 topology theorem at the same `g` and `x`. Its global first-coordinate equality is used only where the topology theorem requires it, on the chart source. No global inverse behavior is inferred. + +The derivative kernel carries the required real normed-space structure. The topology theorem does not require it to be complete or explicitly finite dimensional; the existing normed-space structure suffices for the convex half-space argument. + +### Relative topology + +`path_connected_basis_of_openEmbedding` pulls an arbitrary target neighborhood back through a continuous open embedding, selects a smaller path-connected domain neighborhood, and maps it forward. Openness supplies target-neighborhood membership and continuity supplies path connectivity. The image lies inside the original target neighborhood. No global LPC of the codomain is required. + +`path_connected_basis_of_open` specializes this to inclusion of an open subtype that is already LPC. + +`relative_chart_homeomorph` restricts the domain to points of `S` lying in `p.source` and the codomain to points of `T` lying in `p.target`. In its inverse, `p.map_target` first puts the inverse image in the source. The source-local membership equivalence and the chart right-inverse identity then prove membership in `S`. The two inverse identities and continuity arguments use exactly the chart restrictions under which those properties hold. + +`path_connected_basis_of_relative_chart` makes the source and target intersections open in their respective subtypes. It obtains LPC of the target intersection from LPC of `T`, transports it through the restricted homeomorphism, and then transfers the pointwise basis through the open inclusion into `S`. It does not assume ambient openness of either `S` or `T`. + +`closed_superlevel_basis_of_chart` takes the model half-space + +`H = {z : ℝ × F | a ≤ z.fst}`. + +The explicit convexity proof uses nonnegative scalar weights summing to one. The real normed product is locally convex, so convexity supplies LPC of the subtype `H`. The coordinate identity gives the exact membership equivalence on `p.source`. This proves the relative basis result without assuming the desired superlevel LPC. + +For arbitrary `g`, this generic chart theorem does not assert that the whole superlevel is ambient-closed: its public hypotheses only constrain `g` on the chart source. Its conclusion is still valid. In the literal smooth consumer the weak superlevel is genuinely closed by continuity, although global closedness is not needed by the local argument. + +`closed_superlevel_interior_basis` takes the open ambient set `U = {y | a < g y}`. Continuity proves its openness and the Euclidean LPC instance gives LPC of `U`. The inclusion into `S = {y | a ≤ g y}` is the restriction of the identity open embedding. The explicit `MapsTo` proof and specified `(s := U) (t := S)` instantiate the actual restriction interface correctly. Its image is relatively open in `S`; the proof does not require `S` to be ambient-open. + +All final neighborhood filters are those of the actual superlevel subtype. The implementation avoids the false requirement that a boundary point admit an ambient neighborhood contained in its closed superlevel. + +## Candidate changes and closed finding + +The candidate 1 to candidate 3 topology diff changes only proof elaboration details: + +- the `hasBasis_self` witness uses the correct flat constructor grouping; +- four proposition-valued local instance introductions use `let`; +- membership in the let-bound superlevel subtype is explicitly reduced to an inequality; +- the strict-interior inclusion uses an explicitly typed identity, an explicit `MapsTo` proof, and named source/target arguments. + +The six declaration statements and their mathematical roles are unchanged. Candidate 2 to candidate 3 changes only the final open-embedding restriction elaboration. + +During this review, the old 2,271-byte literal file still described the peer chart as provisional at `9873446f5728799ef3d12808df65344827ac4754`, despite its delivered owner-release readback. This was a nonblocking provenance defect, not a theorem defect. The author corrected the header to the released `72edcf5b93be45c29f2d10a26f7d8e861a48f528` input and retained the explicit pending status of the C297 consumer's own execution. The reviewer read the corrected header and verified that every byte from `open Set Filter Topology` onward is identical to the retained `a8c1946f07cee68a4e3210304fdc997455a4e443d0f9edb3b54bfac387702d4e` predecessor. **Finding closed.** + +## Full-census source design + +The audit source imports the literal consumer, thereby importing the four intended source/proof modules. Its census selects declarations by actual module origin for `Lifetime`, `RegularPointChart`, `RegularSuperlevel`, and `RegularSuperlevelLiteral`. It does not restrict the census to a namespace or a handpicked list of public theorem names. + +The environment view is set to nonexporting before enumerating constants, so private and generated declarations are eligible. Each requested module must exist and have a nonempty inventory. Every enumerated name must be present in the checked kernel environment. The code invokes `Lean.collectAxioms` for every name and rejects any returned axiom outside `propext`, `Classical.choice`, and `Quot.sound`; thus `sorryAx` is not permitted. + +The additional required list contains exactly 17 names: two literal Lifetime definitions, seven peer-chart declarations, six topology declarations, and two literal consumers. This is an omission guard, not the total-census definition or a claim that the total inventory has size 17. The actual complete inventory count must be measured from the run. + +The reviewer also read the installed Lean `Lean/Util/CollectAxioms.lean`: it uses the private environment, kernel declarations, and transitive axiom information, including precomputed information for imported declarations. The audit therefore is not a fresh kernel replay of the full import closure. The three initial `#print axioms` commands and three explicit `#check` commands provide selected additional output; they do not replace the module-origin enumeration. + +The audit implementation is source-appropriate for the stated four-module census. No actual census success, count, or standard-only outcome is inferred before its execution. The hosted runner and its output parser are outside this source review. + +## Negative fixtures and analytical control + +`WithoutCoordinateIdentity.lean` supplies the chart and source-membership proof but omits the final source-local first-coordinate identity from the actual `closed_superlevel_basis_of_chart` invocation. The remaining term has a function type from that identity premise to the basis conclusion, whereas the fixture requests the basis proposition itself. A meaningful execution result is the corresponding premise/function-versus-conclusion type mismatch after successful imports. Syntax, unknown-name, import, resource-limit, or timeout failures do not satisfy this control. + +`WithoutRegularOrInterior.lean` supplies smoothness, the level, and the subtype point, but omits the final disjunction from the actual `closed_superlevel_path_connected_basis` invocation. The expected meaningful rejection is again the remaining premise function versus the requested basis proposition, identifying the regular-or-strict-interior condition. This fixture does not prove that no different theorem or proof could cover a particular critical point. + +Both fixtures are deliberately ill-typed interface tests, not Lean counterexamples, and neither had an executed outcome in the evidence reviewed here. + +The supporting analytical control is the smooth function + +\[ +g(0)=0,\qquad g(x)=e^{-1/x^2}\sin(1/x)\quad(x\ne0). +\] + +All its derivatives at zero vanish, by the polynomial-times-flat-exponential derivative formula. For \(k\ge1\), set + +\[ +p_k=\frac{2}{(4k+1)\pi},\qquad q_k=\frac{2}{(4k+3)\pi}. +\] + +Then \(00\), and \(g(q_k)<0\). Every relative neighborhood of zero in \(S=\{g\ge0\}\) contains some \(p_k\). A path in that neighborhood from zero to \(p_k\) would pass through \(q_k\) by the intermediate value theorem, which is impossible. Thus there is no path-connected relative neighborhood basis at this critical boundary point. + +This demonstrates that arbitrary smoothness does not justify dropping both alternatives. It is non-Morse and does not refute the project's Morse target. The detailed sign intervals, flatness argument, optional smooth periodic composition, and limitations are recorded in the unchanged `reviews/ANALYTIC_CONTROL_AND_PRELIM_REVIEW.md`, 10,767 bytes, SHA-256 `a3c688550b970899389024fddd6b94c7bf7feb5dfeb175f9d7b38a1139f791ca`. + +The separate topology trap is \(g(x)=x\), level zero, at the regular boundary point zero. The sets \([0,\varepsilon)\) are path-connected relative neighborhoods in \([0,\infty)\), but are not ambient neighborhoods of zero in \(\mathbb R\). The reviewed statements and proofs use the correct subtype filters. This mathematical check is not reported as an executed Lean control. + +## Observed execution records and their limits + +This reviewer initiated no Lean build, kernel replay, negative test, or hosted run. The following are records of Claude S's separate execution, read from the retained evidence: + +- Candidate 1: source `0758454e88cb02ad56483face96483d8a878afe5eaa72f1ea629f0ca5a29760f`, compile rc 1, 48 seconds, no object and no kernel replay. The full projected stdout is 2,087 bytes, SHA-256 `8b828f7860a2106ab45d8d37cf5560c842f6ea3bb9652592fff9c41c7ad5db45`. Constructor grouping and subtype elaboration failed; four style warnings were also present. +- Candidate 2: source `b5733777504470cc1a2edfff780d0d7b7f271fdfc3db377cdb093f7e356f946d`, compile rc 1, 47 seconds, no object and no kernel replay. The retained report `evidence/CANDIDATE2_RESULT.json` is 10,735 bytes, SHA-256 `4fbdb29d4c2eecf5b5ec13daf770ef3c225e83c5f41bf584cebd8e7b08b1d866`. The actual reported error concerns inference of the source subset/topology in `IsOpenEmbedding.restrict`. +- Candidate 3: source `0db6ce3ea7358a59c089680d774a6806f0fb747c24d9828850377458156e2f02`, build rc 0 under warning escalation, empty streams, 12.5 seconds; standard `leanchecker -v RegularSuperlevel` rc 0, 10 seconds. The reported Linux object is 208,992 bytes, SHA-256 `cffe26cd70fb2b8e2ddf965562a794745a1358bc22e012a85953578d14220526`, unchanged after replay. + +For candidate 3 the reviewer read `evidence/LINUX_CANDIDATE3_RESULT.json` (11,077 bytes, SHA-256 `ab3b3d8de572310e6054d83e8cf5475ea9f6223c6fc648f89f59246571d9f950`) and the complete `evidence/linux-candidate3-receipt.json` (2,864 bytes, SHA-256 `3f479a7fc32198389acb8d9db23f913495a5357b1ae1e56cd39e6107074e9ef0`). The saved kernel stdout was read and hashed: 28 bytes, SHA-256 `92c0c414a888780c0722d6767245b01bd449841486bdd45f93f47c116fe57b0b`, containing `replaying RegularSuperlevel` and its newline. The report is Math487 comment `6290047895`; the executor is Anthropic Claude session `session_01S16677s1SGeAJmN3QMz4ip`. + +That successful execution covers the six-declaration topology module against its imported environment. It is not `--fresh`, does not establish the literal consumer's elaboration, and includes no C297 full census or either negative fixture. The reviewer did not fetch or independently replay the Linux object. Earlier clean-looking declarations in failed candidates are not counted as separately verified objects. + +## Final boundary + +No unresolved source-level finding prevents freezing these exact proof inputs for the next execution stage. This verdict does not grant formal acceptance in advance of the remaining evidence. + +Still outside this result are the critical-point Morse local form, relative topology at critical boundary points, quotient chart transport, actual global closed-level LPC, C294's critical-level LPC premise removal, strict death drop, and the complete ordinary-H0 adapter. Scientific effect is NONE. Source identities, semantic review, external execution reports, full-census execution, negative-control execution, and eventual final acceptance remain distinct evidence categories. + +Only this new review note was written by the reviewer. Earlier review notes, all Lean sources, imported inputs, execution artifacts, claims, and remote records were left unchanged by the reviewer. diff --git a/frontiers/regular_superlevel_geometry_20261020/reviews/HOSTED_ENGINEERING_SOURCE_REVIEW.md b/frontiers/regular_superlevel_geometry_20261020/reviews/HOSTED_ENGINEERING_SOURCE_REVIEW.md new file mode 100644 index 000000000..2077a9204 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/reviews/HOSTED_ENGINEERING_SOURCE_REVIEW.md @@ -0,0 +1,45 @@ +# C297 hosted engineering source review + +**`PASS_SCOPED_ENGINEERING_SOURCE` — no unresolved publication-blocking finding in the final reviewed bytes.** This approves the verifier's source design for the stated scope; it does not claim hosted execution or formal acceptance. + +Actual reviewer: OpenAI Codex `/root/c292_geometry_review`, delegated work for Dylan Roy. This is same-provider, source-exposed nonauthor engineering review, with organizational independence 0 and human review 0. Prior exposure includes C292–C295 reviews, C294 proof-shape advice, C297 topology/control advice, and the C297 proof-source reviews. The reviewer did not author the hosted verifier, its test module, or its workflow. The reviewer identified the multiline audit-output issue below and reviewed the author's correction. + +The relative links in the following table address the published packet layout. These exact files were reviewed in the working directory's `hosted/` staging area and rehashed at the end of the review. + +| Reviewed artifact | Bytes | SHA-256 | +|---|---:|---| +| [c297_hosted_verify.py](../c297_hosted_verify.py) | 25,481 | `fefd7500e698d75c60cc907c3b679a498e598a4c235f3b3e7fe2e1102502e217` | +| [test_c297_hosted_verify.py](../test_c297_hosted_verify.py) | 10,784 | `8510b0fca398f75dc28dd35bae5ab7c6f6d2735c74b453d2c93c0606b4c3df28` | +| `c297-regular-superlevel.yml` (published at `.github/workflows/c297-regular-superlevel.yml`) | 3,129 | `03b3d8fb4ca95316247b93ad3937ea2d56f0509040c819534873be1bb341eab3` | + +The concrete blocker found during review is **closed**: the original physical-line audit parser rejected valid wrapped axiom arrays emitted by pinned Lean. I checked actual retained C294 examples, read the failing regression, reviewed the logical-record replacement, and read the subsequent normal and optimized nine-test results. The replacement preserves rejection of interrupted/truncated records, malformed records, duplicate declarations, forbidden axioms, and missing required targets. + +The final implementation matches the requested execution contract: + +- **Five fresh builds:** an initially absent local object directory, ordered builds of Lifetime, peer chart, topology, literal consumer, and audit. +- **Four standard kernel replays:** peer chart, topology, literal consumer, and audit; no claim of fresh import-closure replay. +- **Complete four-module census:** all declaration records are parsed, module counts and total must agree, all 17 required targets must occur, and axioms are restricted to the three standard names. +- **Two negatives:** exact omitted-premise invocation and diagnostic checks, not merely exit-code checks. Overall success requires semantic validation of both. +- **Source/object stability:** hashes are checked before and after verification; existing local objects cannot change, builds may add only their own permitted outputs, and replay/control phases cannot alter the inventory. +- **Failure evidence:** handled process failures and timeouts retain binary streams and receipts. Completed object/control metadata is saved consistently in phase and aggregate records. Timeout handling tolerates the process-exit/kill race. +- **Workflow:** commit-pinned actions, `contents: read`, checkout credentials disabled, bounded timeouts, and an always-run artifact upload. Tested commit/tree, PR head/base context, run/attempt, actual runtime binaries, and dependency pins are recorded. + +I independently matched the workflow's manifest digest, **`c339a9d1ca5b9ef70f8d581ea0760f11922aba2cd16cbeeb7aba02092b476e94`**, to the 1,539-byte local [manifest](../HOSTED_SOURCE_MANIFEST.json) and verified all seven file bindings against the reviewed sources. + +For interpreting future evidence, a phase-level `PASS` initially records the expected process/object outcome. Negative acceptance additionally requires `intended_missing_premise_rejection: true` and the aggregate final success status. Remote source-origin equality and full dependency-artifact custody remain separately scoped owner checks, as the verifier states. + +The retained engineering records read during review include `TEST_WRAPPED_RED.*`, `TEST_WRAPPED_GREEN.*`, and `TEST_WRAPPED_OPTIMIZED.*`, plus `C294_WRAPPED_OUTPUT_CHARACTERIZATION.json`. The latter records a marker-prefix-only projection of the retained C294 audit stdout, SHA-256 `062a8168ad5b05f1238ea8fd516d7fc5a806941cf77480b6de6837921c294386`, and an author-performed parser check covering its 235 declarations. This is reuse of existing output to characterize the engineering parser, not a new Lean run or a C297 census result. + +## C296-N1 dependency boundary + +A later coordination update supplied by the root reports a separate native review, ID `5584579361`, and [Math488 comment `6290185439`](https://github.com/d6g8k5htny-coder/Math-/pull/488#issuecomment-6290185439), with disposition `AMEND_SCOPED` for C296-N1 at peer head `72edcf5b93be45c29f2d10a26f7d8e861a48f528`. The reported finding concerns the peer workflow's negative classifier accepting some token-containing syntax, setup, or resource failures. The update reports that the actual hosted negative was the intended type mismatch and that the mathematical/interface source was clean. + +This paragraph attributes that coordination update; this reviewer did not independently reread or reproduce the separate native finding and does not supply the peer's approval or fix. It does not convert the C296 peer PR into a blanket accepted dependency. + +C297 consumes the exact `RegularPointChart.lean` proof source, 2,767 bytes, SHA-256 `5568c8d6e03f7064cd5924ebe2814ae746100505ae31789d5c975902528f9fa2`. It does not consume the peer workflow or negative classifier. The C297 verifier's own two controls use the stricter invocation and diagnostic checks reviewed above, and the C297 execution contract rebuilds and replays the chart module. C296-N1 remains with its existing reviewer and source owner; no takeover or duplicate repair is implied. + +## Reviewer actions and limits + +Same-provider, source-exposed nonauthor engineering review, **org0/human0**. I read retained test records but ran no tests, Lean, hosted execution, or remote action, and edited no implementation files. The only subsequent reviewer write was this authorized review record, preserving the substantive engineering verdict and adding the explicitly attributed dependency caveat. + +This is source-bound engineering review. Actual hosted outcomes, downloaded artifact equality, final formal acceptance, source custody, and scientific acceptance remain separate gates. diff --git a/frontiers/regular_superlevel_geometry_20261020/reviews/PROJECTION_IDENTITIES.json b/frontiers/regular_superlevel_geometry_20261020/reviews/PROJECTION_IDENTITIES.json new file mode 100644 index 000000000..211befe77 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/reviews/PROJECTION_IDENTITIES.json @@ -0,0 +1,32 @@ +[ + { + "path": "reviews/CANDIDATE3_SOURCE_REVIEW.md", + "original_bytes": 18027, + "original_sha256": "c794c85794767711c05f5580bed49d35c011d939c39d0c4a51872b7cccdebc4d", + "public_bytes": 18301, + "public_sha256": "3b235ab4cdfb6b28c4b21c45424fd03bb1a7e9d27b5f91e8003934364468b3b4", + "replacements": [ + { + "replacement": "$C297_ROOT", + "occurrences": 1 + } + ] + }, + { + "path": "reviews/ANALYTIC_CONTROL_AND_PRELIM_REVIEW.md", + "original_bytes": 10767, + "original_sha256": "a3c688550b970899389024fddd6b94c7bf7feb5dfeb175f9d7b38a1139f791ca", + "public_bytes": 11006, + "public_sha256": "177e11e6b873d89f186aec8d85b8a3aef117635156fb91ac630073ac5b8e8fbe", + "replacements": [ + { + "replacement": "$C297_ROOT", + "occurrences": 1 + }, + { + "replacement": "$PINNED_MATHLIB", + "occurrences": 1 + } + ] + } +] diff --git a/frontiers/regular_superlevel_geometry_20261020/test_c297_hosted_verify.py b/frontiers/regular_superlevel_geometry_20261020/test_c297_hosted_verify.py new file mode 100644 index 000000000..372ce6d7f --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/test_c297_hosted_verify.py @@ -0,0 +1,193 @@ +"""Engineering controls only. No Lean invocation or scientific acceptance.""" +import hashlib +import importlib.util +import inspect +import json +import os +from pathlib import Path +import sys +import tempfile +import unittest + +MODULE_PATH = Path(__file__).with_name('c297_hosted_verify.py') + + +class HostedVerifierTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + if MODULE_PATH.exists(): + spec = importlib.util.spec_from_file_location('c297_hosted_verify', MODULE_PATH) + cls.v = importlib.util.module_from_spec(spec) + spec.loader.exec_module(cls.v) + else: + cls.v = None + + def verifier(self): + self.assertIsNotNone(self.v, 'the scoped verifier is not implemented') + return self.v + + def test_modified_source_bytes_are_rejected(self): + """Dropping size/hash verification would accept the modified file.""" + v = self.verifier() + with tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / 'Proof.lean' + path.write_bytes(b'abc') + expected = {'bytes': 3, 'sha256': + 'ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad'} + v.verify_file(path, expected, Path(tmp)) + path.write_bytes(b'abd') + with self.assertRaisesRegex(RuntimeError, 'identity mismatch'): + v.verify_file(path, expected, Path(tmp)) + + def test_audit_cannot_omit_required_target_or_hide_axiom(self): + """Count-only validation would accept a substituted target or sorryAx.""" + v = self.verifier() + good = ( + 'SUPERLEVEL_AUDIT_MODULE A COUNT 1\n' + 'SUPERLEVEL_AUDIT_DECL A.target AXIOMS [propext]\n' + 'SUPERLEVEL_AUDIT_MODULE B COUNT 1\n' + 'SUPERLEVEL_AUDIT_DECL B.target AXIOMS []\n' + 'SUPERLEVEL_AUDIT_STANDARD_ONLY_PASS COUNT 2\n') + got = v.validate_audit(good, modules=('A', 'B'), required=('A.target', 'B.target')) + self.assertEqual(got['declaration_count'], 2) + for bad in (good.replace('B.target', 'B.other'), + good.replace('[propext]', '[sorryAx]'), + good.replace('B.target AXIOMS []', 'A.target AXIOMS []')): + with self.subTest(bad=bad), self.assertRaises(RuntimeError): + v.validate_audit(bad, modules=('A', 'B'), required=('A.target', 'B.target')) + + def test_pinned_lean_multiline_axiom_records(self): + """Actual pinned Lean wraps the unchanged Lifetime axiom arrays.""" + v = self.verifier() + proper = ( + 'SUPERLEVEL_AUDIT_MODULE Lifetime COUNT 1\n' + 'SUPERLEVEL_AUDIT_DECL UniversalLaw.Spec.Lifetime.IsUnrestrictedLeadingCoefficient AXIOMS [propext,\n' + ' Classical.choice,\n' + ' Quot.sound]\n' + 'SUPERLEVEL_AUDIT_STANDARD_ONLY_PASS COUNT 1\n') + args = {'modules': ('Lifetime',), + 'required': ('UniversalLaw.Spec.Lifetime.IsUnrestrictedLeadingCoefficient',)} + self.assertEqual(v.validate_audit(proper, **args)['declaration_count'], 1) + for bad in (proper.replace(' Quot.sound]', ' sorryAx]'), + proper.replace(' Quot.sound]\n', ''), + proper.replace(' Quot.sound]', ' Quot.sound] trailing garbage'), + proper[:proper.index(' Quot.sound]')]): + with self.subTest(bad=bad), self.assertRaises(RuntimeError): + v.validate_audit(bad, **args) + + def test_fake_negative_or_import_failure_cannot_pass(self): + """Exit-only or theorem-name-only validation accepts the wrong rejection.""" + v = self.verifier() + proper = ( + 'WithoutRegularOrInterior.lean:25:2: error: Type mismatch\n' + ' TorusRegularSuperlevel.closed_superlevel_path_connected_basis hsmooth a x\n' + 'has type\n a < g ↑x ∨ ¬IsCriticalPoint d g ↑x → (𝓝 x).HasBasis basis id\n' + 'but is expected to have type\n (𝓝 x).HasBasis basis id\n') + v.validate_negative('WithoutRegularOrInterior', 1, proper) + for code, output in ((0, proper), (-9, proper), + (1, proper.replace('a < g ↑x ∨ ¬IsCriticalPoint d g ↑x →', 'Continuous g →')), + (1, proper + 'unknown module RegularSuperlevel\n'), + (1, proper.replace('Type mismatch', 'unexpected token'))): + with self.subTest(code=code, output=output), self.assertRaises(RuntimeError): + v.validate_negative('WithoutRegularOrInterior', code, output) + coordinate = ( + 'WithoutCoordinateIdentity.lean:26:2: error: Type mismatch\n' + ' TorusRegularSuperlevel.closed_superlevel_basis_of_chart a x p hx\n' + 'has type\n (∀ y ∈ p.source, (p y).fst = g y) → (𝓝 x).HasBasis basis id\n' + 'but is expected to have type\n (𝓝 x).HasBasis basis id\n') + v.validate_negative('WithoutCoordinateIdentity', 1, coordinate) + with self.assertRaises(RuntimeError): + v.validate_negative('WithoutCoordinateIdentity', 1, + coordinate.replace('(p y).fst = g y', 'True')) + + def test_failed_phase_receipt_and_exact_streams_survive_abort(self): + """Raising before persistence would discard the actual failing phase.""" + v = self.verifier() + with tempfile.TemporaryDirectory() as tmp: + evidence = Path(tmp) + report = {'status': 'HOLD_NOT_COMPLETED', 'phase_results': []} + with self.assertRaisesRegex(RuntimeError, 'unexpected exit'): + v.run_phase('deliberate-failure', + [sys.executable, '-c', + 'import sys;sys.stdout.buffer.write(b"out\\xff");sys.stderr.write("err");sys.exit(7)'], + evidence, dict(os.environ), evidence, report, timeout=10) + saved = json.loads((evidence / 'RESULT.json').read_text()) + phase = saved['phase_results'][0] + self.assertEqual(phase['exit_code'], 7) + self.assertEqual(phase['status'], 'FAIL') + self.assertFalse(phase['timed_out']) + self.assertEqual((evidence / 'deliberate-failure.stdout').read_bytes(), b'out\xff') + self.assertEqual((evidence / 'deliberate-failure.stderr').read_bytes(), b'err') + self.assertEqual(phase['stdout_sha256'], hashlib.sha256(b'out\xff').hexdigest()) + self.assertTrue((evidence / 'deliberate-failure.receipt.json').exists()) + + + def test_timeout_preserves_partial_stream_and_receipt(self): + """Timeout handling must not discard the child output or phase result.""" + v = self.verifier() + with tempfile.TemporaryDirectory() as tmp: + evidence = Path(tmp) + report = {'status': 'HOLD_NOT_COMPLETED', 'phase_results': []} + with self.assertRaises(RuntimeError): + v.run_phase('deliberate-timeout', + [sys.executable, '-u', '-c', + 'import time;print("before timeout");time.sleep(3)'], + evidence, dict(os.environ), evidence, report, timeout=0.1) + receipt = json.loads((evidence / 'deliberate-timeout.receipt.json').read_text()) + self.assertTrue(receipt['timed_out']) + self.assertEqual(receipt['status'], 'FAIL') + self.assertEqual((evidence / 'deliberate-timeout.stdout').read_bytes(), b'before timeout\n') + + def test_phase_rejects_imported_object_mutation(self): + """A successful compiler process may not alter a prior input object.""" + v = self.verifier() + self.assertIn('build_dir', inspect.signature(v.run_phase).parameters, 'object input monitoring is not implemented') + with tempfile.TemporaryDirectory() as tmp: + evidence = Path(tmp) + build = evidence / 'objects' + build.mkdir() + (build / 'Lifetime.olean').write_bytes(b'frozen input') + report = {'status': 'HOLD_NOT_COMPLETED', 'phase_results': []} + with self.assertRaises(RuntimeError): + v.run_phase('deliberate-object-mutation', + [sys.executable, '-c', + 'from pathlib import Path;Path("objects/Lifetime.olean").write_bytes(b"changed")'], + evidence, dict(os.environ), evidence, report, + timeout=10, build_dir=build) + receipt = json.loads((evidence / 'deliberate-object-mutation.receipt.json').read_text()) + self.assertEqual(receipt['exit_code'], 0) + self.assertEqual(receipt['status'], 'FAIL') + self.assertIn('Lifetime.olean', receipt['objects_before']) + self.assertNotEqual(receipt['objects_before'], receipt['objects_after']) + self.assertIsNotNone(receipt['object_validation_error']) + + def test_build_allows_only_its_own_outputs(self): + """A build may add its target object, not an unrelated replacement.""" + v = self.verifier() + self.assertTrue(hasattr(v, 'validate_objects'), 'object change validation is not implemented') + previous = {'Lifetime.olean': {'bytes': 2, 'sha256': 'a' * 64}} + good = dict(previous, **{'RegularSuperlevel.olean': {'bytes': 3, 'sha256': 'b' * 64}}) + v.validate_objects(previous, good, 'RegularSuperlevel') + for bad in (dict(good, **{'Unrelated.olean': {'bytes': 1, 'sha256': 'c' * 64}}), + previous, + dict(good, **{'Lifetime.olean': {'bytes': 2, 'sha256': 'd' * 64}})): + with self.subTest(bad=bad), self.assertRaises(RuntimeError): + v.validate_objects(previous, bad, 'RegularSuperlevel') + + def test_amended_phase_receipt_matches_aggregate(self): + """Semantic/object metadata must not exist only in the aggregate receipt.""" + v = self.verifier() + self.assertTrue(hasattr(v, 'save_phase'), 'amended receipt persistence is not implemented') + with tempfile.TemporaryDirectory() as tmp: + evidence = Path(tmp) + report = {'status': 'HOLD_NOT_COMPLETED', 'phase_results': []} + rec, _, _ = v.run_phase('valid-phase', [sys.executable, '-c', 'pass'], + evidence, dict(os.environ), evidence, report, timeout=10) + rec['intended_missing_premise_rejection'] = True + v.save_phase(evidence, report, rec) + self.assertEqual(json.loads((evidence / 'valid-phase.receipt.json').read_text()), + json.loads((evidence / 'RESULT.json').read_text())['phase_results'][0]) + + +if __name__ == '__main__': + unittest.main() From 363a533e8e0a1308781d88697f46479e327dd344 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 20 Oct 2026 07:11:26 -0500 Subject: [PATCH 2/2] Recognize displayed chart coercion in C297 negative-control evidence Retain the first hosted HOLD, reproduce its exact diagnostic, and permit only the optional coercion display in the required coordinate identity. No Lean proof, source manifest, workflow, or scientific status changes. --- .../c297_hosted_verify.py | 2 +- .../COERCION_PROJECTION_IDENTITIES.json | 15 ++++ .../development/TEST_COERCION_GREEN.stderr | 25 ++++++ .../development/TEST_COERCION_GREEN.stdout | 4 + .../TEST_COERCION_OPTIMIZED.stderr | 25 ++++++ .../TEST_COERCION_OPTIMIZED.stdout | 4 + .../development/TEST_COERCION_RED.stderr | 36 ++++++++ .../development/TEST_COERCION_RED.stdout | 4 + ...sted-run1-WithoutCoordinateIdentity.stdout | 6 ++ ...osted-run1-WithoutRegularOrInterior.stdout | 6 ++ .../HOSTED_COERCION_AMENDMENT_REVIEW.md | 86 +++++++++++++++++++ .../test_c297_hosted_verify.py | 21 +++++ 12 files changed, 233 insertions(+), 1 deletion(-) create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/COERCION_PROJECTION_IDENTITIES.json create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_GREEN.stderr create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_GREEN.stdout create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_OPTIMIZED.stderr create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_OPTIMIZED.stdout create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_RED.stderr create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_RED.stdout create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/hosted-run1-WithoutCoordinateIdentity.stdout create mode 100644 frontiers/regular_superlevel_geometry_20261020/development/hosted-run1-WithoutRegularOrInterior.stdout create mode 100644 frontiers/regular_superlevel_geometry_20261020/reviews/HOSTED_COERCION_AMENDMENT_REVIEW.md diff --git a/frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py b/frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py index 518053213..ae29c544f 100644 --- a/frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py +++ b/frontiers/regular_superlevel_geometry_20261020/c297_hosted_verify.py @@ -209,7 +209,7 @@ def validate_negative(name, returncode, output): and 'IsCriticalPoint d g' in flat) elif name == 'WithoutCoordinateIdentity': ok = ('closed_superlevel_basis_of_chart a x p hx' in flat and '∀' in flat - and 'p.source' in flat and re.search(r'\(p y\)\.(?:fst|1)\s*=\s*g y', flat)) + and 'p.source' in flat and re.search(r'\(↑?p y\)\.(?:fst|1)\s*=\s*g y', flat)) else: raise RuntimeError('unknown negative control') if not ok: diff --git a/frontiers/regular_superlevel_geometry_20261020/development/COERCION_PROJECTION_IDENTITIES.json b/frontiers/regular_superlevel_geometry_20261020/development/COERCION_PROJECTION_IDENTITIES.json new file mode 100644 index 000000000..6bbdafddd --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/COERCION_PROJECTION_IDENTITIES.json @@ -0,0 +1,15 @@ +{ + "scope": "Only native path spelling projected; full original retained privately. No mathematical, diagnostic or test-result omission.", + "failed_prepublication_attempt": "Path-screen rejected unprojected RED stderr; no remote write occurred from that rejected staging attempt.", + "projections": [ + { + "path": "development/TEST_COERCION_RED.stderr", + "original_bytes": 2742, + "original_sha256": "0045daa87111a04665923f19287703530e31e0ab4f54dc99dcd4c046850863af", + "published_bytes": 2580, + "published_sha256": "dc1858215dd9372d2211892eb22e9d8ecbc3bc61df85ebdc1e299038ea91ccae", + "replacement": "native C297 root path replaced by $C297_ROOT", + "replacements": 2 + } + ] +} diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_GREEN.stderr b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_GREEN.stderr new file mode 100644 index 000000000..e075685e8 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_GREEN.stderr @@ -0,0 +1,25 @@ +test_actual_coordinate_diagnostic_with_displayed_coercion (test_c297_hosted_verify.HostedVerifierTests) +Run 39418891714 prints the chart coercion as (↑p y), not (p y). ... ok +test_amended_phase_receipt_matches_aggregate (test_c297_hosted_verify.HostedVerifierTests) +Semantic/object metadata must not exist only in the aggregate receipt. ... ok +test_audit_cannot_omit_required_target_or_hide_axiom (test_c297_hosted_verify.HostedVerifierTests) +Count-only validation would accept a substituted target or sorryAx. ... ok +test_build_allows_only_its_own_outputs (test_c297_hosted_verify.HostedVerifierTests) +A build may add its target object, not an unrelated replacement. ... ok +test_failed_phase_receipt_and_exact_streams_survive_abort (test_c297_hosted_verify.HostedVerifierTests) +Raising before persistence would discard the actual failing phase. ... ok +test_fake_negative_or_import_failure_cannot_pass (test_c297_hosted_verify.HostedVerifierTests) +Exit-only or theorem-name-only validation accepts the wrong rejection. ... ok +test_modified_source_bytes_are_rejected (test_c297_hosted_verify.HostedVerifierTests) +Dropping size/hash verification would accept the modified file. ... ok +test_phase_rejects_imported_object_mutation (test_c297_hosted_verify.HostedVerifierTests) +A successful compiler process may not alter a prior input object. ... ok +test_pinned_lean_multiline_axiom_records (test_c297_hosted_verify.HostedVerifierTests) +Actual pinned Lean wraps the unchanged Lifetime axiom arrays. ... ok +test_timeout_preserves_partial_stream_and_receipt (test_c297_hosted_verify.HostedVerifierTests) +Timeout handling must not discard the child output or phase result. ... ok + +---------------------------------------------------------------------- +Ran 10 tests in 0.215s + +OK diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_GREEN.stdout b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_GREEN.stdout new file mode 100644 index 000000000..c363d4ea7 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_GREEN.stdout @@ -0,0 +1,4 @@ +C297 valid-phase: exit=0 timeout=False seconds=0.021915 +C297 deliberate-failure: exit=7 timeout=False seconds=0.024743 +C297 deliberate-object-mutation: exit=0 timeout=False seconds=0.039815 +C297 deliberate-timeout: exit=-15 timeout=True seconds=0.10834 diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_OPTIMIZED.stderr b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_OPTIMIZED.stderr new file mode 100644 index 000000000..0750d2028 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_OPTIMIZED.stderr @@ -0,0 +1,25 @@ +test_actual_coordinate_diagnostic_with_displayed_coercion (test_c297_hosted_verify.HostedVerifierTests) +Run 39418891714 prints the chart coercion as (↑p y), not (p y). ... ok +test_amended_phase_receipt_matches_aggregate (test_c297_hosted_verify.HostedVerifierTests) +Semantic/object metadata must not exist only in the aggregate receipt. ... ok +test_audit_cannot_omit_required_target_or_hide_axiom (test_c297_hosted_verify.HostedVerifierTests) +Count-only validation would accept a substituted target or sorryAx. ... ok +test_build_allows_only_its_own_outputs (test_c297_hosted_verify.HostedVerifierTests) +A build may add its target object, not an unrelated replacement. ... ok +test_failed_phase_receipt_and_exact_streams_survive_abort (test_c297_hosted_verify.HostedVerifierTests) +Raising before persistence would discard the actual failing phase. ... ok +test_fake_negative_or_import_failure_cannot_pass (test_c297_hosted_verify.HostedVerifierTests) +Exit-only or theorem-name-only validation accepts the wrong rejection. ... ok +test_modified_source_bytes_are_rejected (test_c297_hosted_verify.HostedVerifierTests) +Dropping size/hash verification would accept the modified file. ... ok +test_phase_rejects_imported_object_mutation (test_c297_hosted_verify.HostedVerifierTests) +A successful compiler process may not alter a prior input object. ... ok +test_pinned_lean_multiline_axiom_records (test_c297_hosted_verify.HostedVerifierTests) +Actual pinned Lean wraps the unchanged Lifetime axiom arrays. ... ok +test_timeout_preserves_partial_stream_and_receipt (test_c297_hosted_verify.HostedVerifierTests) +Timeout handling must not discard the child output or phase result. ... ok + +---------------------------------------------------------------------- +Ran 10 tests in 0.227s + +OK diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_OPTIMIZED.stdout b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_OPTIMIZED.stdout new file mode 100644 index 000000000..a0dabb7ee --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_OPTIMIZED.stdout @@ -0,0 +1,4 @@ +C297 valid-phase: exit=0 timeout=False seconds=0.025516 +C297 deliberate-failure: exit=7 timeout=False seconds=0.052431 +C297 deliberate-object-mutation: exit=0 timeout=False seconds=0.022206 +C297 deliberate-timeout: exit=-15 timeout=True seconds=0.106616 diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_RED.stderr b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_RED.stderr new file mode 100644 index 000000000..b4771168e --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_RED.stderr @@ -0,0 +1,36 @@ +test_actual_coordinate_diagnostic_with_displayed_coercion (test_c297_hosted_verify.HostedVerifierTests) +Run 39418891714 prints the chart coercion as (↑p y), not (p y). ... ERROR +test_amended_phase_receipt_matches_aggregate (test_c297_hosted_verify.HostedVerifierTests) +Semantic/object metadata must not exist only in the aggregate receipt. ... ok +test_audit_cannot_omit_required_target_or_hide_axiom (test_c297_hosted_verify.HostedVerifierTests) +Count-only validation would accept a substituted target or sorryAx. ... ok +test_build_allows_only_its_own_outputs (test_c297_hosted_verify.HostedVerifierTests) +A build may add its target object, not an unrelated replacement. ... ok +test_failed_phase_receipt_and_exact_streams_survive_abort (test_c297_hosted_verify.HostedVerifierTests) +Raising before persistence would discard the actual failing phase. ... ok +test_fake_negative_or_import_failure_cannot_pass (test_c297_hosted_verify.HostedVerifierTests) +Exit-only or theorem-name-only validation accepts the wrong rejection. ... ok +test_modified_source_bytes_are_rejected (test_c297_hosted_verify.HostedVerifierTests) +Dropping size/hash verification would accept the modified file. ... ok +test_phase_rejects_imported_object_mutation (test_c297_hosted_verify.HostedVerifierTests) +A successful compiler process may not alter a prior input object. ... ok +test_pinned_lean_multiline_axiom_records (test_c297_hosted_verify.HostedVerifierTests) +Actual pinned Lean wraps the unchanged Lifetime axiom arrays. ... ok +test_timeout_preserves_partial_stream_and_receipt (test_c297_hosted_verify.HostedVerifierTests) +Timeout handling must not discard the child output or phase result. ... ok + +====================================================================== +ERROR: test_actual_coordinate_diagnostic_with_displayed_coercion (test_c297_hosted_verify.HostedVerifierTests) +Run 39418891714 prints the chart coercion as (↑p y), not (p y). +---------------------------------------------------------------------- +Traceback (most recent call last): + File "$C297_ROOT/hosted/test_c297_hosted_verify.py", line 114, in test_actual_coordinate_diagnostic_with_displayed_coercion + v.validate_negative('WithoutCoordinateIdentity', 1, actual) + File "$C297_ROOT/hosted/c297_hosted_verify.py", line 216, in validate_negative + raise RuntimeError('negative control did not reject its intended missing premise') +RuntimeError: negative control did not reject its intended missing premise + +---------------------------------------------------------------------- +Ran 10 tests in 0.214s + +FAILED (errors=1) diff --git a/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_RED.stdout b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_RED.stdout new file mode 100644 index 000000000..015ae6680 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/TEST_COERCION_RED.stdout @@ -0,0 +1,4 @@ +C297 valid-phase: exit=0 timeout=False seconds=0.020868 +C297 deliberate-failure: exit=7 timeout=False seconds=0.024343 +C297 deliberate-object-mutation: exit=0 timeout=False seconds=0.037213 +C297 deliberate-timeout: exit=-15 timeout=True seconds=0.112403 diff --git a/frontiers/regular_superlevel_geometry_20261020/development/hosted-run1-WithoutCoordinateIdentity.stdout b/frontiers/regular_superlevel_geometry_20261020/development/hosted-run1-WithoutCoordinateIdentity.stdout new file mode 100644 index 000000000..fcb526253 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/hosted-run1-WithoutCoordinateIdentity.stdout @@ -0,0 +1,6 @@ +/home/runner/work/Math-/Math-/frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutCoordinateIdentity.lean:24:2: error: Type mismatch + TorusRegularSuperlevel.closed_superlevel_basis_of_chart a x p hx +has type + (∀ y ∈ p.source, (↑p y).1 = g y) → (𝓝 x).HasBasis (fun V => V ∈ 𝓝 x ∧ IsPathConnected V) id +but is expected to have type + (𝓝 x).HasBasis (fun V => V ∈ 𝓝 x ∧ IsPathConnected V) id diff --git a/frontiers/regular_superlevel_geometry_20261020/development/hosted-run1-WithoutRegularOrInterior.stdout b/frontiers/regular_superlevel_geometry_20261020/development/hosted-run1-WithoutRegularOrInterior.stdout new file mode 100644 index 000000000..c883a5719 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/development/hosted-run1-WithoutRegularOrInterior.stdout @@ -0,0 +1,6 @@ +/home/runner/work/Math-/Math-/frontiers/regular_superlevel_geometry_20261020/negative-project/WithoutRegularOrInterior.lean:22:2: error: Type mismatch + TorusRegularSuperlevel.closed_superlevel_path_connected_basis hsmooth a x +has type + a < g ↑x ∨ ¬IsCriticalPoint d g ↑x → (𝓝 x).HasBasis (fun V => V ∈ 𝓝 x ∧ IsPathConnected V) id +but is expected to have type + (𝓝 x).HasBasis (fun V => V ∈ 𝓝 x ∧ IsPathConnected V) id diff --git a/frontiers/regular_superlevel_geometry_20261020/reviews/HOSTED_COERCION_AMENDMENT_REVIEW.md b/frontiers/regular_superlevel_geometry_20261020/reviews/HOSTED_COERCION_AMENDMENT_REVIEW.md new file mode 100644 index 000000000..c87c61033 --- /dev/null +++ b/frontiers/regular_superlevel_geometry_20261020/reviews/HOSTED_COERCION_AMENDMENT_REVIEW.md @@ -0,0 +1,86 @@ +# C297 hosted coercion-classifier amendment review + +**`PASS_SCOPED_ENGINEERING_AMENDMENT` — the minimal classifier correction is appropriate.** Run 1 remains **HOLD**; this does not replace the required successful hosted run. + +Actual reviewer: OpenAI Codex `/root/c292_geometry_review`, delegated work for Dylan Roy. This is same-provider, source-exposed nonauthor review, with organizational independence 0 and human review 0. Exposure includes the prior C297 mathematical/source reviews, topology/control advice, the hosted verifier review and multiline-parser finding, and the actual run-1 negative diagnostics. The reviewer did not author this classifier change or its regression test. + +`$C297_ROOT` denotes the C297 working/evidence root without disclosing a machine-specific path. This amendment review supplements the frozen prior hosted engineering review; it does not rewrite that historical review or the run-1 evidence. + +## Actual diagnostic and artifact binding + +I read both actual negative diagnostics and receipts under `$C297_ROOT/hosted-run1/`, and verified their extracted bytes against the corresponding members of `$C297_ROOT/C297_RUN1_39418891714.zip`: + +- ZIP: **323,718 bytes**, SHA-256 `edb500e87ab5c6880a32ffdf3950c186728bec24c8f758d3d9170f091fd81157`. +- `negative-WithoutRegularOrInterior.stdout`: **449 bytes**, SHA-256 `a723a09d113b51625b2f1ea3be658adf97077c1b545b65c63d021ee186efbeae`. +- `negative-WithoutCoordinateIdentity.stdout`: **438 bytes**, SHA-256 `5968ca1e824c98dc0c3871735efa6ea0c451f59d51473eb493cd706e29d707a2`. + +Both are the intended missing-premise type mismatches, with rc 1, no timeout, empty stderr, and unchanged local objects. The precise mismatch in the old classifier was the displayed **`↑p` coercion**: `.1` was already accepted alongside `.fst`. + +The coordinate diagnostic shows the actual invocation + +```text +TorusRegularSuperlevel.closed_superlevel_basis_of_chart a x p hx +``` + +with type + +```text +(∀ y ∈ p.source, (↑p y).1 = g y) → + (𝓝 x).HasBasis (fun V => V ∈ 𝓝 x ∧ IsPathConnected V) id +``` + +where the requested type is the basis proposition itself. The regular-or-interior diagnostic analogously shows the remaining explicit premise + +```text +a < g ↑x ∨ ¬IsCriticalPoint d g ↑x +``` + +before the basis conclusion. Neither diagnostic is a syntax, import, setup, or resource failure. + +The reviewed coordinate receipt is 2,426 bytes, SHA-256 `cb9341f2223afb18b0756f90effaa529ce083e1a5e9204b3bb4b61b8e1ce3436`; the regular-or-interior receipt is 2,470 bytes, SHA-256 `b0652e343a1f50a7dc8510f7439bf00ce0fcd214366997af2882c7770c33327e`. Both receipts, both stdout/stderr pairs, and the aggregate `RESULT.json` matched their actual ZIP-member bytes. + +## Exact source delta + +The only production-code change is: + +```text +\(p y\)\.(?:fst|1)\s*=\s*g y +→ +\(↑?p y\)\.(?:fst|1)\s*=\s*g y +``` + +It accepts the observed spelling without relaxing the required chart, coordinate identity, function, source, invocation, or failure-kind checks. The added regression uses the actual diagnostic form and checks rejection after removing or changing those essential elements. + +I compared the amended verifier and test module with the exact support files retained in the run-1 source snapshot. The verifier difference is the one regex change above. The test difference adds the actual coercion diagnostic and rejection mutations for missing identity, wrong chart, wrong function, missing source condition, unrelated invocation, and an import error. + +Final reviewed identities: + +| Artifact | Bytes | SHA-256 | +|---|---:|---| +| `c297_hosted_verify.py` | 25,485 | `18985d363f3a0b0529e88c9c69dd07c626e6b5f82a251c19c7d820117b7d47c1` | +| `test_c297_hosted_verify.py` | 12,196 | `0d1d8d18a11334364151d16f7640af2730e38f17d8240ddf0244decc2f8376cd` | +| Unchanged `c297-regular-superlevel.yml` | 3,129 | `03b3d8fb4ca95316247b93ad3937ea2d56f0509040c819534873be1bb341eab3` | + +The reviewed staged support files are under `$C297_ROOT/hosted/`. This review concerns this exact amendment; it neither authorizes a change to the frozen Lean sources nor treats the amended classifier as a new proof. + +## Retained engineering control evidence + +I read the retained regression failure and subsequent **10/10 normal and optimized** test results: + +| Retained log under `$C297_ROOT/hosted/` | Bytes | SHA-256 | +|---|---:|---| +| `TEST_COERCION_RED.stderr` | 2,742 | `0045daa87111a04665923f19287703530e31e0ab4f54dc99dcd4c046850863af` | +| `TEST_COERCION_GREEN.stderr` | 1,774 | `08ab1b1edfbc8dad4238f37b4c15fcb733de877108132cf3335c8e4e3f643df2` | +| `TEST_COERCION_OPTIMIZED.stderr` | 1,774 | `10c767efdf08964c67741e1669944bea761fabcb88dd76a6b53beb29dfa8634e` | + +The failing regression reports the actual-diagnostic rejection before the one-line fix. The subsequent normal and optimized results report all ten controls passing. These are the verifier author's engineering executions, not this reviewer's executions and not new Lean runs. + +## Preserved outcome and acceptance boundary + +Run 1's aggregate correctly records `HOLD_NOT_COMPLETED`, lacks `completed_at`, and lacks the second negative's semantic-acceptance flag. Its `RESULT.json` is 45,173 bytes, SHA-256 `55d8cac09bb7a96265de7f3c18bf75ae2aba1ee5d6a3138b96f6f705080e3bc3`. Those records must remain unchanged. The phase-level `PASS` on the coordinate process records the expected exit/object outcome; it is not a completed semantic classification. + +Full artifact acceptance will bind the next hosted run and these amended support identities. It must still establish the exact source bindings, five builds, four standard named-module kernel replays, complete four-module census, both intended missing-premise rejections, and the final source/object stability checks. + +C296-N1 remains with the peer reviewer and source owner. This narrowly reviewed C297 classifier change neither supplies blanket approval of the peer workflow nor duplicates its repair. + +I ran no tests, Lean, or hosted verification and made no remote action. I edited no implementation or Lean source. The only write was this authorized amendment-review record. Same-provider exposed nonauthor review, **org0/human0**. Scientific effect: **NONE**. diff --git a/frontiers/regular_superlevel_geometry_20261020/test_c297_hosted_verify.py b/frontiers/regular_superlevel_geometry_20261020/test_c297_hosted_verify.py index 372ce6d7f..e9bbfc960 100644 --- a/frontiers/regular_superlevel_geometry_20261020/test_c297_hosted_verify.py +++ b/frontiers/regular_superlevel_geometry_20261020/test_c297_hosted_verify.py @@ -100,6 +100,27 @@ def test_fake_negative_or_import_failure_cannot_pass(self): v.validate_negative('WithoutCoordinateIdentity', 1, coordinate.replace('(p y).fst = g y', 'True')) + def test_actual_coordinate_diagnostic_with_displayed_coercion(self): + """Run 39418891714 prints the chart coercion as (↑p y), not (p y).""" + v = self.verifier() + actual = ( + '/home/runner/work/Math-/Math-/frontiers/regular_superlevel_geometry_20261020/' + 'negative-project/WithoutCoordinateIdentity.lean:24:2: error: Type mismatch\n' + ' TorusRegularSuperlevel.closed_superlevel_basis_of_chart a x p hx\n' + 'has type\n' + ' (∀ y ∈ p.source, (↑p y).1 = g y) → (𝓝 x).HasBasis (fun V => V ∈ 𝓝 x ∧ IsPathConnected V) id\n' + 'but is expected to have type\n' + ' (𝓝 x).HasBasis (fun V => V ∈ 𝓝 x ∧ IsPathConnected V) id\n') + v.validate_negative('WithoutCoordinateIdentity', 1, actual) + for bad in (actual.replace('(↑p y).1 = g y', 'True'), + actual.replace('(↑p y).1 = g y', '(↑q y).1 = g y'), + actual.replace('(↑p y).1 = g y', '(↑p y).1 = h y'), + actual.replace('p.source', 'Set.univ'), + actual.replace('closed_superlevel_basis_of_chart a x p hx', 'unrelated a x p hx'), + actual + 'unknown module RegularSuperlevel\n'): + with self.subTest(bad=bad), self.assertRaises(RuntimeError): + v.validate_negative('WithoutCoordinateIdentity', 1, bad) + def test_failed_phase_receipt_and_exact_streams_survive_abort(self): """Raising before persistence would discard the actual failing phase.""" v = self.verifier()