[F1] Add tensor regularity and frame bridges (#41)

[AxelDlv00]

Contributor : contributor 🧑‍💻 🔁

Profile: contributor (contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra

🔍 Scope

Part of #41. This PR advances S12 with a focused evaluation-level regularity
and local-frame component slice for the exact bundled leviCivitaConnection.
It does not claim to complete the full S12 acceptance criteria.

✅ Delivered

• Adds a Hom-bundle mfderiv evaluation bridge and its global directional-
  derivative regularity form.
• Adds an indexed rank-generic producer for
  mixedCovariantDerivativeAlong and the source-ordered
  secondCovariantDerivative, under an explicit smooth metric-dual witness
  for contravariant slots.
• Adds witness-free covariant (p = 0) producers, scalar rank-zero adapters,
  and one-form regularity adapters.
• Adds local-frame covectors, inverse-Gram coefficient and ContMDiffAt
  calculations, and the canonical frame dual-action -Γ bridge with the
  Christoffel component wrapper.
• Records the slice and its open replacement triggers in ROADMAP.md.

🟠 Boundary

The producers return evaluation-level predicates; they do not construct a
bundled tensor-product section or prove multilinearity/tensoriality of the
output. The arbitrary mixed-rank producer keeps its indexed metric-dual
regularity witness visible. The lower-level frame theorem is point-local,
while the canonical local-frame wrapper discharges that premise on the chart
base set through inverse-Gram coefficients.

The unconditional bundled producer, full mixed dual-frame +Γ/-Γ component
expansion, unconditional inner/second-direction extension independence,
canonical Hessian/trace compatibility, and flat/nonconstant model regressions
remain open. TensorLaplacian stays a direct-only leaf, as required by the
accepted roadmap until the S13 replacement trigger; MorganTianLib/Ch01.lean
is intentionally unchanged.

🧪 Local validation

• Contributor LSP diagnostics for the changed Lean source completed with no
  diagnostics on the final source snapshot.
• Direct elaboration against the pinned artifacts completed with
  -DwarningAsError=true after integrating the current origin/main.
• Exported #print axioms probes report only propext, Classical.choice,
  and Quot.sound for the new declarations.
• git diff --check, conflict-marker, proof-hole, unsafe/axiom, forbidden-
  dependency, and Chapter 2 import scans are clean.
• The repository-owned Lean CI / lake-build (pull_request) workflow remains
  the authoritative exact-head validation; no local full lake build was run.

📚 References

Morgan--Tian, Ricci Flow and the Poincare Conjecture, Chapter 1 discussion
preceding lapformula, pp. 39--40, bibliography key morganTian2007;
pinned Mathlib ContMDiffMFDeriv, Hom-bundle, covariant-derivative,
Tensoriality, trace, local-frame, Gram, adjugate, and nonsingular-inverse APIs.

[AxelDlv00]

Reviewer : mathematical-correctness 📐 ✅

Profile: mathematical-correctness (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 57df350

🔍 Coverage

I reviewed the immutable exact head 57df3509fe9ee144f44a59af973ae219bd07108f against base d90c66c2084ec07625f45acbfc9eecb1ee5852d0, including the complete changes.diff, the changed Lean source, and the S12 entry in ROADMAP.md. The PR describes an explicitly partial evaluation-level slice, so I treated the still-open bundled producer, extension-independence, and model-regression items as boundary conditions rather than silently required additions.

The mathematical review covered every added public declaration in MorganTianLib/Ch01/Connection/TensorLaplacian.lean: the Hom-bundle/directional-derivative bridges and metric-compatibility formulas (lines 349–515), the indexed first/second regularity producers and covariant/scalar/one-form adapters (1099–1322), and the local-frame covector, inverse-Gram, dual-action, and Christoffel bridges (1692–2109).

✅ Verified

• contMDiffAt_mvfderiv_apply_along and directionalDerivative_contMDiff use the standard smooth mfderiv Hom-bundle section followed by smooth fibre evaluation. The ∞ regularity and the explicit omission of finite-dimensionality are appropriate for this calculus bridge.
• dualCovariantVector_apply_formula_at (438) is exactly the metric-compatibility identity
  (∇_X θ♯)^♭(Z) = X[θ(Z)] - θ(∇_X Z). Its hypotheses are precisely the pointwise differentiability needed by the pinned IsMetricCompatible.mvfderiv_inner_eq; no differentiability of the arbitrary direction section is being smuggled in.
• dualCovariantVector_isSmoothCovectorSection (488) correctly combines that identity with smooth connection evaluation. mixedCovariantDerivativeAlong_isSmooth (1099) makes the contravariant metric-dual regularity witness explicit, proves smoothness of each updated argument family, and then uses only finite sums and subtraction. It does not assert multilinearity, tensoriality, or a bundled tensor section.
• secondCovariantDerivative_isSmooth (1177) preserves the source order ∇_X(∇_Z A) - ∇_{∇_X Z}A. The p = 0 specializations and scalar/one-form adapters are genuine vacuous-index consequences; Fin 0 and zero-dimensional fibres are handled without an unstated positive-dimension assumption.
• The local-frame coefficient theorem (1780) has the correct orientation: if G r j = g(e_r,e_j), then the coefficients solve Gᵀ c = e_a, hence c_k = (G⁻¹) a k, exactly as stated. Gram non-singularity follows from local-frame linear independence, and the determinant/adjugate argument gives the claimed pointwise smoothness on the open trivialization base set.
• dualCovariantVector_frameCovector_apply_frame (1941) has the correct dual-frame sign, -Γ, and the canonical wrapper discharges its differentiability premise through the inverse-Gram result. Combining it with the existing covariantVector_christoffel_formula gives the displayed -(1/2) factor and the same derivative indices as the bundled Levi--Civita formula; the chart-interior hypothesis is retained.

No changed statement relies on a converse, a hidden nondegeneracy assumption, or a wrong direction/order implication. I found no blocking mathematical defect.

🟡 Scope note

The generic producer's indexed hdual premise is materially stronger than the desired eventual unconditional theorem, but it is visible in the statement, sufficient for every recursive use, and explicitly recorded as provisional in the PR and roadmap. That is an intentional partial boundary, not a false mathematical claim.

🧪 Validation

I inspected the exact-head source and pinned Mathlib definitions for ContMDiffAt.mfderiv_const, Hom-bundle evaluation, metric compatibility, local-frame coefficients, Gram determinants, and nonsingular matrix inverses. The exact-head diff passes git diff --check; the changed Lean source contains no sorry, admit, axiom, or unsafe marker. Per immutable-review policy I did not run Lake, download caches, or start LSP. The author-reported direct elaboration and CI validation were not independently rerun here.

📚 References

The source-order comparison is Morgan--Tian, Chapter 1, pp. 39--40 (morganTian2007), and the implementation reuses the existing Connection.leviCivitaConnection/covariantVector_christoffel_formula together with the pinned Mathlib CovariantDerivative.Metric, VectorBundle.Hom, VectorBundle.LocalFrame, GramMatrix, Adjugate, and NonsingularInverse APIs.

💬 Decision

✅ Approve. The exact head meets the mathematical-correctness bar for the partial S12 slice, with no blocking findings in the declarations reviewed.

[AxelDlv00]

Reviewer : maths-lean-correspondence 🌉 ✅

Profile: maths-lean-correspondence (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 57df350

Reviewer : maths-lean-correspondence 🌉

🔍 Coverage

I reviewed the immutable change from base d90c66c2084ec07625f45acbfc9eecb1ee5852d0
to exact head 57df3509fe9ee144f44a59af973ae219bd07108f, using review.json,
changes.diff, both changed-file snapshots, the PR record, and the accepted
S12 entry in ROADMAP.md (issue #41).
The declared boundary is a partial, evaluation-level S12 slice. I covered all
changed declarations in these groups:

• the Hom-bundle/mvfderiv bridges (contMDiffAt_mvfderiv_apply_along,
  directionalDerivative_contMDiff, lines 349 and 374);
• metric-dual compatibility and the indexed first/second regularity producers,
  including the rank-zero and one-form adapters (lines 386, 438, 488, and 1099--1322);
• local-frame covectors, inverse-Gram smoothness, dual-frame signs, and the
  Christoffel component wrappers (lines 1692--2109), including both private
  determinant/inverse helpers; and
• the module documentation and the S12 roadmap update.

✅ Verified

• d% in the calculus bridge is Mathlib's mvfderiv (pinned
  Geometry/Manifold/MFDeriv/NormedSpace.lean), and the proof uses the intended
  ContMDiffAt.mfderiv_const, contMDiffAt_hom_bundle, and
  ContMDiffAt.clm_bundle_apply APIs. The conclusion is the applied derivative
  fun y => d% f y (X y), not a different coordinate derivative.
• dualCovariantVector_apply_formula and its pointwise form use the exact
  Riesz map (InnerProductSpace.toDual) and Mathlib's
  IsMetricCompatible.mvfderiv_inner_eq. Their hypotheses and conclusion are
  precisely the dual-connection identity
  X[theta(Z)] - theta(nabla_X Z); no smoothness of the direction X is
  silently added or needed.
• mixedCovariantDerivativeAlong_isSmooth updates every contravariant slot by
  dualCovariantVector and every covariant slot by covariantVector, with the
  displayed minus sums. Its indexed hdual premise is used exactly where the
  metric-dual section is required. secondCovariantDerivative_isSmooth expands
  the source order nabla_X (nabla_Z A) - nabla_(nabla_X Z) A, matching the raw
  definition at lines 583--592.
• The p = 0 witness is genuinely Fin.elim0; the scalar rank-zero and
  one-form adapters reduce the argument families with Subsingleton/Fin 1
  exactly, rather than assuming a nonempty slot. Existing rank-zero equality
  declarations give the stated Hessian interpretation.
• frameCovector is Mathlib's localFrame_coeff converted to a fibrewise
  continuous linear map. On the base set its action is the basisAt.repr
  Kronecker delta. The inverse-Gram proof solves G.transpose * c = e_a, hence
  c_k = (G^-1) a k; the transpose and matrix indices are in the correct
  orientation. The local-frame smoothness proof uses
  contMDiffAt_iff_localFrame_coeff and an eventual equality inside the open
  base set, so off-domain zero values do not alter the point-local claim.
• Metric compatibility then gives the coframe action -Gamma, and the combined
  wrapper has the existing covariantVector = nabla_(e_i) e_j order and the
  Christoffel expression from the pinned connection module. The docstrings and
  roadmap accurately call these evaluation-level/direct-only bridges and leave
  the bundled producer and full mixed-frame expansion open.

🟡 Scope note

IsSmoothCovectorSection and IsSmoothMixedTensorSection are evaluation
predicates, not bundled tensor smoothness contracts, and the mixed producer
keeps an explicit metric-dual witness. That is a visible, intentional boundary
in the declarations, PR description, and roadmap; it is not an implicit
strengthening, unsatisfiable hypothesis, or correspondence defect. The omitted
unconditional/bundled work therefore does not block this declared slice.

🧪 Validation

The exact-head metadata and SHA match review.json; static diff checks are
clean, and the changed Lean source has no proof-hole, project axiom, or
unsafe declaration. I did not run Lake or LSP, as required for this immutable
review context; contributor-reported elaboration/CI remains implementation
evidence rather than a substitute for the correspondence checks above.

📚 References consulted

The source correspondence was checked against Morgan--Tian Chapter 1,
pp. 39--40 (morganTian2007, present in docs/references.bib), and the pinned
Mathlib definitions in ContMDiffMFDeriv, VectorBundle/Hom,
CovariantDerivative/Metric, VectorBundle/LocalFrame, GramMatrix,
Matrix/Adjugate, and Matrix/NonsingularInverse. A focused search for
Mathlib PRs on contMDiffAt_hom_bundle, local-frame inverse-Gram components,
and induced Hom/tensor connections found no close merged analogue; the pinned
source was used directly. The current LocalFrame API is documented at
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.html.

💬 Decision

✅ Approve. I found no maths--Lean correspondence mismatch or unintended
vacuity on exact head 57df3509fe9ee144f44a59af973ae219bd07108f.

[AxelDlv00]

Reviewer : lean-quality 🧪 🔴

Profile: lean-quality (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: changes-requested 🔴
Head: 57df350

🔍 Coverage

Reviewed the complete exact-head change at 57df3509fe9ee144f44a59af973ae219bd07108f
(base d90c66c2084ec07625f45acbfc9eecb1ee5852d0). The diff adds the
evaluation-level regularity/Hom-bundle bridge, indexed first- and second-derivative
producers and p = 0 adapters, and the local-frame inverse-Gram/Christoffel block;
it also records the S12 partial boundary in ROADMAP.md. This is a Lean-quality
review; mathematical and correspondence questions are left to their assigned
profiles.

✅ Verified

• contMDiffAt_mvfderiv_apply_along and directionalDerivative_contMDiff use the
  existing Hom-bundle and mfderiv APIs and correctly omit the model
  finite-dimensionality assumption.
• mixedCovariantDerivativeAlong_isSmooth and
  secondCovariantDerivative_isSmooth keep the indexed metric-dual witness
  explicit and document that the result is an evaluation predicate, not a bundled
  tensor-product section. The covariant (p = 0), scalar, and one-form adapters
  follow that boundary.
• frameCovector, the inverse-Gram regularity lemmas, and the canonical dual-action
  and Christoffel wrappers are placed in the existing Connection.TensorLaplacian
  ownership boundary. The stable MorganTianLib.Ch01 umbrella remains unchanged,
  as required by the roadmap's provisional-leaf trigger.
• The immutable source/ file is byte-identical to head/; static scans found no
  code sorry, admit, axiom, unsafe, debug output, proof holes, conflict
  markers, trailing whitespace, or lines over 100 characters. The repository has
  an exact-head Lean CI / lake-build (pull_request) workflow; this review did not
  run Lake or LSP because the job policy disables both.

🔴 Findings

1. An exported theorem has no declaration docstring.
   frameCovector_apply_frame_of_mem at
   MorganTianLib/Ch01/Connection/TensorLaplacian.lean:1705 starts immediately
   after the frameCovector definition's docstring. It is a public [simp]
   theorem with a useful local-frame hypothesis, so the preceding docstring does
   not document it. Please add a concise /-- ... -/ describing the base-set
   condition and the dual-frame evaluation. Keep the statement, proof, and simp
   choice unchanged.

🟠 Documentation corrections

• The docstring at lines 1256--1260 for
  scalarTensor_isSmoothSecondCovariantDerivative says that this declaration's
  raw evaluator “agrees with the iterated directional derivative”. Its result type
  only supplies IsSmoothSecondCovariantDerivative; the explicit rank-zero
  evaluator equation is secondCovariantDerivativeCovariant_rank_zero. Please
  describe this theorem as the regularity wrapper and cross-reference the equation.
• The docstring at lines 1283--1285 says that
  scalarTensor_constant_isSmoothSecondCovariantDerivative “checks both
  regularity and normalization”, while its conclusion supplies regularity only.
  Please say that secondCovariantDerivativeCovariant_constant supplies the
  separate normalization fact.

🟡 Nonblocking quality notes

• The three added matrix imports (GramMatrix, Adjugate, and
  NonsingularInverse) are transitively available through the direct
  Connection.Christoffel import (Christoffel imports the first and third, and
  pinned NonsingularInverse.lean publicly imports Adjugate). They are all used,
  so this is only an import-graph cleanup suggestion: remove the duplicate edges
  or document why explicit direct edges are preferred. There is no behavior change
  requested.
• The standalone attribute [nolint simpNF] for the frame theorem has a sensible
  normal-form rationale, but it is worth revisiting when linting is enabled. The
  current workflows set lint: false and publish no changed-file timing report,
  so I make no performance claim.

📚 References consulted

The repository documentation at
/tmp/palimpsest-documentation/doc-strings.md requires every definition and
major theorem to have a faithful /-- ... -/ string; this matches the upstream
mathlib documentation style.
For the import note I checked the pinned module headers (Christoffel.lean and
NonsingularInverse.lean). A focused upstream search also found
mathlib PR 40680,
which removes redundant simpNF suppressions (“Remove the attribute whenever its
redundant”); the present rationale preserves a user-facing normal form, so I treat
that as a cleanup discussion rather than a blocker. The open
Hom-bundle covariant-derivative PR 43020
was treated as trajectory evidence only because it is not in the pinned release.

💬 Decision

🔴 Request changes. The missing public declaration docstring is a library-level
documentation defect and also misses the S12 acceptance criterion. Please apply
that small documentation fix and the two wording corrections above; no proof/API
rewrite or umbrella export is requested.

[AxelDlv00]

Reviewer : lean-quality 🧪 📣

Profile: lean-quality (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 57df350

🔴 This exported [simp] theorem has no declaration docstring: the preceding /-- ... -/ belongs to frameCovector. Please add a concise docstring stating the base-set hypothesis and the dual-frame evaluation. Keep the theorem statement, proof, and simp choice unchanged.

[AxelDlv00]

Contributor : contributor 🧑‍💻 📣

Profile: contributor (contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 57df350

✅ Applied. Added a declaration docstring immediately before frameCovector_apply_frame_of_mem describing the x ∈ t.baseSet premise and its Kronecker-delta dual-frame evaluation. The theorem statement, proof, and [simp] attribute are unchanged in commit 72b3b8d.

[AxelDlv00]

Reviewer : lean-quality 🧪 📣

Profile: lean-quality (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 57df350

🟠 The docstring says this declaration's raw evaluator "agrees with the iterated directional derivative", but the result type only provides IsSmoothSecondCovariantDerivative; the explicit rank-zero evaluator equation is secondCovariantDerivativeCovariant_rank_zero. Please describe this theorem as the regularity wrapper and cross-reference that equation.

[AxelDlv00]

Contributor : contributor 🧑‍💻 📣

Profile: contributor (contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 57df350

✅ Applied. Reworded scalarTensor_isSmoothSecondCovariantDerivative as an evaluation-level regularity wrapper and explicitly cross-referenced secondCovariantDerivativeCovariant_rank_zero for the evaluator equation. The declaration and proof are unchanged in commit 72b3b8d.

[AxelDlv00]

Reviewer : lean-quality 🧪 📣

Profile: lean-quality (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 57df350

🟠 The docstring says this declaration "checks both regularity and normalization", while its conclusion supplies regularity only. Please say that secondCovariantDerivativeCovariant_constant supplies the separate normalization fact.

[AxelDlv00]

Contributor : contributor 🧑‍💻 📣

Profile: contributor (contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 57df350

✅ Applied. Corrected scalarTensor_constant_isSmoothSecondCovariantDerivative to state that it establishes only IsSmoothSecondCovariantDerivative; the separate normalization fact is now identified as secondCovariantDerivativeCovariant_constant. The theorem and proof are unchanged in commit 72b3b8d.

[AxelDlv00]

Reviewer : architecture 🏗️ ✅

Profile: architecture (architecture)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 57df350

🔍 Coverage

I reviewed the exact head 57df3509fe9ee144f44a59af973ae219bd07108f against
base d90c66c2084ec07625f45acbfc9eecb1ee5852d0, issue #41, the complete changes.diff, both changed files, and the immutable source snapshots. The architecture pass covered every new declaration in MorganTianLib/Ch01/Connection/TensorLaplacian.lean: the Hom-bundle directional regularity bridge (lines 349--380), dual-connection and rank-generic evaluation producers (438--1322), and the local-frame/inverse-Gram/Christoffel bridges (1692--2109), together with the ROADMAP.md and import-graph changes.

The issue text's earlier request to export the leaf through the umbrella is reconciled by the later accepted roadmap boundary: ROADMAP.md:704 and the Ch01.lean module documentation require this provisional layer to remain direct-only until the S13 replacement trigger. The unchanged umbrella is therefore intentional, not an undisclosed omission.

✅ Verified

• The new connection-facing statements take the explicit Bundle.ContMDiffRiemannianMetric ... g and use the exact leviCivitaConnection g; local Bundle.RiemannianBundle instances are transported from g. I found no competing metric, connection, or tensor representation and no dependency-order inversion.
• mixedCovariantDerivativeAlong_isSmooth (line 1099) and secondCovariantDerivative_isSmooth (1177) are genuinely rank-generic and preserve the source order ∇_X (∇_Z A) - ∇_{∇_X Z} A. The indexed metric-dual regularity obligation is visible in the public hdual premise (1107--1109), while the p = 0 adapters (1217--1239) are actually witness-free rather than merely renamed one-form wrappers.
• The output remains the documented evaluation-level predicate. The declarations and module text explicitly do not claim multilinearity, tensoriality, extension independence, or a bundled tensor-product connection, so this slice does not package the missing canonical result behind a facade.
• The frame route has a coherent dependency chain: frameCovector (1692) -> inverse-Gram coefficients (1780) -> local ContMDiffAt/differentiability (1863/1922) -> the dual-action -Γ bridge (1941/1988) -> the existing canonical Christoffel theorem (2043/2083). The lower-level differentiability premise and the canonical _of_mem discharge are both explicit; the full mixed dual-frame expansion remains open as recorded.
• The new matrix imports are focused on the inverse-Gram proof. lakefile.lean's default target globs all MorganTianLib submodules, so the direct leaf is still part of the CI build even though it is absent from the stable umbrella. The roadmap audit row and provisional-debt row record the same boundary and replacement trigger.

🟡 Scope note

The indexed hdual witness and evaluation-level predicates are real provisional debt, not a canonical S12 completion. The unconditional mixed producer, bundled tensor-section construction, full dual-frame component expansion, inner/second-direction extension independence, canonical Hessian/trace compatibility, and flat/nonconstant regressions remain open. Those omissions are stated in the PR, source documentation, and ROADMAP.md:357/704, with an objective S13 consumer trigger, so they do not block this explicitly partial milestone.

🧪 Validation

• review.json confirms the reviewed base/head SHAs and the two-file change boundary.
• The changed diff is clean of sorry/admit/axiom/unsafe, forbidden Chapter 2 imports, conflict markers, and whitespace errors; no repository files were modified during review.
• I inspected the exact-head checkout workflow and package target configuration. Per the immutable review policy, I did not run Lake, download caches, or start LSP; the contributor-reported CI result was not independently rerun here.

📚 References

The source citation was checked against docs/references.bib (morganTian2007) and the retained Morgan--Tian prelim.tex discussion preceding lapformula (pp. 39--40). The pinned Mathlib source Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean:33--41 still describes an induced Hom(V,W) connection as future work, which supports keeping this evaluation-level bridge explicit. A focused search of current mathlib pull requests for a packaged induced tensor/Hom connection and the local-frame coefficient route found no closer analogue; adjacent prior art recorded by the roadmap includes PR 36845 and PR 36036, neither of which changes this boundary.

💬 Decision

✅ Approve. At the exact reviewed head, this is an architecturally coherent and honestly bounded S12 increment: it advances the canonical route, keeps provisional APIs out of the stable export, and names the work required before S13 can consume it. I found no blocking architecture correction.

[AxelDlv00]

Contributor : contributor 🧑‍💻 🚫

Profile: contributor (contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 57df350

✅ Revision

Applied all three requested documentation changes in commit 72b3b8dc9b060c9364f51ee9822b9d2a54e57424 (new head 72b3b8d). The theorem statements, proofs, attributes, and API surface are unchanged.

✅ Findings

• 3885530527: Applied. Added the public declaration docstring for frameCovector_apply_frame_of_mem, including the x ∈ t.baseSet condition and the Kronecker-delta dual-frame evaluation.
• 3885530554: Applied. Recast scalarTensor_isSmoothSecondCovariantDerivative as an evaluation-level regularity wrapper and cross-referenced secondCovariantDerivativeCovariant_rank_zero for the explicit evaluator equation.
• 3885530576: Applied. Clarified that scalarTensor_constant_isSmoothSecondCovariantDerivative establishes only IsSmoothSecondCovariantDerivative; secondCovariantDerivativeCovariant_constant supplies the separate normalization fact.

The nonblocking import-graph note is unchanged because it was identified as cleanup rather than a requested behavioral or documentation correction.

🧪 Validation

• Refreshed origin and confirmed the branch was already integrated with origin/main; no merge conflict or additional protected-branch change was present.
• Focused elaboration of MorganTianLib/Ch01/Connection/TensorLaplacian.lean against the pinned artifacts completed with -DwarningAsError=true and no output diagnostics.
• git diff --check passed, and static scans found no proof holes, sorry, admit, axiom, unsafe, TODO/FIXME markers, or conflict markers in the changed source.
• The contributor LSP bridge was invoked, but its diagnostic endpoint reported diagnostics_unavailable because the checkout build tree is not known clean and is read-only; the independent pinned elaboration above completed successfully. No local full lake build was run, leaving the repository workflow as the authoritative CI check.

💬 Handoff

The final revision is pushed to palimpsest/contributor/issue-41 at 72b3b8d.

[AxelDlv00]

Palimpsest automation ⚙️ 📣

Engine: codex
Model: gpt-5.6-sol
Effort: ultra

Palimpsest revision recorded: profile contributor published head 57df3509fe9ee144f44a59af973ae219bd07108f -> 72b3b8dc9b060c9364f51ee9822b9d2a54e57424 in response to review(s) review artifact 5460233695. Reviewers should reverify only the affected findings and changed material.

[AxelDlv00]

Reviewer : mathematical-correctness 📐 ✅

Profile: mathematical-correctness (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 72b3b8d

🔍 Coverage

I reviewed the immutable exact head 72b3b8d against base d90c66c, reconciling PR 64, the complete diff, both changed files, the S12 roadmap contract, the retained Morgan--Tian source, and the pinned Mathlib declarations used by the proofs.

The PR is a disclosed partial S12 slice: it adds conditional evaluation-level regularity and local-frame component bridges, while leaving the bundled tensor producer, full mixed component expansion, extension independence, Hessian/trace compatibility, and model regressions open. That boundary is reflected in ROADMAP.md and does not change the stable umbrella. Within the mathematical-correctness dimension I covered every added public declaration and the determinant/inverse helpers in MorganTianLib/Ch01/Connection/TensorLaplacian.lean, grouped as follows:

• the Hom-bundle directional-derivative and metric-compatibility bridges (lines 349--515);
• the rank-generic first/second regularity producers and covariant, scalar, and one-form adapters (lines 1099--1323);
• the frame covector, inverse-Gram regularity, dual-action sign, and Christoffel component bridges (lines 1693--2112).

✅ Verified

• contMDiffAt_mvfderiv_apply_along obtains the smooth Hom-bundle derivative section from ContMDiffAt.mfderiv_const and evaluates it on a smooth tangent section. At C-infinity, the derivative-order loss is harmless, and no finite-dimensional model hypothesis is mathematically needed.
• dualCovariantVector_apply_formula_at is exactly metric compatibility rewritten through the Riesz map: (∇_X θ♯)^♭(Z) = X[θ(Z)] - θ(∇_X Z). The pointwise differentiability assumptions on θ♯ and Z are sufficient; the direction is only evaluated at x, so no hidden smoothness assumption on X is required. The smooth covector wrapper then establishes precisely its evaluation-level predicate.
• mixedCovariantDerivativeAlong_isSmooth treats the directional term and every finite correction sum with the stated hypotheses. Its recursive use in secondCovariantDerivative_isSmooth preserves Morgan--Tian's order ∇_X(∇_Z A) - ∇_{∇_X Z}A; it neither assumes nor concludes symmetry in X,Z.
• The p = 0 adapters discharge the metric-dual witness genuinely by Fin.elim0. Scalar rank zero, constant scalars, one-forms, empty argument families, and zero-dimensional fibres introduce no unstated nontriviality or positive-dimension assumption. The revised scalar docstrings also correctly distinguish regularity from the separate evaluator and normalization equations.
• On t.baseSet, frameCovector evaluates on the local frame as the Kronecker delta. If G r j = g(e_r,e_j) and c are the coefficients of its metric dual, the equations are G-transpose c = e_a, hence c_k = (G-inverse) a k, which is the orientation stated by metricDualSection_frameCovector_coeff. Local-frame independence makes the Gram determinant nonzero, so using the totalized matrix inverse only near that nonsingular point is sound.
• The locally constant dual-frame pairing gives ∇_{e_i} ε^a(e_j) = -ε^a(∇_{e_i}e_j) = -Γ^a_{ij}. Combining this with the existing Christoffel theorem yields the displayed -(1/2) factor with inverse-Gram entry (G-inverse) a l and derivative order ∂_i g_lj + ∂_j g_il - ∂_l g_ij. The chart wrapper retains the required interior-point hypothesis; the intrinsic frame identity only needs base-set membership.

I found no converse error, sign or index reversal, hidden nondegeneracy condition, or mathematically false statement.

🟡 Scope

The generic producer's universal indexed hdual premise is stronger than the eventual unconditional tensor theorem, but it is explicit, sufficient for every contravariant replacement used in the proof, and recorded as provisional in both the PR and roadmap. This is an intentional partial boundary, not a mathematical defect.

🧪 Validation

The changed snapshots are byte-identical to the exact-head files under source/, and review.json records the expected head. A no-index diff check emitted no whitespace diagnostics, and the added Lean declarations contain no sorry, admit, new axiom, unsafe, or conflict marker. I inspected the pinned Mathlib source for ContMDiffAt.mfderiv_const, contMDiffAt_hom_bundle, IsMetricCompatible.mvfderiv_inner_eq, local-frame coefficients, Gram non-singularity, and nonsingular inverses.

Per the immutable-review policy in /tmp/palimpsest-documentation/pr-review.md and /tmp/palimpsest-documentation/mathlib-reviewing.md, I did not run Lake, download caches, or start LSP; the controller did not enable a targeted diagnostic. No upstream PR-history search was needed because the current pinned source and the publication directly settled the mathematical claims.

📚 References

Morgan--Tian, Chapter 1 (morganTian2007), gives ∇(dx^a) = -Γ^a_{ij} dx^i ⊗ dx^j and, before lapformula, ∇²ω(·,X,Y) = (∇_X∇_Yω)(·) - ∇_{∇_X Y}ω(·), explicitly noting the nonsymmetry. The bibliography key is present in docs/references.bib.

💬 Decision

✅ Approve. The exact head meets the mathematical-correctness bar for this explicitly partial S12 slice, with no blocking or material nonblocking mathematical findings.

[AxelDlv00]

Reviewer : maths-lean-correspondence 🌉 ✅

Profile: maths-lean-correspondence (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 72b3b8d

🔁 Reverification scope

I rechecked exact head 72b3b8dc9b060c9364f51ee9822b9d2a54e57424 against
review.json, the immutable source and head snapshots, the patch, and the
forge revision record. The prior maths--Lean correspondence audit at
review artifact 5460109045
covered the unchanged declarations at 57df3509fe9ee144f44a59af973ae219bd07108f.
The revision record
and contributor response
report that this head changes only documentation, with theorem statements,
proofs, attributes, and the API surface unchanged. Following the
incremental-review rule in
/tmp/palimpsest-documentation/pr-review.md, I focused on the affected
correspondence claims.

✅ Verified

• MorganTianLib/Ch01/Connection/TensorLaplacian.lean:1708
  (frameCovector_apply_frame_of_mem) now documents both the explicit
  x ∈ t.baseSet premise and the Kronecker-delta evaluation. These are
  exactly the theorem's hypothesis and conclusion at lines 1713--1716.
• MorganTianLib/Ch01/Connection/TensorLaplacian.lean:1260
  (scalarTensor_isSmoothSecondCovariantDerivative) now calls
  itself an evaluation-level IsSmoothSecondCovariantDerivative wrapper and
  points to secondCovariantDerivativeCovariant_rank_zero for the separate
  evaluator equation. The prose no longer attributes that equation to this
  regularity theorem.
• MorganTianLib/Ch01/Connection/TensorLaplacian.lean:1287
  (scalarTensor_constant_isSmoothSecondCovariantDerivative) now
  states that it supplies only the regularity predicate and names
  secondCovariantDerivativeCovariant_constant as the separate normalization
  result. This matches its type and proof.
• The prior correspondence checks carry forward for the Hom/mvfderiv bridge,
  metric-dual identity, source order of the second derivative, rank-zero and
  one-form adapters, inverse-Gram index orientation, and the local-frame
  -Γ sign. No new quantifier, coercion, or vacuity mismatch is introduced by
  this documentation delta; the provisional evaluation-level boundary and
  roadmap remain accurately stated.

🧪 Validation

review.json records the expected head, and both changed files under source/
are byte-identical to their head/ snapshots. A no-index diff check emitted
no whitespace diagnostics. I did not run Lake or LSP, as required for this
immutable review context; the contributor's focused elaboration is retained as
reported evidence, not treated as an independent correspondence argument.

💬 Decision

✅ Approve. The documentation corrections align the prose with the exact
Lean statements, and the unchanged mathematical correspondence remains sound
on exact head 72b3b8dc9b060c9364f51ee9822b9d2a54e57424.

[AxelDlv00]

Reviewer : architecture 🏗️ ✅

Profile: architecture (architecture)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 72b3b8d

🔍 Coverage

I reviewed the exact head 72b3b8dc9b060c9364f51ee9822b9d2a54e57424 against
base d90c66c2084ec07625f45acbfc9eecb1ee5852d0, including the complete
TensorLaplacian.lean and ROADMAP.md diff, the changed-file snapshots, and
the stable Ch01.lean import boundary.

The change is one coherent S12 slice. I traced the Hom-bundle directional
regularity bridge (contMDiffAt_mvfderiv_apply_along, line 349), the dual
regularity bridge (line 488), the indexed first/second evaluation producers
and their p = 0 adapters (lines 1099, 1177, 1217, and 1232), and the local
frame/inverse-Gram/sign wrappers (lines 1693, 1783, 1866, 1944, and 2046).

✅ Verified

• mixedCovariantDerivativeAlong_isSmooth and
  secondCovariantDerivative_isSmooth return the existing evaluation-level
  predicates. They retain the indexed metric-dual regularity witness and do
  not manufacture multilinearity, tensoriality, extension independence, or a
  tensor-product bundle. The second producer preserves the documented order
  ∇_X (∇_Z A) - ∇_{∇_X Z} A.
• The covariant (p = 0), scalar, and one-form wrappers are downstream
  adapters to that same evaluator contract; they do not silently become a
  bundled Hessian or Laplacian API. The constant-scalar theorem is separately
  documented as regularity only, with the existing normalization theorem left
  distinct.
• The directional-derivative proof constructs the existing Hom-bundle total
  space and uses Mathlib's contMDiffAt_hom_bundle/application API. It keeps
  leviCivitaConnection g as the sole connection and introduces no competing
  metric, connection, or tensor representation.
• frameCovector and the inverse-Gram coefficient/smoothness lemmas are
  point-local: the substantive statements require p ∈ t.baseSet, and the
  canonical wrappers use trivializationAt, Module.finBasis, and the
  existing covariantVector_christoffel_formula. The -Γ sign bridge and
  its chart formula therefore remain adapters to the canonical connection,
  not a new coordinate-defined connection.
• The exact stable umbrella is preserved. MorganTianLib/Ch01.lean remains
  unchanged and continues to state that Connection.TensorLaplacian is
  direct-only until the S13 bundled, extension-independent producer exists.
  The roadmap still marks S12 Partial, keeps the S13 replacement trigger,
  and explicitly lists the bundled producer, full mixed component expansion,
  Hessian/trace compatibility, and model regressions as open.
• The dependency direction is sound for this slice: only the existing
  connection/Christoffel modules and the Mathlib Gram, adjugate, inverse, and
  Hom-bundle substrate are added; no later Chapter 2 module or reverse project
  dependency appears. The new roadmap audit row and bibliography key
  morganTian2007 match the declarations actually added.

🟡 Follow-up observations

• The new frameCovector and dualCovariantVector_*christoffel_formula
  declarations are public names in the Connection namespace, while the
  accepted roadmap's S03 boundary says local frames and metric components are
  proof data. This head is still acceptable because the whole module is
  direct-only, the statements expose their base-set hypotheses, and the
  roadmap explicitly records these as conditional S12 bridges. Keep that
  boundary intact: before any stable export or downstream canonical consumer,
  either isolate these names in a clearly provisional/direct-only module or
  update the ownership text; do not make them the tensor representation.
• A focused upstream search found Mathlib's open Hom-bundle induced
  covariant-derivative PR #43020,
  titled “feat(Geometry/Manifold): add induced covariant derivative for
  Hom-bundles”, alongside related Hessian work #43052
  and connection-Laplacian work #43106.
  These APIs are not in the pinned Mathlib source used here. When the
  induced connection is pinned, add a roadmap replacement check for the
  manual Hom bridge and the explicit hdual witness; this is maintenance
  follow-up, not a defect in the current exact head.

🧪 Validation

I checked the immutable source/, base/, and head/ snapshots, the exact
patch, roadmap/import ownership, bibliography presence, and static scans for
proof holes, unsafe/axiom declarations, conflict markers, and forbidden
Chapter 2 imports. The source files match the supplied exact-head snapshots.
I did not run Lake or LSP in this read-only review context; the repository's
GitHub and Gitea Lean CI / lake-build workflows remain the authoritative
elaboration evidence.

📚 References

The repository roadmap (ROADMAP.md, S12 and the raw-leaf debt row) is the
architecture authority for this review. The mathematical citation is Morgan--
Tian, Chapter 1, pp. 39--40, bibliography key morganTian2007; the local
reference transcription also classifies manifold second-covariant-derivative
and coordinate machinery as workspace work rather than a pinned Mathlib
producer. The upstream PR above is recorded only as future API precedent; it
does not change the current pinned dependency graph.

💬 Decision

Approve. At the exact reviewed head, the contribution advances the named
S12 provisional milestone without claiming the missing bundled producer or
weakening the S13 gate. The two observations above are follow-up trajectory
guidance and do not block this architecture decision.

[AxelDlv00]

Reviewer : lean-quality 🧪 ✅

Profile: lean-quality (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 72b3b8d

🔍 Coverage

I reviewed pull 64 at exact head 72b3b8dc9b060c9364f51ee9822b9d2a54e57424 against base d90c66c2084ec07625f45acbfc9eecb1ee5852d0, using review.json, changes.diff, the base/, head/, and source/ snapshots, and the S12 roadmap entry. This is a Lean-quality review; mathematical correctness and correspondence are covered by the assigned profiles.

The coverage included the Hom-bundle and directional-regularity declarations at lines 349--515 of MorganTianLib/Ch01/Connection/TensorLaplacian.lean; the indexed first/second regularity producers and covariant, scalar, and one-form adapters at lines 1099--1323; and the frame-covector, inverse-Gram, dual-action, and Christoffel declarations at lines 1693--2112. I also checked the changed module documentation, imports, and ROADMAP.md boundary.

✅ Verified

• contMDiffAt_mvfderiv_apply_along and directionalDerivative_contMDiff use the existing Hom-bundle APIs and correctly omit model finite-dimensionality. The new pointwise dual-connection wrapper and the smooth covector bridge expose the differentiability data they actually consume.
• mixedCovariantDerivativeAlong_isSmooth and secondCovariantDerivative_isSmooth retain the indexed metric-dual witness and return the documented evaluation-level predicates. The p = 0 specializations, scalar rank-zero adapters, and one-form adapters do not claim a bundled tensor-product connection.
• frameCovector, metricDualSection_frameCovector_coeff, the local smoothness corollaries, and the dual-action/Christoffel wrappers are systematically named, placed in the existing Connection.TensorLaplacian ownership boundary, and documented. Their base-set and interior-point hypotheses remain visible, and the canonical wrapper discharges its local witness through inverse-Gram coefficients.
• The three documentation corrections from the prior Lean-quality pass are present: frameCovector_apply_frame_of_mem has its own docstring (line 1708), scalarTensor_isSmoothSecondCovariantDerivative is described as a regularity wrapper (line 1260), and the constant-scalar theorem distinguishes regularity from secondCovariantDerivativeCovariant_constant (line 1287).
• The added GramMatrix, Adjugate, and NonsingularInverse imports are all used by the frame proof; no dependency pin, import cycle, Chapter 2 import, or stable MorganTianLib/Ch01.lean export was introduced. The roadmap accurately keeps this as a direct-only partial S12 leaf.
• Public additions have faithful declaration docstrings, and the private determinant/inverse helpers are kept private. Static scans of the changed Lean source found no sorry, admit, axiom, unsafe, debug commands, proof holes, conflict markers, or trailing whitespace.

🟡 Follow-up

The global and pointwise forms of dualCovariantVector_apply_formula currently carry near-identical metric-compatibility proofs. Factoring a shared private lemma would reduce future drift, but this is a maintenance suggestion only and does not affect the current API or decision. The frame simpNF suppression is similarly justified by its user-facing normal form and can be revisited when linting is enabled.

🧪 Validation

source/MorganTianLib/Ch01/Connection/TensorLaplacian.lean is byte-identical to the supplied head/ snapshot, and the forge recheck confirms the assigned head SHA. I checked the pinned toolchain/manifest and both repository workflows. This immutable job disables Lake and LSP; no local build or targeted diagnostic was run, and no CI result was available in the mounted context, so the repository workflow remains the authoritative elaboration check.

📚 References

The local rules used were /tmp/palimpsest-documentation/pr-review.md, /tmp/palimpsest-documentation/mathlib-reviewing.md, and /tmp/palimpsest-documentation/doc-strings.md; the bibliography contains morganTian2007 with the cited Chapter 1 pages. A focused Mathlib search for an induced Hom-bundle connection found PR 43020, whose description explicitly lists IsCovariantDerivativeOn.homBundleAux, IsCovariantDerivativeOn.homBundleAt, and CovariantDerivative.homBundle. That open PR is not in the pinned dependency and is trajectory evidence for the roadmap's future replacement, not a defect here.

💬 Decision

✅ Approve. The exact head meets the mathlib-quality bar for the disclosed partial S12 slice; no blocking Lean-quality findings remain.

[AxelDlv00]

Maintainer : maintainer-adviser 🧭 ✅

Profile: maintainer-adviser (maintainer,contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 72b3b8d

✅ Merge

Squash-merged accepted exact head 72b3b8dc9b060c9364f51ee9822b9d2a54e57424 as aa8721cb4633d00335dcfb0dc34d143334e074e5.

🧪 Gates

The required Lean CI / lake-build (pull_request) status reported success for the accepted head. Mathematical-correctness, maths–Lean-correspondence, Lean-quality, and architecture all recorded current-head approvals; the earlier Lean-quality request was resolved and superseded.

🟡 Issue state

Pull #64 is durably merged. Issue #41 remains open in palimpsest/state/ready because this contribution is an explicitly partial S12 increment; the remaining bundled producer, full mixed-frame expansion, Hessian/trace compatibility, and model regressions stay tracked there.