Which convex-analysis branches reach the curve limit?

L2 · public-dev · structural QA, not a theorem proof

Read the source mathematical proof and optional Lean. This is context linkage, not an equivalent mathematical question.

List the target proofs with a directed path to the indicated interface in this supplied compiled-body slice. Does such a path prove mathematical necessity? A missing path here is not a full-closure independence certificate.

Targets: Actual flow rate, Gradient pairing bound, Midpoint envelope

Queried interface: Curve slope limit

Scroll horizontally on a small screen. Solid arrows: selected theorem constants occur in the compiled proof bodies, including proof-term annotations. Other constants and private auxiliaries are omitted; a missing path is not full-closure independence. Neutral colours make no proof-status claim.

Related exercises about selected statements: A quadratic envelope from one midpoint · From a selected-curve chord inequality to its first-order bound.

Independent structural review and limits

Current editorial status: accepted. This is AI review of structural QA, not a theorem or calibrated difficulty.

Compiled constant occurrence includes proof-term annotations and is not minimal premise dependence. An absent induced path for the midpoint does not prove full-closure independence or impossibility of a different proof using the interface.
The profiles are direct constants in unexpanded elaborated statements, not type-definition closure, binder-role classification or a list of necessary assumptions.

Exact review bindings and report hashes · Current independent review and explicit historical supersession

Evidence kind and source scope

This is a recorded source-bound compiler snapshot. CI separately replays the trusted extractor. It is not a fresh Lean run in this browser, a full proof closure or a minimal-premise certificate. Unique proof constants do not count runtime invocations, recursive calls or oracle queries.

Recorded compiler slice and provenance

An edge records constant occurrence in this compiled proof body, including proof-term annotations. Statement profiles record only whitelisted direct type-constant occurrences, not logical requirements. Neither certifies mathematical necessity or a full dependency closure. No path in an induced slice does not imply no path in the full closure.

Exact JSON snapshot and response schema

