17.3. The license clause — side conditions do not transfer🔗

A relation's license clause is the part of its declaration that extends its witness beyond the carrier rung the witness is proved at: one entry per further rung of the carrier ladder, each naming how the claim holds there — a repair theorem, or an independent witness restated at that rung.

Definition17.3.1

Group: The interface clause and the judgments on it. A boundary is declared , so a membership choice can be wrong about it — and the two decidable comparisons below are exactly the two ways it can be wrong: not the boundary the members compute, or not a faithful deployment of the tier below. (3)

Group member previews

Preview

Definition 17.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 15.6.5

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

One rung of a relation's license clause: the carrier rung the claim is extended to, and how it holds there. Laws transfer across the carrier ladder at the cost of one rounding step per join; side conditions do not — a nonzero-total hypothesis checked over the reals constrains the exact total, over binary32 the rounded fold, and neither implies the other. So a relation claimed beyond the rung its witness is stated at owes, per additional rung, either a named repair — exact, where rounding is the identity on the values in play, or nonneg, where nonnegative on-grid weights rule the cancellation out — or restated: an independent witness proved at that rung. A rung claimed with no repair and no restatement is refused, because a side condition does not transfer by being assumed to.

Lean code for Definition17.3.1●1 definition

structure(2 fields)defined in PropertyKindCalculus/Provenance.lean

complete

structure PropertyKindCalculus.Provenance.RelationLicense : Type

structure PropertyKindCalculus.Provenance.RelationLicense :
  Type

One rung of a relation's license clause: the carrier rung the claim is extended to,
spelled as the ladder names it (`ℝ`, `FP32`, `Float`, …), and how the claim holds there.
A relation with an empty license list is stated at its witness's own rung and claims
nothing beyond it; each entry here is one further rung, answered for by name.

Fields

rung : String

The carrier rung, as the ladder names it.

transfer : PropertyKindCalculus.Provenance.TransferStatus

How the claim holds at this rung: transferred by a named repair, or restated by a
named per-rung witness.

Proof for Definition 17.3.1

uses 0

A rung name and a three-constructor transfer status, each constructor carrying the name of its evidence; the elaborator checks the named evidence is a sorry-free theorem, and the refusal of an unanswered rung is a pinned probe.