d6g8k5htny-coder · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026
@@ -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
@@ -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"
+    }
+  }
+}
@@ -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.
@@ -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.