d6g8k5htny-coder · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026
@@ -0,0 +1,71 @@
+name: C299 critical ridge (hosted Lean, no scientific promotion)
+'on':
+  pull_request:
+    paths:
+      - 'frontiers/critical_ridge_20261020/**'
+      - '.github/workflows/c299-critical-ridge.yml'
+      - 'formal/lean-toolchain'
+      - 'formal/lakefile.toml'
+      - 'formal/lake-manifest.json'
+      - 'specifications/lean_statements_20261010/Specifications/Lifetime.lean'
+  push:
+    branches: [main]
+    paths:
+      - 'frontiers/critical_ridge_20261020/**'
+      - '.github/workflows/c299-critical-ridge.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: c299-${{ github.event_name == 'pull_request' && github.event.pull_request.number || github.run_id }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+jobs:
+  c299-hosted-formal:
+    name: c299-hosted-formal
+    runs-on: ubuntu-24.04
+    timeout-minutes: 205
+    env:
+      LEAN_NUM_THREADS: '2'
+      # Exact frozen five-module and two-control source manifest.
+      C299_MANIFEST_SHA256: '13deb8d5c9a2c50ee419c15bcefaabb4855be16cedf060400fbbf5775a616519'
+    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/critical_ridge_20261020/c299_hosted_verify.py source --manifest-sha256 "$C299_MANIFEST_SHA256"
+          python3 -B -S -m unittest discover -s frontiers/critical_ridge_20261020 -p test_c299_hosted_verify.py -v
+          python3 -B -O -S -m unittest discover -s frontiers/critical_ridge_20261020 -p test_c299_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/critical_ridge_20261020/c299_hosted_verify.py execute --manifest-sha256 "$C299_MANIFEST_SHA256"
+      - name: Retain exact C299 tested-run sources, objects, streams and failure receipts
+        if: always()
+        timeout-minutes: 5
+        uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9
+        with:
+          name: c299-hosted-${{ github.run_id }}-${{ github.run_attempt }}
+          path: .lake/c299-hosted-evidence/
+          include-hidden-files: true
+          if-no-files-found: warn
+          retention-days: 90
@@ -0,0 +1,15 @@
+# C299 declared execution contract
+
+Declared by OpenAI Codex /root before initial hosted execution, under the verified C299 claim6e894b1f-d783-4ea0-adae-597e116b239a. This record authorizes only the dedicated additive draft-PR workflow and its bounded local phases. It does not authorize merging, deployment or scientific promotion.
+
+Inputs: exact HOSTED_SOURCE_MANIFEST.json digest inserted into the workflow; five named Lean sources and two negative fixtures; exact versioned verifier, tests, workflow and existing formal configuration. Native prepublication identity records bind these bytes before dispatch. The checkout, actual PR head/base, tested commit/tree, run/attempt/job, all nine package revisions, selected runtime binaries and exact source snapshots are retained by the runner and separately read back.
+
+Commands: source preflight via python3 -B -S; inert verifier tests via python3 -B -S -m unittest and python3 -B -O -S -m unittest; pinned lean-action cache setup with build/test/lint disabled; then lake env python3 -B -S ../frontiers/critical_ridge_20261020/c299_hosted_verify.py execute --manifest-sha256 <exact digest>. The driver resolves the actual runtime through lean --print-prefix and --version before invoking the measured binary.
+
+Formal sequence: five fresh builds, dependency order Lifetime, TorusTopology, MorseFiniteCritical, CriticalRidge, CriticalRidgeAxiomAudit; four standard named-module leanchecker replays excluding Lifetime; two actual omitted-premise fixtures WithoutCriticality and WithoutNegativeDefiniteness. Each formal phase uses a900-second cap; runtime probes30seconds; build/negative Lean commands use2threads and -M14000. The empty local output directory is prepended to the Lake environment. Build success requires rc0 and exact intended new objects; each negative requires rc1 plus the source-bound semantic diagnostic. Any unresolved classifier qualification keeps aggregate HOLD even if all commands executed.
+
+The dedicated job's205-minute platform cap is a conservative hard upper bound inherited from the reviewed pattern, not a claimed expected duration. The live cooperative claim must be renewed or the work handed off before expiry. No automatic native or hosted retry. Changed source/support inputs or unresolved actual failures are the only reasons for a further complete sequence.
+
+Before every process the exact command is determined from the source-bound driver; complete raw stdout/stderr and terminal receipt are saved, including failures/timeouts. The actual run preserves individual and aggregate receipts, before/after source/package/runtime/object identities, complete census and expected-negative flags. Artifacts upload even on failure. Missing or cancelled upload is HOLD, never inferred success. Final native/remote byte and hosted-artifact verification and substantive nonauthor review remain necessary.
+
+The native author candidate1 attempt is separately declared and uses historical byte-verified C293 objects for development; it is not the hosted fresh local-module sequence. Its timeout or import stall cannot count as a mathematical result. No full imported-library clean replay is claimed.
@@ -0,0 +1,48 @@
+{
+  "files": {
+    "negative-project/WithoutCriticality.lean": {
+      "bytes": 944,
+      "sha256": "6ebc44de843b951c312add4848962d76c4788cc10bdacf17002eb69fd370f1d2"
+    },
+    "negative-project/WithoutNegativeDefiniteness.lean": {
+      "bytes": 872,
+      "sha256": "ad204aee211aa3074621f56eeaf8e1a3f3a522b7c7cbe2bbdd67f3759833feb9"
+    },
+    "project/CriticalRidge.lean": {
+      "bytes": 9053,
+      "sha256": "9ff65416927182f6dad06646f04821b3af6bdd131740d93bf229354a81e19c38"
+    },
+    "project/CriticalRidgeAxiomAudit.lean": {
+      "bytes": 2728,
+      "sha256": "cff55f5b7721a621530ae1020b81e6cc89ce5c405396145e1ca5d3cfba4b2fb7"
+    },
+    "project/Lifetime.lean": {
+      "bytes": 51383,
+      "sha256": "90f4892608e953ecc696bb32ea159d1c178ceb8a1c6edfd11acfceb14af462c6"
+    },
+    "project/MorseFiniteCritical.lean": {
+      "bytes": 9445,
+      "sha256": "95a660134eda49eecfe6181884bd23b4e4ca210e228d2463de29e5f821df047b"
+    },
+    "project/TorusTopology.lean": {
+      "bytes": 12257,
+      "sha256": "ddb145b3f791c181d4f2a51e54e711937297bd6476ba55bcd5252b7ddb57cfe1"
+    }
+  },
+  "schema_version": 1,
+  "scientific_effect": "NONE",
+  "source_origins": {
+    "Lifetime": {
+      "commit": "7af365e8c8db1ae0275d4efe08a70a678f153ca2",
+      "path": "frontiers/critical_level_attainment_20261020/final-project/Lifetime.lean"
+    },
+    "MorseFiniteCritical": {
+      "commit": "7af365e8c8db1ae0275d4efe08a70a678f153ca2",
+      "path": "frontiers/critical_level_attainment_20261020/final-project/MorseFiniteCritical.lean"
+    },
+    "TorusTopology": {
+      "commit": "7af365e8c8db1ae0275d4efe08a70a678f153ca2",
+      "path": "frontiers/critical_level_attainment_20261020/final-project/TorusTopology.lean"
+    }
+  }
+}
@@ -0,0 +1,29 @@
+# Actual negative partial-gradient ridge (C299)
+
+This finite formal unit constructs one local correction `r : E d → V` from the literal `Lifetime.IsSmooth`, criticality at `p`, and strict negativity of the literal Hessian on every nonzero vector of the actual submodule `V`. The selected function has value zero and C2 regularity at zero; on one common neighborhood, the derivative of `f` at `p+w+r(w)` vanishes on every vector of V; its derivative satisfies `H(w+Dr(0)w,z)=0`.
+
+The parameter w is ambient. Restriction to a positive complement is later work; no orthogonality premise, supplied ridge, inverse certificate, Morse chart, desired local path connectivity or finite event list is an input. The zero subspace is included.
+
+The source uses the actual restricted Hessian block, proves its invertibility by strict negativity and finite-dimensional Riesz duality, and applies pinned Mathlib's smooth product implicit-function theorem. C293's literal-Hessian identity is consumed unchanged.
+
+Development status at first publication: source review performed, native import attempt retained, hosted elaboration and final formal verification pending. An execution report must bind the actual revision; this document does not claim compilation or theorem acceptance.
+
+## Provenance and verification boundaries
+
+Upstream sources are byte-identical to Math- commit `7af365e8c8db1ae0275d4efe08a70a678f153ca2`, paths `frontiers/critical_level_attainment_20261020/final-project/{Lifetime,TorusTopology,MorseFiniteCritical}.lean`. The source manifest binds all five modules and two intentionally ill-typed controls. Lean4.34.1 and Mathlib `d13f23b723b8a846827a245b89c10fc7d3f11612` are pinned by the existing formal environment.
+
+The dedicated workflow builds all five local modules into an empty output directory, standard-kernel checks the four non-Lifetime modules, and audits every declaration originating in all four proof/input modules, including private/generated constants. The audit module itself is built and kernel checked, but is not a fifth imported-origin census. Permitted axioms are only propext, Classical.choice, Quot.sound. The nine new public declarations are required targets within the complete census, not its denominator. The complete target list also includes four consumed source interfaces.
+
+Two omitted-premise controls target criticality and negative definiteness. A source-bound expected type-mismatch diagnostic is required; syntax/import/resource failures do not count. Initial diagnostic qualification remains pending until real compiler output is reviewed. Standard named-module checks do not replay or rebuild the entire imported Mathlib closure. Existing dependency objects may be cached; every local proof/input object in this workflow is freshly built. Tests and model agreement do not establish scientific acceptance.
+
+Actual principal: Dylan Roy. Actual source author: OpenAI Codex delegated agent `/root/adapter_feasibility_c292`; coordinator and delivery executor: `/root`, chat `01a0bbb5-2fcb-77f0-b78b-4d220ddd7ab2`; verification engineering author: `/root/c297_hosted_verifier`; fresh source-exposed nonauthor reviewer: `/root/c299_nonauthor_review`. Same provider, organizational independence0, blind0, human0. No human review by Dylan is claimed. Scientific effect NONE.
+
+## Remaining work
+
+Reduced-Hessian positivity, uniform signs and fiber concavity, actual tube paths, a cofinal path-connected neighborhood basis, Euclidean all-point assembly, actual quotient-superlevel transport, and C294's hclosedLPC discharge remain OPEN. Actual finite ordinary bars, elder pairing versus adjacency, once-counting, field-first sampling, all-small-bars converses and regional shrinking collisions remain separate OPEN obligations. A global factorial bound does not settle the regional collision node.
+
+Canonical coordination: Math- PR487 comment6292314595; R17 cooperative claim6e894b1f-d783-4ea0-adae-597e116b239a. Historical sources and other agents' claims remain unchanged. No merge, Ready transition or scientific promotion is part of this delivery.
+
+Governing onboarding sources read for this delivery: [15 October owner mandate](https://github.com/d6g8k5htny-coder/main/blob/b665307520948308a53d190d7341bf301df3b3a2/governance/OWNER_MANDATE_20261015.md) and [standing delegation](https://github.com/d6g8k5htny-coder/main/blob/b665307520948308a53d190d7341bf301df3b3a2/governance/OP-AUTONOMY-20260923-v2.1.md). The current scoped instructions and explicit stops still control. Linking these records establishes availability, not a future recipient's acknowledgement.
+
+Source custody update before hosted execution: the source author's additive correction [6292292150](https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6292292150) now supplies the literal reviewed6961-byte proposal, including both terminal LFs. Its raw bytes match SHA25696a13c7e14e781220915e927caa34ba9ca94e26bd12bb7d53e7459b759c9b141. The original shorter payload and explicit reconstruction history remain preserved; the mathematical version did not change.
@@ -0,0 +1,32 @@
+[
+  {
+    "path": "sources/ridge-UNREVIEWED_RIDGE_ROUTE_V1.md",
+    "bytes": 6961,
+    "sha256": "96a13c7e14e781220915e927caa34ba9ca94e26bd12bb7d53e7459b759c9b141",
+    "source": "https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6292079965",
+    "reconstruction": "append one LF",
+    "direct_fenced_bytes": 6960,
+    "direct_fenced_sha256": "6d9e532505307c5f115701b693046d8ebba6fea913a07f43fd8ecee6e3516558",
+    "raw_fenced_equality": false
+  },
+  {
+    "path": "sources/ridge-NONAUTHOR_REVIEW.md",
+    "bytes": 20646,
+    "sha256": "de928866de9d077a980bc9c42744bfe557c2b6ff7c16b6c840449f4b21542657",
+    "source": "https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6292079965",
+    "reconstruction": "direct fenced bytes",
+    "direct_fenced_bytes": 20646,
+    "direct_fenced_sha256": "de928866de9d077a980bc9c42744bfe557c2b6ff7c16b6c840449f4b21542657",
+    "raw_fenced_equality": true
+  },
+  {
+    "path": "sources/api-API_AUDIT_REPORT.md",
+    "bytes": 17303,
+    "sha256": "1cc33f6368c628702dd447e1b20d8506deaf1b6132712a2feb13aaee6a02c4ae",
+    "source": "https://github.com/d6g8k5htny-coder/Math-/pull/487#issuecomment-6292239804",
+    "reconstruction": "direct fenced bytes",
+    "direct_fenced_bytes": 17303,
+    "direct_fenced_sha256": "1cc33f6368c628702dd447e1b20d8506deaf1b6132712a2feb13aaee6a02c4ae",
+    "raw_fenced_equality": true
+  }
+]