{
  "id": "sogb-g006",
  "core_id": "sogb-023",
  "family": "convex-flow-first-order-rate",
  "title": "Which convex-analysis branches reach the curve limit?",
  "library_domains": [
    "optimisation"
  ],
  "track": "graph-json",
  "level": "L2",
  "split": "public-dev",
  "skills": [
    "graph-reading",
    "semantic-boundary"
  ],
  "targets": [
    "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValue.value_le",
    "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn",
    "AutoSamplingTheory.TechnicalLemmas.Geometry.StrongConvexity.centered_quadratic_lower_bound_of_strongConvexOn_minimizer"
  ],
  "question": "List the target proofs with a directed path to the indicated interface in this supplied compiled-body slice. Does such a path prove mathematical necessity? A missing path here is not a full-closure independence certificate.",
  "context": {
    "direction": "theorem-to-selected-constant-in-compiled-proof-body",
    "edges": [
      [
        "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValue.value_le",
        "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn"
      ],
      [
        "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn",
        "AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity"
      ],
      [
        "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn",
        "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn"
      ]
    ],
    "kind": "compiled-proof-body-constant-occurrences",
    "node_labels": {
      "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValue.value_le": "Actual flow rate",
      "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn": "Strong-convex model",
      "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn": "Gradient pairing bound",
      "AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity": "Curve slope limit",
      "AutoSamplingTheory.TechnicalLemmas.Geometry.StrongConvexity.centered_quadratic_lower_bound_of_strongConvexOn_minimizer": "Midpoint envelope"
    },
    "nodes": [
      "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValue.value_le",
      "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn",
      "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn",
      "AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity",
      "AutoSamplingTheory.TechnicalLemmas.Geometry.StrongConvexity.centered_quadratic_lower_bound_of_strongConvexOn_minimizer"
    ],
    "scope": "induced public-theorem slice; unselected constants, private auxiliaries and Mathlib parents are omitted",
    "source_sha256_lf": {
      "AutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowValue.lean": "17ef3289cc2553d16fb00941203999fbac698adeb684833151b40c0b90e9dfd3",
      "AutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexFirstOrder.lean": "6efa3254bc53f8bd93423d56c79f38b90af35f0097e1223940c328861b336c17",
      "AutoSamplingTheory/TechnicalLemmas/Geometry/GeodesicConvexity.lean": "9ed8c8f65014e5494a8ae8a9c6afdbe4c5d628886505b86bc832895c0780b0ff",
      "AutoSamplingTheory/TechnicalLemmas/Geometry/StrongConvexity.lean": "4ff7d1a85259002e0a3f947ea509935eb9866bf3741daa361733ed041968f1f1"
    },
    "statement_constant_whitelist": [
      "CompleteSpace",
      "Differentiable",
      "HasDerivAt",
      "HasDerivWithinAt",
      "HasGradientAt"
    ],
    "statement_profile_scope": "Direct constant occurrences in the unexpanded elaborated statement; not a binder-role analysis, inferred hypothesis list or full type dependency closure.",
    "statement_profiles": {
      "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValue.value_le": [
        "CompleteSpace",
        "Differentiable",
        "HasDerivWithinAt"
      ],
      "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn": [
        "CompleteSpace",
        "HasGradientAt"
      ],
      "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn": [
        "CompleteSpace",
        "HasGradientAt"
      ],
      "AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity": [
        "HasDerivAt"
      ],
      "AutoSamplingTheory.TechnicalLemmas.Geometry.StrongConvexity.centered_quadratic_lower_bound_of_strongConvexOn_minimizer": []
    },
    "truth_boundary": "An edge records constant occurrence in this compiled proof body, including proof-term annotations. Statement profiles record only whitelisted direct type-constant occurrences, not logical requirements. Neither certifies mathematical necessity or a full dependency closure. No path in an induced slice does not imply no path in the full closure.",
    "snapshot_sha256": "c40480f0760e7fc74c6473d57fe2ca1596777501f6c757c93398f0f316d729e1",
    "provenance": {
      "context_sha256": "9fb4de23eadc561e0c7bc18ac2556160a1c0fa7925c348c636aa0f846311b2be",
      "core_binding_sha256": "4a0607efb0c7bf22a09cc2d1ced0f8033582c57fd04e0225279f2e0782d169dc",
      "core_id": "sogb-023",
      "generator_sha256_lf": "2f570810651543df28853b31847a0ba5b676675231febca78269a67cb13a9229",
      "lakefile_sha256_lf": "1757b85b37f0a68972791443e3a8da33fd97ede414732fabb8e7d747b070c51c",
      "local_import_closure_sha256_lf": {
        "AutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowValue.lean": "17ef3289cc2553d16fb00941203999fbac698adeb684833151b40c0b90e9dfd3",
        "AutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexFirstOrder.lean": "6efa3254bc53f8bd93423d56c79f38b90af35f0097e1223940c328861b336c17",
        "AutoSamplingTheory/TechnicalLemmas/Geometry/GeodesicConvexity.lean": "9ed8c8f65014e5494a8ae8a9c6afdbe4c5d628886505b86bc832895c0780b0ff",
        "AutoSamplingTheory/TechnicalLemmas/Geometry/LogConcavity.lean": "671a445ebc61dc54dd234b0d24158369bc5f5846ea896069f920f85fcd54bb9b",
        "AutoSamplingTheory/TechnicalLemmas/Geometry/StrongConvexity.lean": "4ff7d1a85259002e0a3f947ea509935eb9866bf3741daa361733ed041968f1f1"
      },
      "mathlib_manifest_sha256_lf": "b83ca83b9cf7caa85fa8b023c2ff9a3fb7a7cce7e1c332e810c348535ec49c37",
      "selection_sha256": "6828e5c9611f0ea2e1ae9a4269c23a5a4cd6c89c3f6356f200073de72c9dc363",
      "source_sha256_lf": {
        "AutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowValue.lean": "17ef3289cc2553d16fb00941203999fbac698adeb684833151b40c0b90e9dfd3",
        "AutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexFirstOrder.lean": "6efa3254bc53f8bd93423d56c79f38b90af35f0097e1223940c328861b336c17",
        "AutoSamplingTheory/TechnicalLemmas/Geometry/GeodesicConvexity.lean": "9ed8c8f65014e5494a8ae8a9c6afdbe4c5d628886505b86bc832895c0780b0ff",
        "AutoSamplingTheory/TechnicalLemmas/Geometry/StrongConvexity.lean": "4ff7d1a85259002e0a3f947ea509935eb9866bf3741daa361733ed041968f1f1"
      },
      "toolchain": "leanprover/lean4:v4.33.0"
    }
  },
  "graph_sha256": "48f41f83f7af69425c3b942738af46158867d912f5134cbd270830d0cbb8abe8",
  "answer_schema": {
    "nodes": "list of distinct declaration ids; order ignored by scorer",
    "entails_mathematical_necessity": "boolean; whether this evidence certifies mathematical necessity"
  },
  "remove": "AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity",
  "binding_sha256": "1d7babdd58a789f902c03fe78d35e07c2e2e89a353569f1a1c1bf7631b94c7c4"
}

Reference structural answer · 2 checks, 1 point

{
  "nodes": [
    "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValue.value_le",
    "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn"
  ],
  "entails_mathematical_necessity": false
}

One point requires both the exact structural node set and a false mathematical-necessity certification. The constant boundary answer earns no standalone credit. Edges have only the stated evidence kind. Neither a positive path nor an absent induced path proves mathematical necessity or full-closure independence.

No model score, theorem-equivalence certificate or calibrated difficulty is asserted.