The @[cites] attribute

Binds a Lean declaration to a statement in a paper, by a key that a human minted and that contains no corpus-derived bytes.

@[cites "stmt:9f4c1a20b7d3:bridgeland2007.lem-8.2" (relation := one_way)
        (frontier := ["gltilde-universal-cover"])]
theorem foo : ... := ...

Why the key looks like that

stmt:<12 hex>:<label>. The 12 hex digits are a registry id minted once per topic repo; the label is chosen by the person writing the registry entry.

The paper coordinate — arXiv id, version, printed number — is deliberately not in the key. It lives in typed fields of the registry entry, so that a textbook: source with no arXiv version is expressible and no tokenizer can be broken by an id that itself contains a colon (math/0212237 is fine; a DOI is not). Nothing a corpus computes appears here, which is what makes a citation survive a re-ingest that rotates every chunk id.

Why relation is mandatory

It records how strongly this declaration is claimed to relate to the cited statement, and there is no safe default. A missing relation that defaulted to anything would be an axis inferred from silence, which the trust model forbids. Machine artifacts always spell it relation_claimed; only a dated, named human review may promote a claim to confirmed.

What this attribute does NOT do

It does not check the mathematics, does not look at the paper, and does not know whether the registry key exists — the registry lives in the topic repo and is validated separately. What it checks is that the key is well formed, so a typo fails at compile time instead of surfacing as an unresolvable citation much later.

inductive MathFormalContract.Relation : Type

How strongly a declaration is claimed to relate to the statement it cites.

Ordered from strongest to weakest. Every value is a claim by the author, not a verified fact; confirmation is a separate, human, dated act.

• exact : Relation

  The declaration states the cited statement, with no added hypotheses.

• equivalent : Relation

  Provably interderivable with the cited statement in this environment.

• specialization : Relation

  A special case of the cited statement.

• oneWay : Relation

  The cited statement implies this one, but not conversely.

• noClaim : Relation

  Related, but no implication is claimed in either direction.

def MathFormalContract.instBEqRelation.beq : Relation → Relation → Bool

Equations

• MathFormalContract.instBEqRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance MathFormalContract.instBEqRelation : BEq Relation

Equations

• MathFormalContract.instBEqRelation = { beq := MathFormalContract.instBEqRelation.beq }

@[implicit_reducible]

instance MathFormalContract.instHashableRelation : Hashable Relation

Equations

• MathFormalContract.instHashableRelation = { hash := MathFormalContract.instHashableRelation.hash }

def MathFormalContract.instHashableRelation.hash : Relation → UInt64

Equations

• MathFormalContract.instHashableRelation.hash MathFormalContract.Relation.exact = 0
• MathFormalContract.instHashableRelation.hash MathFormalContract.Relation.equivalent = 1
• MathFormalContract.instHashableRelation.hash MathFormalContract.Relation.specialization = 2
• MathFormalContract.instHashableRelation.hash MathFormalContract.Relation.oneWay = 3
• MathFormalContract.instHashableRelation.hash MathFormalContract.Relation.noClaim = 4

def MathFormalContract.instReprRelation.repr : Relation → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance MathFormalContract.instReprRelation : Repr Relation

Equations

• MathFormalContract.instReprRelation = { reprPrec := MathFormalContract.instReprRelation.repr }

@[implicit_reducible]

instance MathFormalContract.instInhabitedRelation : Inhabited Relation

Equations

• MathFormalContract.instInhabitedRelation = { default := MathFormalContract.instInhabitedRelation.default }

def MathFormalContract.Relation.toString : Relation → String

The wire spelling of a Relation. Kept as an explicit total function rather than derived, because these strings are a contract with the schemas and must not change when a constructor is renamed.

Equations

• MathFormalContract.Relation.exact.toString = "exact"
• MathFormalContract.Relation.equivalent.toString = "equivalent"
• MathFormalContract.Relation.specialization.toString = "specialization"
• MathFormalContract.Relation.oneWay.toString = "one_way"
• MathFormalContract.Relation.noClaim.toString = "no_claim"

@[implicit_reducible]

instance MathFormalContract.instToStringRelation : ToString Relation

Equations

• MathFormalContract.instToStringRelation = { toString := MathFormalContract.Relation.toString }

structure MathFormalContract.CitesEntry : Type

One @[cites] binding: a declaration, the statement key it claims, the strength of that claim, and the assumption-frontier ids it leaves open.

• declName : Lean.Name

  The declaration carrying the attribute.

• key : String

  The registry key, of the form stmt:<12 hex>:<label>.

• relation : Relation

  The claimed relation. Never defaulted.

• frontier : Array String

  Ids of frontier items this declaration does not discharge.

• note : String

  Free-text qualification of the claim. Empty means absent, and the emitter writes null rather than "" — a consumer must be able to tell "no note" from "a note that says nothing".

  Not decoration: relation := no_claim says two declarations are related without saying how, which is unreadable without one. The emission schema makes note a required key (nullable), and mfc lint rule E-06 fails a no_claim binding whose note is null. That rule is deliberately left on the mfc side rather than enforced here, so the rejection fixture it names stays authorable.

@[implicit_reducible]

instance MathFormalContract.instBEqCitesEntry : BEq CitesEntry

Equations

• MathFormalContract.instBEqCitesEntry = { beq := MathFormalContract.instBEqCitesEntry.beq }

