9j: delete metricInner typeclass abbrev — end of typeclass-bound metric API#45
Merged
Conversation
…Manifold.lean - Project-wide mass perl: metricInner (abbrev) → HasMetric.metric.metricInner (dot) - Project-wide mass perl: metricInner_X (lemma) → HasMetric.metric.metricInner_X (dot-method) - Theorem declaration names preserved (exclusion regex) - Files defining the abbrev (SmoothManifold.lean, RiemannianMetric.lean) reverted - Deleted MetricAPI section (lines 122-302 of SmoothManifold.lean, ~180 LOC): - metricInner abbrev + 14 wrapper lemmas - metricToDual / metricRiesz / metricToDualEquiv abbrevs - metricInner_contMDiffWithinAt wrapper - Final external callsite fix: ReducedBoundary.lean uses fully-qualified Riemannian.HasMetric.metric.metricInner Simp set preserved: RiemannianMetric.metricInner_X lemmas already tagged @[simp, metric_simp], so post-substitution dot-method calls inherit simp behavior naturally. After this PR, no typeclass-bound metric abbrev exists in the codebase. All metric access is either: * g.metricInner / g.metricRiesz / ... — explicit g via dot-method * HasMetric.metric.metricInner / ... — typeclass projection followed by dot-method
…unused imports; cleanup deferred)
This was referenced May 19, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
9j — final step of the explicit-g cascade (umbrella #9). Removes the typeclass-bound
metricInnerabbrev + its 14 wrapper lemmas +metricToDual/metricRiesz/metricToDualEquivabbrevs +metricInner_contMDiffWithinAtwrapper fromManifold/SmoothManifold.lean'sMetricAPIsection (~180 LOC deleted).After this PR, no typeclass-bound metric abbrev exists in the codebase. All metric access is either:
g.metricInner/g.metricRiesz/ ... — explicitgvia dot-methodHasMetric.metric.metricInner/ ... — typeclass projection followed by dot-methodMigration
Project-wide perl mass-substitute:
metricInner X Y Z(abbrev call) →HasMetric.metric.metricInner X Y Z(dot)metricInner_X(lemma) →HasMetric.metric.metricInner_X(dot-method)^theorem|^lemma|^abbrev|^def metricInner)SmoothManifold.lean,RiemannianMetric.lean) untouched by perl; abbrev deletion done by handOne external callsite needed a fully-qualified namespace fix (
ReducedBoundary.lean:Riemannian.HasMetric.metric.metricInner).Simp set preservation
RiemannianMetric.metricInner_Xlemmas at the def site (Riemannian/Metric/RiemannianMetric.lean) are already tagged@[simp]and@[metric_simp]. Post-substitution dot-method calls (HasMetric.metric.metricInner_Xandg.metricInner_X) inherit simp behavior naturally.Cascade complete
This closes the umbrella issue #9 (explicit-g cascade):
RiemannianMetrictype with explicit gsubst hgpattern_gnotations droppedmetricInnertypeclass abbrev deletedTest plan
lake buildclean