/-
  Custody-Class: PUBLIC-SHIPPED
  Surface-Role: STABLE-SURFACE

  Exact public Calculus root. Its transitive closure intentionally owns all
  four PathVerdict sources (`Core`, `Edges`, `Domains`, `Located`). Rung 1
  added `Domains` and `Located`; their 36 receipts remain separately gated.
  The Calculus-native 191-receipt inventory begins with the governed-family
  signature (rung 2 of
  the Admissibility Calculus promotion campaign, admitted 2026-07-17), its
  first two instances — static Weathering and the two-claim
  BoundedPaidReachability (rung 3, admitted 2026-07-17) — the exact
  refusal-packet spine with both instance adapters (rung 4, admitted
  2026-07-18), the indexed comparison framework (rung 5, admitted
  2026-07-18; the concrete seven-entry ledger remains receipt-bound
  research-tree evidence), the stored-decision crossing with its
  Weathering/bounded-paid inhabitant (rung 6, admitted 2026-07-18), and
  the origin/history-bound BreakGlass terminal instance (rung 7, admitted
  2026-07-18; closed relative to consumer-supplied Atoms, with the
  explicit Quot.sound/Classical.choice-over-opaque-substrate footprint
  accepted at ratification).

  `Admissibility.Calculus` is the ratified namespace of the
  **Admissibility Calculus**.  All seven campaign rungs are admitted, and
  the capital-C naming claim was separately ratified on 2026-07-18 as its
  own reviewed act (research-tree record
  ADMISSIBILITY_CALCULUS_CAPITAL_C_RATIFICATION_2026-07-18.md, pinned to
  custody base 62ac346b1fdc).  The name attaches to the exact
  custody-closed object; it is not by itself a runtime-conformance or
  completeness claim. A runtime claiming correspondence must declare its
  exact scope, map every governed type/book/decision and transport boundary in
  that scope, and provide executable preservation and transport evidence with
  revision-bound qualification receipts. A formal refinement proof may
  strengthen covered obligations but does not waive those artifacts.
-/

import LeanProofs.Admissibility.Calculus.Core
import LeanProofs.Admissibility.Calculus.Instances.Weathering
import LeanProofs.Admissibility.Calculus.Instances.BoundedPaidReachability
import LeanProofs.Admissibility.Calculus.Instances.Weathering.Spine
import LeanProofs.Admissibility.Calculus.Instances.BoundedPaidReachability.Spine
import LeanProofs.Admissibility.Calculus.Comparison
import LeanProofs.Admissibility.Calculus.Crossing
import LeanProofs.Admissibility.Calculus.Instances.WeatheringBoundedPaidCrossing
import LeanProofs.Admissibility.Calculus.Instances.BreakGlass
import LeanProofs.Admissibility.Calculus.Instances.BreakGlass.Spine
import LeanProofs.Admissibility.Calculus.Instances.BreakGlass.Comparison
import LeanProofs.Admissibility.Calculus.Instances.BreakGlass.Crossing