Combine a proof path with an exact statement profile

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 only targets that BOTH have a directed path to the indicated interface AND contain every requested constant in their supplied unexpanded-statement profile. This is a structural/type-occurrence filter, not proof of necessary hypotheses or that other targets lack a genuine gradient.

Targets: Actual flow rate, Strong-convex model, 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.

Statement-occurrence filter

Requested constants: CompleteSpace, HasGradientAt.

Direct constant occurrences in the unexpanded elaborated statement; not a binder-role analysis, inferred hypothesis list or full type dependency closure. Absence here does not mean absence after unfolding or proof derivation.

Selected declaration	Emitted direct constants
Actual flow rate	`CompleteSpace`, `Differentiable`, `HasDerivWithinAt`
Strong-convex model	`CompleteSpace`, `HasGradientAt`
Gradient pairing bound	`CompleteSpace`, `HasGradientAt`
Curve slope limit	`HasDerivAt`
Midpoint envelope	None of the whitelisted constants; not a claim of no assumptions.

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.

A positive path and a matching direct type profile jointly certify only these two structural predicates, not that either constant or theorem is a necessary mathematical premise.
Missing HasGradientAt in value_le's direct profile is not absence after definition unfolding or proof derivation. Missing midpoint reachability is not a full-closure independence certificate. Private auxiliaries, unselected constants and Mathlib parents remain omitted.

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-g007",
  "core_id": "sogb-023",
  "family": "convex-flow-first-order-rate",
  "title": "Combine a proof path with an exact statement profile",
  "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.firstOrder_lower_bound_of_strongConvexOn",
    "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn",
    "AutoSamplingTheory.TechnicalLemmas.Geometry.StrongConvexity.centered_quadratic_lower_bound_of_strongConvexOn_minimizer"
  ],
  "question": "List only targets that BOTH have a directed path to the indicated interface AND contain every requested constant in their supplied unexpanded-statement profile. This is a structural/type-occurrence filter, not proof of necessary hypotheses or that other targets lack a genuine gradient.",
  "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",
  "required_statement_constants": [
    "CompleteSpace",
    "HasGradientAt"
  ],
  "binding_sha256": "7ab244e584039fe810507f7cc78c61e7e739e183db1fb96ce5286054dd9ffa18"
}

Reference structural answer · 2 checks, 1 point

{
  "nodes": [
    "AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn",
    "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.