Skip to content

Commit 332fe70

Browse files
Xinze-Li-MoqianXinze-Li-Moqian
committed
Sync SORRY_CATALOG.md + CI EXPECTED to the actual count of 33
Pre-sync state had three numbers disagreeing: summary table said 20, sub-tables enumerated 28, CI workflow hardcoded `EXPECTED=32`, while the real count is 33. CI therefore failed on every push. Rewrites the catalog from a fresh enumeration of the 33 public sorrys (Algebraic + Tensor + Riemannian + GeometricMeasureTheory; Regularity is gitignored and tracked locally). Scope expanded to include Algebraic and Tensor, which were missing from the previous catalog but counted by CI's grep. Classifications: - 22 PRE-PAPER (concrete closure path: Mathlib API to extend or framework self-build to perform) - 11 CITED-BLACK-BOX (named theorem from literature, body delegated to citation): Maggi 2012 isoperimetric chapters (×9), Allard 1972 rectifiability, Petersen Bochner-Weitzenboeck Bumps `.github/workflows/ci.yml` EXPECTED constant 32 -> 33 so CI matches catalog. Adds a closing note documenting the maintenance contract for adding/closing future sorrys.
1 parent 26410c4 commit 332fe70

2 files changed

Lines changed: 86 additions & 73 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ jobs:
2222
--include="*.lean" \
2323
OpenGALib \
2424
2>/dev/null | wc -l | tr -d ' ')
25-
EXPECTED=32
25+
EXPECTED=33
2626
if [ "$ACTUAL" -ne "$EXPECTED" ]; then
2727
echo "::error::Sorry count drift: expected $EXPECTED, found $ACTUAL"
2828
echo "If the change is intentional, update docs/SORRY_CATALOG.md (and the EXPECTED constant in this workflow)."

‎docs/SORRY_CATALOG.md‎

Lines changed: 85 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -1,88 +1,101 @@
11
# Sorry Catalog
22

3-
Central registry of `sorry` occurrences in OpenGA. Every sorry carries a
4-
classification + repair plan. CI snapshots the count; new sorry additions
5-
require updating this file.
3+
Central registry of `sorry` occurrences in OpenGALib. Every sorry carries a
4+
classification and (for PRE-PAPER) a closure path. CI snapshots the total
5+
count; new sorry additions require updating this file.
6+
7+
## Scope
8+
9+
This catalog covers the **public library content**: `Algebraic`, `Tensor`,
10+
`Riemannian`, `GeometricMeasureTheory`. `Regularity/` is gitignored
11+
(paper-specific consumer) and tracked locally; its sorrys are not in the
12+
public count.
613

714
## Classification
815

9-
* **PRE-PAPER** — gap in Mathlib API or framework primitive; closure path
10-
is framework self-build or Mathlib upstream.
16+
* **PRE-PAPER** — gap in Mathlib API or framework primitive; closure path is
17+
framework self-build or Mathlib upstream.
1118
* **CITED-BLACK-BOX** — theorem quoted from a paper, body never proven in
12-
the framework.
13-
* **PAPER-INTERNAL** — proof obligation owned by an application paper, not
14-
the library.
15-
* **CONJECTURAL** — open mathematics.
19+
the framework. The named theorem is the value; the proof is delegated to
20+
the citation.
1621

1722
## Total counts
1823

