initial

Author: denisecase

.github/workflows/ci.yml

@@ -14,16 +14,3 @@ jobs:
     steps:
       - uses: actions/checkout@v6 # OBS: v6 current as of Dec 2025
       - uses: leanprover/lean-action@v1 # OBS: v1 current as of Dec 2025
-
-      # REQ.CI.DEPENDENCIES
-      # WHY:
-      #   lake-manifest.json is generated and not committed.
-      #   CI must regenerate it deterministically.
-      - name: Lake update
-        run: lake update
-
-      # REQ.CI.BUILD
-      # WHY:
-      #   Proofs are the deliverable.
-      - name: Lake build
-        run: lake build

.gitignore

@@ -1,2 +1 @@
 /.lake
-lake-manifest.json

lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "NeutralSubstrate",
+ "lakeDir": ".lake"}