Framework Axioms

Some theorems come from the rest of mathematics. Verum lets you postulate them as axioms while keeping the trusted boundary absolutely explicit — every external result a proof relies on appears by name and citation in verum audit --framework-axioms, and every exported .verum-cert carries the same dependency list.

Why framework axioms exist

Not every theorem can, or should, be re-proved from first principles.

• HTT 6.2.2.7 (Lurie's Higher Topos Theory) states that the ∞-category of sheaves on a small ∞-site is an ∞-topos. No mechanised proof of HTT exists in any proof assistant today.
• Connes 2008 axiom (vii) (the first-order condition in Connes–Chamseddine's spectral-triple reconstruction theorem) is a well-known 7-axiom package; nobody has mechanised the surrounding reconstruction proof either.
• Petz 1996 classifies monotone metrics on matrix spaces — again known but not mechanised.

Refusing to proceed until every such result is re-proved from bare type theory would make formalisation of non-toy physics/maths infeasible. Pretending the results are local to the proof would make the trusted boundary invisible to external reviewers.

Verum's resolution is a typed attribute: declare the dependency explicitly, at the axiom, with a citation you can look up.

Declaring a framework axiom

The syntax is an ordinary attribute on an axiom (or any theorem / lemma / corollary you want to mark as depending transitively on an external result):

@framework(lurie_htt, "HTT 6.2.2.7")
axiom sheafification_is_topos<C: Site>(c: C) -> Bool
    requires c.is_presentable()
    ensures  c.sheafification().is_infinity_topos();

@framework(connes_reconstruction, "Connes 2008 axiom (vii)")
axiom first_order_condition<A>(spectral_triple: A) -> Bool
    ensures spectral_triple.first_order_holds();

@framework(petz_classification, "Petz 1996 monotone metrics")
axiom petz_monotone<N: Nat>(rho: DensityMatrix<N>) -> Bool
    ensures rho.is_monotone_under_cptp();

Two arguments, always in this order:

1. A framework identifier — short, machine-readable, snake_case. Convention: match the file under core/math/frameworks/<name>.vr where the framework's full axiom package lives. The stdlib ships eleven canonical packages today; the right-hand column says how many axioms ship in each:

   Identifier	Source	Stdlib file	Axioms
   lurie_htt	Lurie, Higher Topos Theory (2009)	core/math/frameworks/lurie_htt.vr	8
   schreiber_dcct	Schreiber, Differential Cohomology in a Cohesive ∞-Topos (arXiv:1310.7930)	core/math/frameworks/schreiber_dcct.vr	5
   connes_reconstruction	Connes (2008) + Connes 2013 Theorem 1.1	core/math/frameworks/connes_reconstruction.vr	8
   petz_classification	Petz, Monotone metrics on matrix spaces (1996)	core/math/frameworks/petz_classification.vr	4
   arnold_catastrophe	Arnold (1972) + Arnold–Mather (1974) codim ≤ 4	core/math/frameworks/arnold_catastrophe.vr	8
   baez_dolan	GPS (1995), Baez–Dolan (1995), Lurie (2009)	core/math/frameworks/baez_dolan.vr	4
   diakrisis	Diakrisis foundational theorems (108.T α/ε duality core)	core/math/frameworks/diakrisis.vr	6
   diakrisis_acts	Diakrisis Acts roster (Articulation Calculus actions)	core/math/frameworks/diakrisis_acts.vr	16
   diakrisis_biadjunction	Diakrisis biadjunction theorems	core/math/frameworks/diakrisis_biadjunction.vr	2
   diakrisis_extensions	Diakrisis foundational extensions	core/math/frameworks/diakrisis_extensions.vr	4
   diakrisis_stack_model	Diakrisis stack-model theorems	core/math/frameworks/diakrisis_stack_model.vr	6

   71 framework axioms across 11 frameworks ship in the stdlib today (verified via grep -c "@framework(" core/math/frameworks/*.vr). Adding a new framework is a matter of dropping a new file into core/math/frameworks/ and citing it from proofs. The audit CLI discovers them automatically; verum audit --framework-axioms enumerates the full inventory.

   Each stdlib file follows a common shape:

   • a carrier protocol (e.g. Site, InfinityTopos, SpectralTriple, OperatorMonotoneFunction, FunctionGerm, Tricategory) that witnesses the minimal algebraic data the axioms talk about;
   • one @framework(name, "citation") axiom per named theorem in the source work;
   • requires / ensures clauses carrying the precondition and the conclusion of each theorem so downstream apply-based proofs can actually consume them.

2. A citation — a free-form string literal. Be specific enough that an auditor can find the exact result: section number, theorem number, axiom name, page reference. Every stdlib-shipped axiom follows the pattern "<short-ref> (<short-description>)", e.g. "HTT 6.2.2.7", "DCCT §3.9 (cohesive hexagon)", "Connes 2008 axiom (vii) — Poincaré duality".

The attribute is grammar-legal via the generic attribute production identifier , [ '(' , attribute_args , ')' ] (see the Grammar reference — Visibility and attributes), and typed by verum_ast::attr::FrameworkAttr. A malformed @framework(...) (wrong arg count, non-string citation) is a reportable user error, not a silent acceptance.

Enumerating the trusted boundary

Before accepting a proof corpus for publication / audit / downstream use, every reviewer wants to see the exact set of external results it depends on. Verum emits that set on demand:

$ verum audit --framework-axioms

Framework-axiom trusted boundary
────────────────────────────────────────
  Parsed 42 .vr file(s), skipped 0 unparseable file(s).
  Found 12 marker(s) across 4 framework(s):

  ▸ connes_reconstruction (1 marker)
    · axiom first_order_condition  —  Connes 2008 axiom (vii)  (src/physics.vr)
  ▸ lurie_htt (5 markers)
    · axiom sheafification_is_topos  —  HTT 6.2.2.7      (src/category.vr)
    · axiom presentable_localization —  HTT 5.5.4.15     (src/category.vr)
    · axiom adjoint_functor_thm      —  HTT 5.5.2.9      (src/category.vr)
    · axiom kan_extension_universal  —  HTT 4.3.3.7      (src/category.vr)
    · axiom accessible_inf_cat       —  HTT 5.4.2        (src/category.vr)
  ▸ petz_classification (2 markers)
    · axiom petz_monotone           —  Petz 1996 monotone metrics (src/quantum.vr)
    · axiom uhlmann_fidelity        —  Petz–Uhlmann 1986          (src/quantum.vr)
  ▸ schreiber_dcct (4 markers)
    · axiom cohesive_hexagon         —  DCCT §3.9         (src/cohesive.vr)
    · axiom super_cohesion           —  DCCT §3.10        (src/cohesive.vr)
    · axiom rheonomy_modality        —  DCCT §3.12        (src/cohesive.vr)
    · axiom differential_cohesion    —  DCCT §4.1         (src/cohesive.vr)

• The tool walks every .vr file under the project root, skipping target/, hidden directories, node_modules/.

• Markers on axiom, theorem, lemma, and corollary declarations are all collected.

• Both Item.attributes and {Theorem,Axiom}Decl.attributes are walked, so attribute placement (outside the keyword vs inside the decl) does not affect visibility.

• Malformed @framework(...) attributes make the command exit non-zero, so CI can gate on "no hidden axioms":

  $ verum audit --framework-axioms
  ...
  ⚠  1 malformed @framework(...) marker(s) found:
    · src/bad.vr on missing_second_arg  —  expected @framework(<ident>, "<citation>")
  
  Error: 1 malformed @framework(...) attribute(s) — expected
    @framework(<ident>, "<citation>")
  $ echo $?
  1

Certificate export

When you export a proof to .verum-cert for independent checking (verum export --to {coq, lean, isabelle, dedukti, metamath}), the framework-axiom dependency list is carried along in the certificate envelope. External tooling consuming the certificate must either:

• supply the cited framework axioms in the target system (a Coq importer can re-emit them as Axiom ...), or
• reject the certificate as "depends on axiom set X that the local environment does not admit".

Either way the dependency is surfaced, not silent.

Stratified theorem tags

For corpora that distinguish rigorous from framework-conditional from stratified theorems, the workflow is:

1. A rigorous-core theorem has no @framework on itself and depends only on axioms marked @framework. The proof is as strong as the cited results.
2. A framework-conditional theorem carries its own @framework marker, so consumers see immediately that it is conditional on X.
3. A stratified theorem lists every relevant marker and the audit output makes the stratification a simple grep.

The convention: every theorem's trusted base is visible to any reviewer in seconds, and provenance never leaks.

Interaction with the trusted kernel

@framework axioms are registered in the kernel's AxiomRegistry with their FrameworkId { framework, citation } attribution. The kernel's LCF-style checker (see Architecture → trusted kernel) treats them as black-box postulates: a use of sheafification_is_topos elaborates to a CoreTerm::Axiom { name, ty, framework } node, and the kernel accepts it only if the axiom name is in the registry and its declared type matches.

This is the explicit counterpart to the implicit trust most proof assistants carry: axioms are not in the library by default; you have to register them, and every registration is enumerable.

The IOU axiom registry — kernel-rule trust extension

@framework axioms above are user-facing mathematical postulates. There is a second, distinct trust-extension surface inside the kernel itself: the IOU axiom registry, which tracks how each of the kernel's own canonical inference rules is discharged.

Every canonical kernel rule (canonical_rules() enumerates 38 — K_Var, K_Univ, K_Pi_Form, K_Lam_Intro, K_App_Elim, K_Sigma_Form, K_Pair_Intro, K_Fst_Elim, K_Snd_Elim, K_Path_Ty_Form, K_Refl_Intro, K_Path_Over_Form, K_HComp, K_Transp, K_Glue, K_Refine_Erase, K_Refine, K_Refine_Omega, K_Refine_Intro, K_Quot_Form, K_Quot_Intro, K_Quot_Elim, K_Inductive, K_Pos, K_Elim, K_Smt, K_FwAx, K_Eps_Mu, K_Universe_Ascent, K_Round_Trip, K_Epsilon_Of, K_Alpha_Of, K_Modal_Box, K_Modal_Diamond, K_Modal_Big_And, K_Shape, K_Flat, K_Sharp) carries a LemmaStatus (crates/verum_kernel/src/soundness/mod.rs::LemmaStatus) with one of three values:

Status	Meaning	Audit-clean?
Proved	A real proof exists in proof_checker.rs's Typing constructor + lean.rs / coq.rs / isabelle.rs / agda.rs exporters	yes
DischargedByFramework	Discharged by a vetted upstream proof (mathlib4, lean4_stdlib, CCHM, Mac Lane Theorem IV.7.3, etc.) with lemma_path, framework, citation fields	yes (L4-acceptable)
Admitted	Open obligation — the rule's soundness lemma is admitted in the per-foundation export (sorry in Lean, Admitted. in Coq, per-rule axiomatization where K_<n>_sound: "..." in Isabelle, postulate in Agda)	no

Current registry state: every canonical kernel rule is either Proved (full structural proof in Lean / Coq + per-rule apply (rule T_<n>) axiomatization-fact discharge in Isabelle

• shape-checked postulate in Cubical Agda) or DischargedByFramework (cited upstream proof). No rules sit at Admitted — see crates/verum_kernel/src/soundness/mod.rs::iou_axiom_specs(), which returns vec![]. Adding a brand-new rule that hasn't yet been proved is allowed (it lands as Admitted plus an iou_axiom_specs entry), but the audit gate flips to failure as soon as that happens — Admitted is never the steady-state.

Consequently #print axioms kernel_soundness (Lean) / Print Assumptions kernel_soundness. (Coq) / print_facts kernel_full_soundness (Isabelle) on the exported soundness corpus enumerates exactly the framework citations — every other constructor's discharge is structural.

The --trust-extension-report audit gate

$ verum audit --trust-extension-report
Trust extension report
────────────────────────────────────────

  ▸ Proved:
      K_Var, K_Univ, K_Pi_Form, K_Lam_Intro, K_App_Elim,
      K_Sigma_Form, K_Pair_Intro, K_Fst_Elim, K_Snd_Elim,
      K_Refine, K_Refine_Intro, K_Path_Ty_Form, K_Refl_Intro,
      K_Path_Over_Form, K_HComp, K_Transp, K_Glue,
      K_Quot_Form, K_Quot_Intro, K_Inductive,
      K_Pos, K_Elim, …

  ▸ DischargedByFramework:
      · K_Pi_Form          mathlib4              CategoryTheory.Adjunction
      · K_Lam_Intro        mathlib4              CategoryTheory.Adjunction
      · K_App_Elim         mathlib4              CategoryTheory.Adjunction
      · K_Sigma_Form       mathlib4              CategoryTheory.Limits.Sigma
      · K_Pair_Intro       mathlib4              CategoryTheory.Limits.Sigma
      · K_Fst_Elim         mathlib4              CategoryTheory.Limits.Sigma
      · K_Snd_Elim         mathlib4              CategoryTheory.Limits.Sigma
      · K_Eps_Mu           Mac Lane              Categories for the Working Mathematician, Theorem IV.7.3
      · K_Round_Trip       Verum-internal        bridge-audit specification

  ▸ Admitted:
      (none — the IOU registry is empty)

Trust extension surface: framework citations only; no open IOUs.

A new Admitted entry — i.e. a kernel rule whose soundness lemma is sorry-equivalent in the export — flips this gate to failure. The discipline ensures every load-bearing meta-theory dependency is enumerable from the kernel itself, with the same "@framework(name, citation) audit shape" as user-facing axioms.

Adding or rewinding an IOU

Removing a DischargedByFramework entry by promoting it to Proved requires landing the corresponding structural proof in proof_checker.rs's Typing inductive and the per-foundation exporters; the audit gate's drift_check cross-validates that the per-rule LemmaStatus in mod.rs agrees with both canonical_rules() and iou_axiom_specs().

Re-introducing an Admitted entry (when a brand-new kernel rule is added that we haven't yet proved) requires the inverse: register it in iou_axiom_specs() with its arity and citation comment, and revert the per-foundation Typing constructor's structural premises to the IOU-hypothesis form. The drift check catches half-completed transitions.

Four foundations agree

The IOU registry status is exported in lock-step to all four foundations: Lean 4 (verification/external/lean/), Coq / Rocq (verification/external/coq/), Isabelle/HOL (verification/external/isabelle/), and Cubical Agda (verification/external/agda/). The export pipeline walks iou_axiom_specs() once and emits the same structured citation in each foundation's syntax via render_iou_axioms_lean() / _coq() / _isabelle() / _agda() — axiom <Rule>_iou in Lean, Axiom <Rule>_iou in Coq, axiomatization … <Rule>_iou blocks in Isabelle, and postulate <Rule>_iou : Ctx → … → Set blocks in Cubical Agda. Cross-foundation disagreement on a rule's discharge status is structurally impossible — the registry is the single source of truth. Drift between the four foundations' emitted text is closed by construction: every backend's IOU block is a cached projection of the same iou_axiom_specs() walk.

Worked example — bridging two proof systems

// File: src/categorical/grothendieck.vr
mount core.math.frameworks.lurie_htt;

/// A Grothendieck site in the HTT sense.
public type Site is protocol {
    fn is_presentable(self) -> Bool;
    fn sheafification(self) -> SheafInfinityTopos;
};

/// The HTT 6.2.2.7 axiom — the headline result.
@framework(lurie_htt, "HTT 6.2.2.7")
axiom htt_6_2_2_7<C: Site>(c: C)
    requires c.is_presentable()
    ensures  c.sheafification().is_infinity_topos();

/// A theorem that consumes the axiom. Not itself marked with
/// @framework — it is rigorous in Verum *modulo* the registered
/// axiom, and the transitive dependency is visible to
/// `verum audit --framework-axioms`.
theorem bures_topology_is_topos(c: BuresSite) -> Bool
    requires c.is_presentable()
    ensures  c.sheafification().is_infinity_topos()
{
    proof by {
        apply htt_6_2_2_7;
    }
}

verum audit --framework-axioms on this file prints:

  ▸ lurie_htt (1 marker)
    · axiom htt_6_2_2_7  —  HTT 6.2.2.7  (src/categorical/grothendieck.vr)

— exactly the trusted-boundary information an external reviewer needs before accepting bures_topology_is_topos as a valid result.

See also

• Gradual verification — the section that introduces the attribute in the context of the 9-strategy spectrum.
• Architecture → trusted kernel — how AxiomRegistry::register plugs into the LCF check loop.
• Contracts — requires / ensures syntax used by axiom declarations.
• Proofs — applying axioms inside tactic scripts via apply.