The @[discharges] attribute

Anchors a frontier discharge in Environment.constants rather than in prose.

@[discharges "gltilde-universal-cover"]
theorem universalCoverData : ... := ...

The rule this exists to satisfy

The design states its own axis-independence rule precisely: "two axes are distinct only if they have distinct evidence-producing programs", and uses it to kill a competing design's three-views-of-one-closure axes.

Axis 6, frontier_discharged, broke that rule. frontier[].discharged_by is hand-edited YAML and mfc only aggregates it. Nothing checked that the named discharger proves anything, and — unlike the faithfulness axis, the other human one — it carried no reviewer and no date. Two of seven axes were human, and one of them was unattributed while presenting as computed.

With this attribute the edge is in the environment: mfc lint rule E-12 requires the declaration named by discharged_by to exist in the emission and to carry @[discharges "<that id>"]. Axis 6 becomes genuinely computed over emission ∪ registry.

What it still does not do

It does not check that the declaration proves the frontier item. Nothing mechanical can: a frontier item is prose about a gap in the world, and the claim that a particular theorem closes it is a mathematical judgement. What this removes is the weaker failure — a discharged_by naming a declaration that does not exist, or that never claimed to discharge anything, which was indistinguishable from a real discharge in every artifact.

The attribute is the author asserting the edge in code that has to compile, next to the proof, where a reviewer reading the theorem sees the claim. That is strictly more than YAML somewhere else, and strictly less than a verified implication. Both halves of that are worth saying out loud.

structure MathFormalContract.DischargesEntry : Type

One @[discharges] binding.

• declName : Lean.Name

  The declaration carrying the attribute.

• frontierId : String

  The frontier item id it claims to discharge.

@[implicit_reducible]

instance MathFormalContract.instInhabitedDischargesEntry : Inhabited DischargesEntry

Equations

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

opaque MathFormalContract.dischargesExt : Lean.SimplePersistentEnvExtension DischargesEntry (Array (Array DischargesEntry))

Storage for every @[discharges] binding, following citesExt exactly.

def MathFormalContract.dischargesEntries (env : Lean.Environment) : Array DischargesEntry

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

Sorted by (frontierId, declName), for the reason citesEntries gives: the emission has to be byte-reproducible and traversal order is not something to rely on.

Equations

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

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

Record one binding in the environment.

Equations

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

def MathFormalContract.dischargesAttr : Lean.ParserDescr

One or more frontier ids. Several is normal: a single construction often closes more than one recorded gap, and forcing one attribute per id would make the common case read as several unrelated claims.

Equations

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

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

Print every @[discharges] binding visible here.

Equations

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