def MathFormalContract.instBEqCitesEntry.beq : CitesEntry → CitesEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• MathFormalContract.instBEqCitesEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance MathFormalContract.instHashableCitesEntry : Hashable CitesEntry

Equations

• MathFormalContract.instHashableCitesEntry = { hash := MathFormalContract.instHashableCitesEntry.hash }

def MathFormalContract.instHashableCitesEntry.hash : CitesEntry → UInt64

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance MathFormalContract.instInhabitedCitesEntry : Inhabited CitesEntry

Equations

• MathFormalContract.instInhabitedCitesEntry = { default := MathFormalContract.instInhabitedCitesEntry.default }

Key validation

Deliberately hand-rolled rather than regex-based: this package has zero dependencies by design (it is the named exception to the consuming repo's one-pin rule, and that exception is bounded by the leaf property), so there is no regex engine available and none should be added.

def MathFormalContract.validateKey (key : String) : Except String Unit

Check a citation key, returning a specific complaint rather than a bare false — a malformed key is almost always a typo, and the author should not have to re-derive the grammar from a rejection.

Equations

• One or more equations did not get rendered due to their size.

The environment extension

opaque MathFormalContract.citesExt : Lean.SimplePersistentEnvExtension CitesEntry (Array (Array CitesEntry))

Storage for every @[cites] binding in the environment.

addEntryFn/addImportedFn are constant, matching the idiom Mathlib's stacks attribute uses: SimplePersistentEnvExtension already retains local entries in the state's first component, so recomputing a derived structure on every declaration would be pure overhead. Read it with citesEntries.

def MathFormalContract.citesEntries (env : Lean.Environment) : Array CitesEntry

Every @[cites] binding visible in env, imported and local.

Sorted by (key, declName). Emission has to be byte-reproducible for the contract's determinism gate, and traversal order here is not something to rely on. Sorting at the read is cheaper to guarantee than sorting at every write.

Equations

• One or more equations did not get rendered due to their size.

def MathFormalContract.addCitesEntry {m : Type → Type} [Lean.MonadEnv m] (e : CitesEntry) : m Unit

Record one binding in the environment.

Equations

• MathFormalContract.addCitesEntry e = Lean.modifyEnv fun (x : Lean.Environment) => Lean.PersistentEnvExtension.addEntry MathFormalContract.citesExt x e

Syntax

def MathFormalContract.citesRelation.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.citesRelation : Category

The claimed relation, as attribute syntax. Its own category so the atoms cannot collide with tactic names.

Equations

• Lean.Parser.Category.citesRelation = { }

def MathFormalContract.citesRelationExact : Lean.ParserDescr

The declaration states the cited statement.

Equations

• MathFormalContract.citesRelationExact = Lean.ParserDescr.node `MathFormalContract.citesRelationExact 1024 (Lean.ParserDescr.symbol "exact")

def MathFormalContract.citesRelationEquivalent : Lean.ParserDescr

Provably interderivable with the cited statement.

Equations

• MathFormalContract.citesRelationEquivalent = Lean.ParserDescr.node `MathFormalContract.citesRelationEquivalent 1024 (Lean.ParserDescr.symbol "equivalent")

def MathFormalContract.citesRelationSpecialization : Lean.ParserDescr

A special case of the cited statement.

Equations

• MathFormalContract.citesRelationSpecialization = Lean.ParserDescr.node `MathFormalContract.citesRelationSpecialization 1024 (Lean.ParserDescr.symbol "specialization")

def MathFormalContract.citesRelationOne_way : Lean.ParserDescr

The cited statement implies this one, not conversely.

Equations

• MathFormalContract.citesRelationOne_way = Lean.ParserDescr.node `MathFormalContract.citesRelationOne_way 1024 (Lean.ParserDescr.symbol "one_way")

def MathFormalContract.citesRelationNo_claim : Lean.ParserDescr

Related, but no implication claimed.

Equations

• MathFormalContract.citesRelationNo_claim = Lean.ParserDescr.node `MathFormalContract.citesRelationNo_claim 1024 (Lean.ParserDescr.symbol "no_claim")

def MathFormalContract.citesAttr : Lean.ParserDescr

Bind this declaration to a statement in a paper.

@[cites "stmt:9f4c1a20b7d3:bridgeland2007.lem-8.2" (relation := one_way)
        (frontier := ["gltilde-universal-cover"])
        (note := "Acts on PreStabilityCondition, not StabilityCondition.")]

relation is mandatory; there is no safe default. frontier and note are optional, independently, and in either presence combination.

The atomic(...) wrappers are load-bearing, not decoration. Both optional groups open with (, so without them the parser commits to frontier on seeing the paren and then fails with "unexpected identifier; expected 'frontier'" on (note := ...) alone — making a note impossible without a frontier. That is the common case, since mfc lint rule E-06 requires a note exactly when relation := no_claim, which usually has no frontier. atomic lets the parser backtrack out of the frontier group and try the note group.

Equations

• One or more equations did not get rendered due to their size.

Inspection

The emitter is the real consumer, but a binding you cannot see is a binding you cannot debug.

def MathFormalContract.«command#cites_dump» : Lean.ParserDescr

Print every @[cites] binding visible here, in emission order.

Equations

• MathFormalContract.«command#cites_dump» = Lean.ParserDescr.node `MathFormalContract.«command#cites_dump» 1024 (Lean.ParserDescr.symbol "#cites_dump")