19-
| Module | PRE-PAPER | CITED-BLACK-BOX | PAPER-INTERNAL | CONJECTURAL | Total |
20-
|--------|-----------|------------------|----------------|-------------|-------|
21-
| Riemannian | 4 | 0 | 0 | 0 | 4 |
22-
| GeometricMeasureTheory | 5 | 9 | 0 | 0 | 14 |
23-
| Regularity | 0 | 2 | 0 | 0 | 2 |
24-
| **Total** | **9** | **11** | **0** | **0** | **20** |
25-
26-
(Bridge investment final closure: Riemannian 9 → 3. The 6 closed sorrys: full
27-
`leviCivitaConnection_exists` smoothness clause + `koszulCovDeriv_const_smoothAt`
28-
+ `koszulCotangentCLM_smoothAt` + 3 associated Curvature smoothness witnesses.
29-
Zero `sorryAx` in `leviCivitaConnection_exists` axiom dependency chain. Phase
30-
1.6 invariant "zero existence axioms in Riemannian package" preserved with
31-
strengthened guarantee: smoothness clause is now real-proven, not bypassed
32-
via PRE-PAPER sorry.)
33-
34-
## Riemannian (10)
35-
36-
| File:line | Identifier | Classification | Repair plan |
37-
|-----------|-----------|---------------|-------------|
38-
| `Curvature.lean:~138` | `ricciTraceMap.map_add'` smoothness witness 1 | PRE-PAPER | `TangentSmoothAt (fun y ↦ covDeriv (const z₁) Y y) x`. Repair: framework `ContMDiffCovariantDerivativeOn` instance for `leviCivitaConnection` (lifts smoothness of input sections to smoothness of `covDeriv` output as a tangent vector field). Linearity proof skeleton is closed; only smoothness witness remains. |
39-
| `Curvature.lean:~143` | `ricciTraceMap.map_add'` smoothness witness 2 | PRE-PAPER | Same as above (z₂ branch). |
40-
| `Curvature.lean:~205` | `ricciTraceMap.map_smul'` smoothness witness | PRE-PAPER | Same as above (single-branch smul case). |
41-
| `Curvature.lean:~256` | `riemannCurvature_inner_diagonal_zero` | PRE-PAPER | Skew-symmetry of $R(X,Y)$ as endomorphism, $\langle R(X,Y) Z, Z\rangle_g = 0$. Closure path via metric-compat 4× + manifold scalar Hessian-Lie (`mfderiv_iterate_sub_eq_mlieBracket_apply`, **now closed**). Outline laid out in proof body. |
42-
| `Curvature.lean:~287` | `ricci_symm` | PRE-PAPER | Symmetry of Ricci. Closure path: trace-via-OnB + Bianchi I (closed) + first-arg antisymm (closed) + diagonal-zero (above). Requires a $g$-orthonormal basis (framework self-build, see `metricOrthonormalBasis` repair plan). |
43-
| `Curvature.lean:~318` | `ricciFormAt.toFun.map_add'` | PRE-PAPER | Linearity of $\mathrm{Ric}(V, \cdot)$ in 2nd tangent vector. Repair: pointwise on $z$, additivity of `riemannCurvature` in 3rd-arg-section follows from `covDeriv_add_field` (already proven) applied to each of 3 covariant-derivative terms; trace inherits linearity. **No new infra needed.** |
44-
| `Curvature.lean:~322` | `ricciFormAt.toFun.map_smul'` | PRE-PAPER | Same path via `covDeriv_smul_const_field` (already proven). |
45-
| `Curvature.lean:~325` | `ricciFormAt.map_add'` | PRE-PAPER | Linearity of $\mathrm{Ric}(\cdot, W)$ in 1st tangent vector. Repair: additivity of `riemannCurvature` in 2nd-arg-section via `covDeriv_add_field` + `VectorField.mlieBracket_add_right` (Mathlib). |
46-
| `Curvature.lean:~327` | `ricciFormAt.map_smul'` | PRE-PAPER | Same path via `covDeriv_smul_const_field` + `VectorField.mlieBracket_const_smul_right` (Mathlib). |
47-
| `Metric/MathlibBridge.lean:~contMDiff` | `RiemannianMetric.toBundleContMDiffRiemannianMetric.contMDiff` | PRE-PAPER | Bundle CLM-section smoothness for the hom-bundle of TangentSpace twice. Phase 1C spike narrowed the goal to: `(T_dual x).linearMapAt y ((g.metricTensor y) ((T_tan x).symm y v)) w = (g.metricTensor y v) w`, which holds because the dual and tangent trivializations cancel on a chart's base set. Closure path: framework helper composing `Trivialization.symmL` + dual-trivialization-cancellation lemma. Not blocking framework usage — the bridge is symbolic; the framework's IPS is `OpenGALib.metricInner`, not Mathlib's bundle IPS (see `Metric/MathlibBridge.lean` "Phase 1C architectural lesson — the irreducible NACG diamond"). |
48-
49-
## GeometricMeasureTheory (14)
50-
51-
| File:line | Identifier | Classification | Repair plan |
52-
|-----------|-----------|---------------|-------------|
53-
| `Rectifiability.lean:85` | rectifiability of stationary varifolds | CITED-BLACK-BOX | Allard 1972 / Pitts 1981 rectifiability theorem; depends on `density > 0` assumption. |
54-
| `HasNormal.lean:126` | `tangentCone_unitNormal_exists` body | PRE-PAPER | Currently uses `Classical.choose` over the trivial existence `⟨fun _ => 0, trivial⟩`. Real repair: extract cone normal from chart-rescale weak limit. |
55-
| `FinitePerimeter.lean:83` | (perimeter measurability) | PRE-PAPER | Mathlib BV-on-charted-manifold gap. |
56-
| `FinitePerimeter.lean:133` | `rbdy ⊆ topClosure` | PRE-PAPER | Reduced boundary topological inclusion; standard but mechanical. |
57-
| `FinitePerimeter.lean:139` | reduced-boundary trichotomy | PRE-PAPER | Density-based trichotomy (interior / boundary / exterior). |
58-
| `Varifold.lean:86` | `density_nonneg` | PRE-PAPER | Direct from definition of density via mass; Mathlib measure-theory lemmas. |
59-
| `Varifold.lean:113` | support characterization | PRE-PAPER | Standard support-via-positive-mass-on-balls; Mathlib `MeasureTheory.Measure.support` adaptation. |
24+
| Module | PRE-PAPER | CITED-BLACK-BOX | Total |
25+
|--------|-----------|------------------|-------|
26+
| Algebraic | 5 | 0 | 5 |
27+
| Tensor | 9 | 0 | 9 |
28+
| Riemannian | 3 | 1 | 4 |
29+
| GeometricMeasureTheory | 5 | 10 | 15 |
30+
| **Total** | **22** | **11** | **33** |
31+
32+
CI workflow `.github/workflows/ci.yml` asserts the total equals 33 (`EXPECTED=33`).
33+
34+
## Algebraic (5)
35+
36+
| File:line | Identifier | Classification | Notes |
37+
|-----------|-----------|---------------|-------|
38+
| `Auxiliary/Fin.lean:86` | `addCases_succAbove_castAdd` | PRE-PAPER | Mathlib gap on `Fin.addCases` ∘ `Fin.succAbove` interaction. Mechanical case split. |
39+
| `Auxiliary/Fin.lean:98` | `addCases_succAbove_natAdd` | PRE-PAPER | Sister lemma to above. Same shape. |
40+
| `Auxiliary/ShuffleDeriv.lean:284` | `derivShuffleEquivLeft` injectivity branch | PRE-PAPER | Internal case in shuffle-derivative bijection. Inherited from external lib port. |
41+
| `Auxiliary/ShuffleDeriv.lean:300` | `derivShuffleEquivLeft` surjectivity (cardinality) | PRE-PAPER | Cardinality balance `(m+n+1)·C(m+n,m) = C(m+n+1,m+1)·(m+1)`. Inherited from external lib. |
42+
| `Auxiliary/ShuffleDeriv.lean:312` | `derivShuffleEquivLeft_sign` | PRE-PAPER | Sign of canonical `Quotient.out'` representatives. Inherited from external lib. |
43+
44+
## Tensor (9)
45+
46+
| File:line | Identifier | Classification | Notes |
47+
|-----------|-----------|---------------|-------|
48+
| `Alternating/Wedge.lean:378` | `uncurryFin_wedge_productL_precompL` | PRE-PAPER | Algebraic identity matching LHS/RHS via `derivShuffleEquivLeft`. Closure path documented in proof body. |
49+
| `Alternating/Wedge.lean:387` | `uncurryFin_wedge_productL_precompR` | PRE-PAPER | Sister identity with sign `(-1)^m`. |
50+
| `Alternating/Wedge.lean:715` | `domDomCongr_finAddFlip_wedge_self` | PRE-PAPER | Depends on removed Mathlib lemma `Equiv.Perm.finAddFlip_equiv_eqFin`. Currently unused; revisit if needed. |
51+
| `DifferentialForm/Basic.lean:194` | `ederiv_basis_expansion` | PRE-PAPER | Basis expansion of exterior derivative. Mechanical from `fderiv_basis`. |
52+
| `DifferentialForm/Basic.lean:286` | `iprod_wedge` algebra | PRE-PAPER | Interior product / wedge product interaction; algebraic. |
53+
| `DifferentialForm/Basic.lean:293` | `pullback.smooth` | PRE-PAPER | Smoothness of `ω ∘ fderiv f` composition. |
54+
| `DifferentialForm/Basic.lean:323` | `pullback_ederiv` (differentiability gap) | PRE-PAPER | Inner gap in pullback-commutes-with-ederiv proof. |
55+
| `DifferentialForm/Basic.lean:326` | `pullback_ederiv` (outer) | PRE-PAPER | Outer goal of same proof. |
56+
| `Product/Pretrivialization.lean:281` | `tensorProductCoordChange_contMDiffOn` | PRE-PAPER | Bundle pretrivialization plumbing; Mathlib gap on tensor-product bundle smoothness. |
57+
58+
## Riemannian (4)
59+
60+
| File:line | Identifier | Classification | Notes |
61+
|-----------|-----------|---------------|-------|
62+
| `Curvature.lean:241` | `riemannCurvature_inner_self_zero` | PRE-PAPER | Skew-symmetry of $R(X,Y)$. Closure path: metric-compat 4× + Hessian-Lie identity (`mfderiv_iterate_sub_eq_mlieBracket_apply`). Proof body sketches it. |
63+
| `Curvature.lean:256` | `ricci_symm` | PRE-PAPER | Symmetry of Ricci. Closure path: trace-via-orthonormal-basis + Bianchi I (closed) + diagonal-zero (above). |
64+
| `Connection.lean:1387` | `koszulCovDeriv_const_smoothAt` | PRE-PAPER | Path-B cascade leftover. Closure: write `metricRiesz_section_smoothAt` against `Bundle.ContMDiffRiemannianMetric` API via chart-pullback unwrapping of the Riesz isomorphism. Self-build follow-up. |
65+
| `Operators/Bochner.lean:49` | `bochner_weitzenboeck` | CITED-BLACK-BOX | Bochner–Weitzenböck identity. Reference: Petersen, *Riemannian Geometry*, §9. Body not provided; framework has all sub-primitives (Hessian, Laplacian, Ricci, gradient) but the identity itself is delegated to the citation. |
66+
67+
## GeometricMeasureTheory (15)
68+
69+
| File:line | Identifier | Classification | Notes |
70+
|-----------|-----------|---------------|-------|
71+
| `Rectifiability.lean:85` | `isRectifiable_of_stationary_density_pos` | CITED-BLACK-BOX | Allard 1972 / Pitts 1981 rectifiability theorem. |
72+
| `HasNormal.lean:128` | `tangentCone_unitNormal_exists` body | PRE-PAPER | Currently `Classical.choose` over trivial existence. Real repair: extract cone normal from chart-rescale weak limit. |
73+
| `FinitePerimeter.lean:83` | perimeter measurability | PRE-PAPER | Mathlib BV-on-charted-manifold gap. |
74+
| `FinitePerimeter.lean:135` | reduced-boundary trichotomy | PRE-PAPER | Density-based trichotomy (interior / boundary / exterior). |
75+
| `Varifold.lean:114` | `density_nonneg` | PRE-PAPER | Direct from definition of density via mass. |
76+
| `Varifold.lean:141` | support characterization | PRE-PAPER | Standard support-via-positive-mass-on-balls. |
6077
| `Isoperimetric/SobolevPoincare.lean:156` | Sobolev–Poincaré inequality | CITED-BLACK-BOX | Maggi 2012 §13. |
61-
| `Isoperimetric/Euclidean.lean:111` | Euclidean isoperimetric | CITED-BLACK-BOX | Maggi 2012 §14. |
62-
| `Isoperimetric/Euclidean.lean:135` | (variant) | CITED-BLACK-BOX | Same source. |
78+
| `Isoperimetric/Euclidean.lean:111` | Euclidean isoperimetric (eq form) | CITED-BLACK-BOX | Maggi 2012 §14. |
79+
| `Isoperimetric/Euclidean.lean:135` | Euclidean isoperimetric (sharp constant) | CITED-BLACK-BOX | Maggi 2012 §14. |
6380
| `Isoperimetric/ReducedBoundary.lean:113` | reduced boundary structure | CITED-BLACK-BOX | De Giorgi structure theorem; Maggi 2012 §15. |
64-
| `Isoperimetric/ReducedBoundary.lean:152` | (variant) | CITED-BLACK-BOX | Same source. |
65-
| `Isoperimetric/BVFunction.lean:114` | BV property | CITED-BLACK-BOX | Maggi 2012 §10. |
81+
| `Isoperimetric/ReducedBoundary.lean:152` | reduced boundary (variant) | CITED-BLACK-BOX | Maggi 2012 §15. |
82+
| `Isoperimetric/BVFunction.lean:114` | BV approximation | CITED-BLACK-BOX | Maggi 2012 §10. |
6683
| `Isoperimetric/Coarea.lean:73` | coarea formula | CITED-BLACK-BOX | Maggi 2012 §18. |
67-
| `Isoperimetric/Coarea.lean:117` | (variant) | CITED-BLACK-BOX | Same source. |
84+
| `Isoperimetric/Coarea.lean:117` | coarea (variant) | CITED-BLACK-BOX | Maggi 2012 §18. |
6885
| `Isoperimetric/Relative.lean:87` | relative isoperimetric | CITED-BLACK-BOX | Maggi 2012 §16. |
6986

