A Property Kind Calculus for Measurement Metrology

17.2. The behavior — the measurement model as a theorem edge🔗

Definition17.2.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
Definition 17.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

The theorem edge between two declared boundaries — the formal seat of the VIM 4 2CD §2.12 measurement model. It names the two contracts, what is claimed (the relation kind), the witness theorem, the claim in the author's own words, and three optional clauses: a tolerance (a declaration whose type is a Quantity at the kind of an output port of the governed boundary — a bound is a kinded quantity, not a float in prose), the named side conditions the claim holds under (each checked to be a declaration the witness statement mentions), and the license clause (one entry per carrier rung). The edge is load-bearing because the semantic claim is often unstatable structurally: a closed-form retrieval contains none of its forward's members, a Newton retrieval contains all of them, a lookup-table retrieval contains the forward only while building its table — yet the scientific claim has one shape in all three cases, and only the theorem edge states it uniformly. #kind_relation checks everything around the proof — the witness a sorry-free theorem, the conclusion in the claimed shape, members of both boundaries mentioned, every optional clause answered for by name — and #kind_relations surveys a namespace's edges as one pinnable report — membership by type, violations rendered in the report itself, @[kindCounterexample]-marked probes as counted exemptions.

Lean code for Definition17.2.1●1 definition
  • structure(11 fields)defined in PropertyKindCalculus/Provenance.lean
    complete
    structure PropertyKindCalculus.Provenance.Relation : Type
    structure PropertyKindCalculus.Provenance.Relation :
  Type
    **A theorem edge between two declared boundaries** (header, "The theorem edge"): the
two contracts, spelled as the environment names them, what the theorem claims of them, the
theorem itself, and the claim in the author's own words — the hypothesis a `refines` holds
under, the quantity a `boundedBy` is bounded by. (The field is `claim` and not `says`
because `says` is a Mathlib tactic keyword, and a field name that cannot be written in a
`where` block downstream is not a field name.) The prose is not checked and is not meant
to be: what is checked is that the named theorem exists, is proved, and is about these two
boundaries.

    Fields

    left : Lean.Name
    The declaration name of the contract on the left of the claim. 
    right : Lean.Name
    The declaration name of the contract on the right. 
    kind : PropertyKindCalculus.Provenance.RelationKind
    What is claimed. 
    witness : Lean.Name
    The declaration name of the theorem that proves it. 
    claim : String
    The claim in the author's words — the hypothesis, the bound, the domain. 
    tolerance : Lean.Name
    For a `boundedBy` edge: the declaration naming the bounding quantity — a `Quantity`
at the kind of an output port of the left boundary, because a tolerance is a kinded
quantity governing what the boundary produces, not a float in prose. Anonymous where
the claim carries its bound inside the witness statement. 
    hypotheses : List Lean.Name
    The named side conditions the claim holds under: declarations the witness statement
mentions, so the domain a consumer must establish is listed at the edge rather than
excavated from the proof. Empty where the claim is unconditional. 
    licenses : List PropertyKindCalculus.Provenance.RelationLicense
    The license clause: one entry per carrier rung the claim is extended to beyond the
rung its witness is stated at, each answered for by a named repair or a named per-rung
restatement (`RelationLicense`). Empty where the claim stops at its witness's rung. 
    wellPosed : Lean.Name
    For an `inverts` edge: the declaration name of the theorem that proves the
inversion's answer exists and is unique — a sorry-free theorem concluding with `∃!` —
on the domain named beside it. Anonymous where well-posedness is not (or not yet)
claimed; an edge whose inversion is *not* single-valued surfaces that in `ambiguity`
instead. 
    domain : Lean.Name
    The declaration naming the domain the well-posedness holds on — the box or
predicate the `wellPosed` statement mentions. Existence and uniqueness are proved *on a
declared domain*, so a `wellPosed` with no `domain` is refused. 
    ambiguity : Lean.Name
    For an `inverts` edge: the declaration name of the theorem that surfaces the
inversion's ambiguity — a sorry-free theorem concluding with the negation of an `∃!`,
the uniqueness that fails (typically: without the domain's certificate). Ambiguity is
surfaced as a declaration a consumer can read, not resolved to whichever root the
algorithm reached first.
Proof for Definition 17.2.1
uses 0

A record of names; nothing about it is decidable, because the witness already is a kernel-checked proposition. What the elaborator adds is the checking of everything around the proof, throwing on every violation, so the command is the report and the gate at once.

Definition17.2.2
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.
uses 0used by 1✓L∃∀N

The four ways an implementing measurement function (VIM 4 2CD §2.13) may relate to its measurement model, each with a checked conclusion shape: equals (an Eq), inverts (an Eq one of whose sides composes members of both boundaries — the round trip must be in the statement), refines (an Eq under at least one bound hypothesis — the smaller domain, stated), and boundedBy (an order relation, its tolerance nameable as a kinded quantity). The exact-versus-approximate axis of a module's honesty is carried here: a fixed-iteration solver's true relation to its model is boundedBy, and the vocabulary makes that statable rather than silently rounding it to equals.

Lean code for Definition17.2.2●1 definition
  • inductive(4 constructors)defined in PropertyKindCalculus/Provenance.lean
    complete
    inductive PropertyKindCalculus.Provenance.RelationKind : Type
    inductive PropertyKindCalculus.Provenance.RelationKind :
  Type
    What a theorem claims about two declared boundaries.

    Constructors

    PropertyKindCalculus.Provenance.RelationKind.inverts :
  PropertyKindCalculus.Provenance.RelationKind
    The left boundary recovers what the right one consumed — an inversion, at the
equation the witness states and on the domain it states it. The witness concludes with
an `Eq` one of whose sides composes members of both boundaries — the round trip. 
    PropertyKindCalculus.Provenance.RelationKind.refines :
  PropertyKindCalculus.Provenance.RelationKind
    The left boundary answers as the right one does wherever a stated hypothesis holds:
the same value on a smaller domain. The witness concludes with an `Eq` and binds at
least one hypothesis — the domain it holds on. 
    PropertyKindCalculus.Provenance.RelationKind.equals :
  PropertyKindCalculus.Provenance.RelationKind
    The two boundaries return the same value. The witness concludes with an `Eq`. 
    PropertyKindCalculus.Provenance.RelationKind.boundedBy :
  PropertyKindCalculus.Provenance.RelationKind
    The left boundary's departure from the right is bounded by a stated quantity. The
witness concludes with an order relation.
Proof for Definition 17.2.2
uses 0

A four-constructor enumeration; the shape checks live in the elaborator, pinned by acceptance and refusal probes for all four kinds.