Ablate availability, not mathematical truth

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 target modules that have an import path to the removed module in this snapshot. Does this prove that their mathematical conclusions cannot be proved without it?

Targets: AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL, AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity

Removed module: AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic

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.

Reachability reports snapshot import availability only. No Lean module was removed, and the result does not establish that either mathematical conclusion is unprovable without that module or unavailable from another proof.

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-g003",
  "core_id": "sogb-002",
  "family": "pl-gradient-iteration",
  "title": "Ablate availability, not mathematical truth",
  "library_domains": [
    "optimisation"
  ],
  "track": "graph-json",
  "level": "L1",
  "split": "public-dev",
  "skills": [
    "graph-ablation",
    "semantic-boundary"
  ],
  "question": "List the target modules that have an import path to the removed module in this snapshot. Does this prove that their mathematical conclusions cannot be proved without it?",
  "targets": [
    "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL",
    "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity"
  ],
  "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"
  },
  "remove": "AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic",
  "binding_sha256": "a9892ad7b6fa718bd9689428537db01018f60aa8aab09ca7fb393e9b2b3bc6cf"
}

Reference structural answer · 2 checks, 1 point

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