pith. machine review for the scientific record. sign in
theorem other other

with

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 350theorem with its immediate consequences.
 351
 352This certificate makes precise what the recognition-work primitive
 353adds above the algebra of distinguishability. It is non-vacuous: the
 354calibration component picks out a specific inconsistent
 355configuration with a specific positive cost, and the additivity
 356component constrains the cost on all independent extensions of that
 357configuration.
 358-/

depends on (21)

Lean names referenced from this declaration's body.