Read a local import edge

L1 · 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 direct imported modules of the target within the supplied induced slice.

Targets: AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL

Scroll horizontally on a small screen. Dashed arrows: source-scanned imports in the supplied slice. The shared module occurs once. Neutral colours make no proof-status claim.

Independent structural review and limits

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

This is source-scanned import availability, not a compiled proof-use edge, a full library dependency closure or a certificate that Basic is mathematically indispensable.

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

Evidence kind and source scope

This graph scans source import declarations, not theorem proof bodies.

Syntactic import availability only; not theorem implication or mathematical necessity.

Exact JSON snapshot and response schema

{
  "id": "sogb-g001",
  "core_id": "sogb-002",
  "family": "pl-gradient-iteration",
  "title": "Read a local import edge",
  "library_domains": [
    "optimisation"
  ],
  "track": "graph-json",
  "level": "L1",
  "split": "public-dev",
  "skills": [
    "graph-reading",
    "semantic-boundary"
  ],
  "question": "List the direct imported modules of the target within the supplied induced slice.",
  "targets": [
    "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL"
  ],
  "context": {
    "kind": "source-scanned-module-imports",
    "direction": "consumer-to-imported-module",
    "scope": "induced slice only; omitted imports are not absent from the whole library",
    "nodes": [
      "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic",
      "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL",
      "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity"
    ],
    "edges": [
      [
        "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL",
        "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic"
      ],
      [
        "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity",
        "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic"
      ]
    ],
    "source_sha256_lf": {
      "AutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentBasic.lean": "3489a169bf3cc4f17f4ba374a2edb1536f9cd5cfdfe67ce57ebbeacca65b1eef",
      "AutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentPL.lean": "382c8a5ba9dae70074114a205eb03c44826cb03c9b20c0f64931ced25fd9bea2",
      "AutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentStationarity.lean": "153f0d676936653c97320261b5a3b3d141346653566b13874ed85acf495c0513"
    },
    "truth_boundary": "Syntactic import availability only; not theorem implication or mathematical necessity."
  },
  "graph_sha256": "f900acfd86cb9fe6e0cc461bdedc4554ae121da215eb96598f1052f6aa1b0a97",
  "answer_schema": {
    "nodes": "list of distinct module ids; order ignored by the scorer",
    "entails_mathematical_necessity": "boolean; whether this evidence certifies mathematical necessity"
  },
  "binding_sha256": "cf66ca781a920db13e9115cab4ecde73e0139379595c74b6eec2747411b2c425"
}

Reference structural answer · 2 checks, 1 point

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