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

Bench / geometry

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

Which space contains the sphere gradient?

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

Why this difficulty?

Identify the tangent-vector domain and metric-dependent gradient characterization before carrying out a projection proof.

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 Lean view is admitted for the general smooth-function sphere-gradient definition, tangent-space construction, uniqueness argument, dependence only on the restriction, or the explanatory ambient-versus-tangent comparison. The local feature identities are supporting instances, not certification of the entire QA.

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

Assumptions and conventions

  • S is the unit sphere in \(\mathbb{R}^{d}\) with \(d\ge 2\), equipped with its induced Euclidean metric. A real-valued function f is smooth on a neighborhood of S. Let \(w\in S\).

Natural-language question

Identify the tangent space at w and the defining directional-derivative identity for the gradient of f restricted to S. In what sense does this differ from the ambient Euclidean gradient? Do not prove an optimization convergence theorem.

Reference mathematical proof

  1. The tangent space is \[T_wS=\{v\in\mathbb R^d:\langle w,v\rangle=0\}.\] Its vectors are ambient vectors subject to an orthogonality condition.

  2. The sphere gradient is the tangent vector G satisfying ⟨G,v⟩=Df(w)[v] for every \(v\in T_{wS}\), using the induced inner product.

  3. The ambient gradient represents derivatives in all ambient directions; it need not itself be tangent. Its orthogonal projection onto \(T_{wS}\) represents the same derivative on the allowed tangent directions.

  4. This is the induced-metric sphere setting. Other manifolds and metrics need their own tangent spaces and gradient characterizations, not an automatic reuse of an ambient formula.

Formal support and missing Lean alignment

The local theorem verifies this characterization for a specific feature potential. It is not a complete formalization of this general introductory definition QA.

Assessment rubric · 4 points
  1. States the tangent space as the orthogonal complement of the unit normal w. (1 point)
  2. Places G in the tangent space and quantifies the derivative identity over tangent directions. (1 point)
  3. Distinguishes ambient directions from induced-metric tangent directions. (1 point)
  4. Keeps the sphere/metric setting explicit without claiming arbitrary-manifold or convergence results. (1 point)

Lean view: not yet aligned

The local theorem verifies this characterization for a specific feature potential. It is not a complete formalization of this general introductory definition QA.

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

What this does—and does not—verify

No general manifold gradient API, retraction theorem, curvature comparison or optimization rate is claimed.

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 induced-sphere-metric definition exercise, supported by the existing feature-gradient instance.

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)

    Mathlib facts / definitions

      Binding SHA-256: a5cda7d4b9f7caaf24bf4dbab8205dae1f0a82e2ebb6b9fdc92d81c748863408