Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Bench / geometry

sogb-005 · public-dev · editorial and formal status separate

Why a sphere gradient is a projected ambient gradient

Riemannian Optimisation · natural-language: L3 (author-assigned; calibration pending)

Why this difficulty?

Connect a derivative, an adjoint and an orthogonal projection, then diagnose the failure of the unit-normal convention.

Editorial review and exact formal-coverage boundary

AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

  • No aligned formal view is admitted. The weaker single-point regularity formulation, nonunit counterexample/correction and explanatory identification with the sphere's induced metric are not certified as a full QA translation by the stronger bundled local theorem.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

  • E,H are real Hilbert spaces. \(F:E\to H\) is Fréchet differentiable at w, with bounded linear derivative D(w). Fix \(r\in H\) and V(w)=2⟨r,F(w)⟩.
  • Assume \(\|w\|=1\) and \(\|D(w)\|\le M\) with \(M\ge 0\). The tangent space of the unit sphere at w is {v:⟨w,v⟩=0}.

Natural-language question

Set g=2D(w)*r and \(G=g-⟨g,w⟩w\). Prove tangency, the directional-derivative identity on tangent vectors and \(\|G\|\le 2M\|r\|\). Explain precisely why the same formula need not project onto w-perpendicular when w is not a unit vector.

Reference mathematical proof

  1. The chain rule and the adjoint identity give DV(w)[v]=2⟨r,D(w)v⟩=⟨g,v⟩. This uses genuine differentiability, not an assertion about a default derivative value.

  2. Since \(\|w\|^{2}=1\), \[\langle w,G\rangle=\langle w,g\rangle-\langle g,w\rangle\|w\|^2=0.\] For v perpendicular to w, ⟨G,v⟩=⟨g,v⟩=DV(w)[v], which identifies the sphere gradient by the induced metric.

  3. The Pythagorean calculation gives \(\|G\|^{2}=\|g\|^{2}-⟨g,w⟩^{2}\le \|g\|^{2}\). Hence \(\|G\|\le \|g\|\le 2\|D(w)*\|\|r\|=2\|D(w)\|\|r\|\le 2M\|r\|\).

  4. Without normalization, \(⟨w,G⟩=⟨g,w⟩(1-\|w\|^{2})\). For example, take \(E=\mathbb{R}\), \(w=2\) and \(g=2\): \(G=-6\) is not perpendicular to w. For a nonzero general normal, the projector instead divides the coefficient by \(\|w\|^{2}\). This is not a formula for an arbitrary manifold without its own tangent and metric data.

Formal support and missing Lean alignment

The existing bundled theorem proves a stronger regularity package. It is support, not a frozen equivalent task for this shorter question and its counterexample.

Assessment rubric · 4 points
  1. Derives the ambient derivative using the chain rule and adjoint, with genuine differentiability. (1 point)
  2. Uses the unit-normal condition to prove tangency and the tangent directional identity. (1 point)
  3. Proves the norm bound by orthogonal projection and the adjoint operator norm. (1 point)
  4. Gives a valid nonunit counterexample and states the correction and manifold boundary. (1 point)

Lean view: not yet aligned

The existing bundled theorem proves a stronger regularity package. It is support, not a frozen equivalent task for this shorter question and its counterexample.

This support theorem does not certify the complete QA or its explanatory counterexamples.

What this does—and does not—verify

Only the unit sphere with its induced metric is treated. No general Riemannian gradient theorem, retraction guarantee or optimization convergence result is asserted.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Original exercise over the local quadratic-feature tangent-gradient theorem and elementary Hilbert-space algebra.

Exact local source and full context · Locate the existing Lean declaration

AutoSamplingTheory.TechnicalLemmas.Geometry.QuadraticFeatureTangentGradient.quadratic_feature_potential_tangent_gradient

ASTIS formal support (not an equivalent QA)

  • AutoSamplingTheory.TechnicalLemmas.Geometry.QuadraticFeatureTangentGradient.quadratic_feature_potential_tangent_gradient

Mathlib facts / definitions

  • ContinuousLinearMap.adjoint_inner_left
  • ContinuousLinearMap.adjoint.norm_map
  • norm_sub_sq_real

Binding SHA-256: ce37724e97b715e2330e57378f5795759da21f91c6f477b863d897b48fe93f74