70-
## Regularity (2)
71-
72-
| File:line | Identifier | Classification | Repair plan |
73-
|-----------|-----------|---------------|-------------|
74-
| `SmoothRegularity.lean:124` | Hausdorff small singular set | CITED-BLACK-BOX | Wickramasekera 2014 main theorem. |
75-
| `SmoothRegularity.lean:140` | smooth minimal hypersurface | CITED-BLACK-BOX | Wickramasekera 2014 + 2 ≤ n ≤ 6 specialization. |
76-
7787
## Notes
7888

79-
* This catalog tracks **public-facing** sorries (Riemannian /
80-
GeometricMeasureTheory / Regularity packages). Application papers
81-
maintain their own catalogs.
82-
* PRE-PAPER classification is **not permanent technical debt**: every
83-
PRE-PAPER entry has a concrete repair trigger (Mathlib API maturation
84-
or framework self-build follow-up).
85-
* Updating this file: when adding a new `sorry`, add a row +
86-
classification + repair plan. When closing a sorry (replacing with a
87-
real proof), remove its row. CI checks total count matches §"Total
88-
counts" table.
89+
* PRE-PAPER is **not permanent technical debt**: every PRE-PAPER entry has a
90+
concrete closure path (either Mathlib API to extend, or framework
91+
self-build to perform). The classification distinguishes "ready to close
92+
with focused work" from "deliberately delegated to a citation".
93+
* CITED-BLACK-BOX entries are **stable by design**: the framework states a
94+
named theorem from the literature and uses it without re-proving the body.
95+
These are the seven Maggi 2012 / Allard 1972 references plus the Bochner
96+
identity.
97+
* Updating this file: when adding a new `sorry`, append a row with
98+
classification + notes, and bump `EXPECTED` in `.github/workflows/ci.yml`.
99+
When closing a sorry (replacing with a real proof), remove its row and
100+
decrement `EXPECTED`. The per-module sub-table count must equal the
101+
summary table count.

0 commit comments

Comments
 (0)