d6g8k5htny-coder · Oct 18, 2026 · Oct 18, 2026 · Oct 18, 2026 · Oct 18, 2026 · Oct 18, 2026
@@ -0,0 +1,71 @@
+name: C293 Morse finite critical (hosted Lean, no scientific promotion)
+'on':
+  pull_request:
+    paths:
+      - 'frontiers/morse_finite_critical_20261018/**'
+      - 'tools/c293_hosted_verify.py'
+      - 'tests/test_c293_hosted_verify.py'
+      - '.github/workflows/c293-morse-finite.yml'
+      - 'formal/lean-toolchain'
+      - 'formal/lakefile.toml'
+      - 'formal/lake-manifest.json'
+      - 'specifications/lean_statements_20261010/Specifications/Lifetime.lean'
+      - 'companions/torus_filtration_20261011/TorusTopology.lean'
+  push:
+    branches: [main]
+    paths:
+      - 'frontiers/morse_finite_critical_20261018/**'
+      - 'tools/c293_hosted_verify.py'
+      - 'tests/test_c293_hosted_verify.py'
+      - '.github/workflows/c293-morse-finite.yml'
+      - 'formal/lean-toolchain'
+      - 'formal/lakefile.toml'
+      - 'formal/lake-manifest.json'
+      - 'specifications/lean_statements_20261010/Specifications/Lifetime.lean'
+      - 'companions/torus_filtration_20261011/TorusTopology.lean'
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: c293-${{ github.event_name == 'pull_request' && github.event.pull_request.number || github.run_id }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+jobs:
+  c293-hosted-formal:
+    name: c293-hosted-formal
+    runs-on: ubuntu-24.04
+    timeout-minutes: 55
+    env:
+      LEAN_NUM_THREADS: '2'
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+          fetch-depth: 1
+      - name: Verify source identities and eight registration engineering tests
+        run: |
+          python3 -B -S tools/c293_hosted_verify.py source
+          python3 -B -S -m unittest discover -s tests -p test_c293_hosted_verify.py -v
+          python3 -B -O -S -m unittest discover -s tests -p test_c293_hosted_verify.py -v
+      - name: Install pinned Lean and retrieve dependency cache
+        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: Build five C293 objects, kernel replay, audit and missing-premise rejection
+        run: |
+          cd formal
+          lake env python3 -B -S ../tools/c293_hosted_verify.py execute
+      - name: Retain exact tested-run C293 outputs including failures
+        if: always()
+        uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9
+        with:
+          name: c293-hosted-${{ github.run_id }}-${{ github.run_attempt }}
+          path: .lake/c293-hosted-evidence/
+          include-hidden-files: true
+          if-no-files-found: warn
+          retention-days: 90
@@ -0,0 +1,37 @@
+# C293 hosted formal replay — engineering-only registration
+
+**Scientific effect: NONE.** This is source-bound, hosted Lean verification of C293's conditional finite-critical-class declaration; it is not acceptance of C292, elder pairing, or the persistence-lifetime law.
+
+## Ownership, source and current gates
+
+Source PR: https://github.com/d6g8k5htny-coder/Math-/pull/482 at exact head 0ea97aff489f9420632b4cee81ad82dbec5fe88e. The stacked CI branch is based on that head; it does not change source modules, source reviews, historical receipts, negative controls, or original evidence.
+
+The existing required math-downstream-gates invokes the original formal-lean.yml, which builds the independent formal/ target. Neither that required job nor the existing torus-filtration.yml companion executes this new C293 declaration. The latter's Claude companion ownership and the separate Sol/elder-registration work remain undisturbed.
+
+The addition is a dedicated C293 workflow named c293-morse-finite.yml. Its c293-hosted-formal job is **not a branch-protection-required context** and is not inserted into formal/gate.py or the required aggregate. Enforcing it as required should follow separately with current gate owners after hosted execution, capacity evidence, source review and readback.
+
+## Hosted invocation and pins
+
+The job uses Lean 4.34.1 and exactly the existing formal Lake project and its nine package pins, including Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612. Python source checks compare all five C293 Lean modules to their published byte counts/SHA-256 values and require exact identity with the canonical Lifetime and TorusTopology upstream files. A mutated control, pin, source or upstream copy fails closed; normal and optimized test modes exercise the guard.
+
+To repeat after installing the formal Lake dependencies, execute from the repository root:
+
+    python3 -B -S tools/c293_hosted_verify.py source
+    python3 -B -S -m unittest discover -s tests -p test_c293_hosted_verify.py -v
+    python3 -B -O -S -m unittest discover -s tests -p test_c293_hosted_verify.py -v
+    cd formal
+    lake env python3 -B -S ../tools/c293_hosted_verify.py execute
+
+The runner verifies tested GitHub commit, repository, run ID and attempt; Lean version; exact installed revisions and clean source; then compiles from new isolated outputs in the order Lifetime, TorusTopology, MorseFiniteCritical, MorseFiniteControls, MorseFiniteAxiomAudit. The three new modules use warnings-as-errors; all builds and the negative control use -j2 -M14000.
+
+**Memory deviation:** The original author receipts use -M4096. Anthropic/Claude's provider-distinct Linux replay, recorded in https://github.com/d6g8k5htny-coder/Math-/pull/482#issuecomment-6246988654 , needed -M14000 for six build/negative invocations. This workflow records the new limit without altering the original receipts.
+
+All five new .olean files must match the published object SHA-256 values. Three named-module leanchecker -v passes, the full 169-declaration (103/38/20/8) standard-only transitive axiom audit, and the exact intended missing-IsMorseDistinct rejection are mandatory. A nonzero result for an unrelated reason is not a pass.
+
+The 90-day workflow artifact contains phase stdout/stderr, digests and exact-run RESULT.json. Hosted standard named-module replay is **not** a hosted leanchecker --fresh of the entire import closure. External --fresh is a separate evidence record; neither implies institutional mathematical acceptance.
+
+## Source review and protected integration
+
+This change should receive review of its *CI verifier*, not substitute for the source author's C293 mathematical review. Inspect the new hosted c293-hosted-formal job and its real logs on the exact tested PR merge; do not reclassify old green checks. Keep this implementation stacked until C293 source PR #482 receives its own legitimate integration disposition. Do not automatically merge into the source author's draft branch, alter rulesets, waive reviewer independence or set a scientific status. Before any later merge, re-check ownership, base/head, source hashes, reviews, gates and the protected merge process.
+
+C293 does not close critical-level local path connectivity or path attainment, the full C292 adapter, almost-sure Morse, elder pairing, exhaustive once-counting, all-small-bars converse, regional collisions or stochastic lifetime transfer.
@@ -0,0 +1,38 @@
+# C293 author notes: finite literal quotient critical set
+
+## Scope and source relationship
+
+The assigned deliverable formalizes the finite-critical-set dependency already proved conventionally in C292, Section 4. It does not reopen or replace that conventional proof. The public endpoint is the finiteness of the full image of all `UniversalLaw.Spec.Lifetime.IsCriticalPoint` points under the actual C263 `TorusFiltration.torus_proj`.
+
+The implementation imports only the supplied, source-verified `Lifetime.lean` and `TorusTopology.lean`; these import the pinned Mathlib. The literal Euclidean space, iterated-Frechet Hessian, inertia encoding, lattice scale, periodicity, and quotient remain unchanged. No product-of-circles torus is substituted.
+
+The primary theorem `TorusMorseFinite.quotientCriticalSet_finite` assumes literal `IsSmooth`, `IsLPeriodic`, and `IsMorseDistinct`, with `L > 0`. Its core theorem only uses the nondegeneracy-at-critical-points conjunct of the Morse-distinct predicate. No finite event list, finite critical set, inverse certificate, closed-level path, elder pairing, or barcode conclusion is a premise.
+
+## Proof structure
+
+1. Identify the literal `iteratedFDeriv` Hessian with `fderiv` of `fderiv`, and derive its symmetry from real `C^2` smoothness.
+2. For a kernel vector `z = v + w` in the complementary inertia subspaces, symmetry and the kernel equation give `B(v,v) = B(w,w)`. The opposite definite signs force `v = w = 0`. Cross terms are retained; the subspaces are not assumed Hessian-orthogonal.
+3. Use the real Riesz equivalence and finite-dimensional injective-endomorphism equivalence to turn the derivative of `fderiv` into an actual continuous linear equivalence. Apply Mathlib's inverse function theorem to derive an isolating open neighborhood of each literal critical point.
+4. Derive periodicity of `fderiv` by differentiating the exact lattice-translation identity. Construct the continuous dual-valued derivative on C263's quotient using `Quotient.lift` and prove the literal pullback identity.
+5. Identify the quotient critical set with the zero set of this descended derivative. It is closed. The projection is open because the supplied C263 theorem constructs a covering map. Images of the Euclidean isolating neighborhoods isolate quotient critical points.
+6. Apply actual quotient compactness and Mathlib's compact-discrete finiteness theorem.
+
+The deterministic proof works for every natural dimension. C292's application retains its own `d >= 1` scope. There is no coefficient-field or limit-order change: the present theorem is real scalar deterministic geometry and has no asymptotic parameter.
+
+## Deliberate mathematical boundary
+
+This unit proves no Morse normal form and no closed-superlevel local path connectivity. Those remain substantive imports needed by the larger C292 closed-level attainment argument. Finiteness of quotient critical points is not a finite-event or elder-registration theorem, not a proof of all small bars or exhaustive once-counting, and not a regional shrinking-collision estimate. It does not modify an owner's separate elder-registration scope.
+
+## Build and review status
+
+Initial source written at approximately 2026-10-18 02:12 UTC. Both exact dependency modules compiled successfully with no stdout/stderr: `Lifetime.lean` in 186.78 seconds and `TorusTopology.lean` in 169.07 seconds, with unchanged input hashes. These builds were launched by the parent and their terminal receipts were read by the author.
+
+The complete first author attempt compiled successfully in 135.75 seconds, exit code 0, no timeout, source unchanged. Its source SHA-256 is `514445e386599258472310fdab555006a206fba9c65ca864d4a7dc103cb5998c`; the exact source is retained as `project/AuthorProbeAttempt001.lean`. Receipt: `runs/20261018T021538Z-MorseFiniteCritical-092f8343/RECEIPT.json`. It emitted four warnings for deprecated `ContinuousLinearMap.add_apply` / `ContinuousLinearMap.zero_apply` aliases, with no errors.
+
+The cleaned candidate changes only those four aliases to `add_apply` / `zero_apply`; no theorem statement or proof structure changes. Its source SHA-256 is `95a660134eda49eecfe6181884bd23b4e4ca210e228d2463de29e5f821df047b`, 9,445 bytes, 223 lines. The exact source is also retained as `project/AuthorProbeAttempt002.lean`. The targeted cleaned-source run is `runs/20261018T022037Z-MorseFiniteCritical-67cf4c01`. It completed at 2026-10-18 02:22:53 UTC in 135.41 seconds, exit code 0, no timeout, source unchanged, with empty stdout and stderr. The resulting `MorseFiniteCritical.olean` SHA-256 is `34ff2a9ed529609dd48a22204b8eacc66eeb943805e2d6e8dee4481cde8ef4e2`.
+
+The author module is frozen at that cleaned-source hash for substantive review and parent final verification. Both author attempts succeeded; the first attempt's warnings are preserved rather than suppressed or discarded. A source scan found no `sorry`, `admit`, `axiom`, or `unsafe` declaration in the author module. This scan is not an axiom audit of the imported proof dependencies.
+
+All author runs use the assigned bounded serial `run_lean.py` with Lean 4.34.1, two threads, 4096 MiB memory limit, 240-second timeout, and the supplied pinned dependency cache. No shared source or dependency cache is modified. Run receipts and source snapshots remain available. Parent final frozen-artifact verification, kernel/axiom audit, and substantive review are separate gates.
+
+The author and assigned reviewer are same-provider and source-exposed. Neither source inspection nor author compilation constitutes independent scientific acceptance.
@@ -0,0 +1,65 @@
+{
+  "started_utc": "2026-10-18T02:57:21.689807+00:00",
+  "inventory_sha256": "f1a429935146b4e406e9ba8cc9ff8b84f7d40c22cc4fea74920dfc013c4911de",
+  "phases": [
+    {
+      "kind": "build",
+      "module": "Lifetime",
+      "started_utc": "2026-10-18T02:57:21.689836+00:00",
+      "ended_utc": "2026-10-18T02:59:03.224627+00:00",
+      "returncode": 0
+    },
+    {
+      "kind": "build",
+      "module": "TorusTopology",
+      "started_utc": "2026-10-18T02:59:03.224669+00:00",
+      "ended_utc": "2026-10-18T03:00:43.914208+00:00",
+      "returncode": 0
+    },
+    {
+      "kind": "build",
+      "module": "MorseFiniteCritical",
+      "started_utc": "2026-10-18T03:00:43.914248+00:00",
+      "ended_utc": "2026-10-18T03:02:23.617988+00:00",
+      "returncode": 0
+    },
+    {
+      "kind": "build",
+      "module": "MorseFiniteControls",
+      "started_utc": "2026-10-18T03:02:23.618032+00:00",
+      "ended_utc": "2026-10-18T03:04:11.727630+00:00",
+      "returncode": 0
+    },
+    {
+      "kind": "build",
+      "module": "MorseFiniteAxiomAudit",
+      "started_utc": "2026-10-18T03:04:11.727680+00:00",
+      "ended_utc": "2026-10-18T03:07:05.596139+00:00",
+      "returncode": 0
+    },
+    {
+      "kind": "kernel",
+      "module": "MorseFiniteCritical",
+      "started_utc": "2026-10-18T03:07:05.596193+00:00",
+      "ended_utc": "2026-10-18T03:08:32.127951+00:00",
+      "returncode": 0
+    },
+    {
+      "kind": "kernel",
+      "module": "MorseFiniteControls",
+      "started_utc": "2026-10-18T03:08:32.127998+00:00",
+      "ended_utc": "2026-10-18T03:10:00.355556+00:00",
+      "returncode": 0
+    },
+    {
+      "kind": "kernel",
+      "module": "MorseFiniteAxiomAudit",
+      "started_utc": "2026-10-18T03:10:00.355596+00:00",
+      "ended_utc": "2026-10-18T03:11:29.812864+00:00",
+      "returncode": 0
+    }
+  ],
+  "scientific_effect": "NONE",
+  "status": "PASS_FROZEN_BUILD_AND_STANDARD_KERNEL_REPLAY",
+  "ended_utc": "2026-10-18T03:11:29.812907+00:00"
+}
@@ -0,0 +1,6 @@
+{
+  "started_utc": "2026-10-18T02:57:21.689419+00:00",
+  "inventory_sha256": "f1a429935146b4e406e9ba8cc9ff8b84f7d40c22cc4fea74920dfc013c4911de",
+  "driver_sha256": "8cb8a75b384c0c84f1a000f217616a3d99710b34bf2e04237b65f220ff9302ce",
+  "scientific_effect": "NONE"
+}
@@ -0,0 +1,69 @@
+{
+  "frozen_utc": "2026-10-18T02:56:53.456259+00:00",
+  "prepare_start_record": "$C293_ROOT/final-prepare-attempts/2026-10-18T025648.570677_0000-4fa2f46bd57a42d5818b82dc46914892.json",
+  "prepare_start_sha256": "0b9a6dea32234c956e08fbdbc167c9e04a4615c9e5fe4b9cca875f404646f91d",
+  "prior_legacy_start": {
+    "path": "$C293_ROOT/FINAL_PREPARE_START.json",
+    "sha256": "9f39ca7a8c6ff0ef0a1fe37830adfe6955015c6cfca50c8a74c5ee1f3ef8add1"
+  },
+  "sources": [
+    {
+      "name": "Lifetime.lean",
+      "sha256": "90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6",
+      "bytes": 51383
+    },
+    {
+      "name": "TorusTopology.lean",
+      "sha256": "ddb145b3f791c181d4f2a51e54e711937297bd6476ba55bcd5252b7ddb57cfe1",
+      "bytes": 12257
+    },
+    {
+      "name": "MorseFiniteCritical.lean",
+      "sha256": "95a660134eda49eecfe6181884bd23b4e4ca210e228d2463de29e5f821df047b",
+      "bytes": 9445
+    },
+    {
+      "name": "MorseFiniteControls.lean",
+      "sha256": "e6171c949ec60a3aea21a8cc028180e16c82e4946a232107d9e82bf8018cdac1",
+      "bytes": 2843
+    },
+    {
+      "name": "MorseFiniteAxiomAudit.lean",
+      "sha256": "326a1cab271bf46a1c7db750ee1565e08dc4856c62e0abce3f5c9f90d923ce9d",
+      "bytes": 3025
+    }
+  ],
+  "build_order": [
+    "Lifetime",
+    "TorusTopology",
+    "MorseFiniteCritical",
+    "MorseFiniteControls",
+    "MorseFiniteAxiomAudit"
+  ],
+  "local_imports": {
+    "Lifetime": [],
+    "TorusTopology": [],
+    "MorseFiniteCritical": [
+      "Lifetime",
+      "TorusTopology"
+    ],
+    "MorseFiniteControls": [
+      "Lifetime"
+    ],
+    "MorseFiniteAxiomAudit": [
+      "MorseFiniteCritical",
+      "MorseFiniteControls"
+    ]
+  },
+  "new_modules": [
+    "MorseFiniteCritical",
+    "MorseFiniteControls",
+    "MorseFiniteAxiomAudit"
+  ],
+  "runner_sha256": "e9b7bd0caa19889e2ba0974c788e13a573645fd3c0839890eee41bbf15831b23",
+  "preparer_sha256": "72bbe39334fa2a7b09d621f81f6211e9a4019804b949f4ea2576e1c4f2927451",
+  "dependency_artifact_inventory_sha256": "4e35e91a0b6f334eb6ad41e586b9704189e7063722d9c2e5f6a87f0839af0d21",
+  "c291_inventory_sha256": "b78b6e0f99bd38c633ae2677c55698363b1290e6d4318e505991c8df259ae2e3",
+  "scientific_effect": "NONE",
+  "execution_provenance": "LOCAL; no hosted qualification"
+}