Skip to content

C299-C7 replacement preparation (agent 8): candidate7 source + manifest/workflow digest rebind #496

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
d6g8k5htny-coder wants to merge 1 commit into
base: codex/c299-critical-ridge-20261020
Choose a base branch
from
Draft

C299-C7 replacement preparation (agent 8): candidate7 source + manifest/workflow digest rebind #496

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/c299-critical-ridge.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ jobs:
env:
LEAN_NUM_THREADS: '2'
# Exact frozen five-module and two-control source manifest.
C299_MANIFEST_SHA256: '13deb8d5c9a2c50ee419c15bcefaabb4855be16cedf060400fbbf5775a616519'
C299_MANIFEST_SHA256: 'f0a2d85dc30f8561fcdd6af3b6eccc00f6d3bb89e7022f64080ffef36c5830ab'
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
with:
Expand Down
4 changes: 2 additions & 2 deletions frontiers/critical_ridge_20261020/HOSTED_SOURCE_MANIFEST.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@
"sha256": "ad204aee211aa3074621f56eeaf8e1a3f3a522b7c7cbe2bbdd67f3759833feb9"
},
"project/CriticalRidge.lean": {
"bytes": 9053,
"sha256": "9ff65416927182f6dad06646f04821b3af6bdd131740d93bf229354a81e19c38"
"bytes": 9047,
"sha256": "4a4d219ac7d38e76dd18ce1f8e42fb877553498e0da1aa80d0c069fb1c59c3a3"
},
"project/CriticalRidgeAxiomAudit.lean": {
"bytes": 2728,
Expand Down
6 changes: 3 additions & 3 deletions frontiers/critical_ridge_20261020/project/CriticalRidge.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,10 +126,10 @@ theorem negativePartialGradient_hasFDerivAt (f : E d → ℝ) (p : E d)
have hcomp := hDp'.comp (0 : E d × V) hadd
change HasFDerivAt (fun q : E d × V =>
(fderiv ℝ f (p + ridgeAddition V q)).comp V.subtypeL) _ _
convert! hcomp.clm_comp (hasFDerivAt_const V.subtypeL (0 : E d × V)) using 1 <;>
convert! hcomp.clm_comp (hasFDerivAt_const V.subtypeL (0 : E d × V)) using 1 ;
first
| rfl
| (simp only [ContinuousLinearMap.comp_zero, zero_add] <;>
| (simp only [ContinuousLinearMap.comp_zero, zero_add] ;
(apply ContinuousLinearMap.ext
intro q
apply ContinuousLinearMap.ext
Expand Down Expand Up @@ -199,7 +199,7 @@ theorem exists_negative_partial_gradient_ridge
(f' := (ContinuousLinearMap.id ℝ (E d)).prod (fderiv ℝ r 0))
(0 : E d)
(by
convert! hDG using 1 <;>
convert! hDG using 1 ;
first
| rfl
| exact Prod.ext rfl hr0)
Expand Down
Loading