17.1. The interface — the declared boundary🔗

Definition17.1.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.2.1

Loading preview

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

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 7.2.4

Loading preview

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

✓L∃∀N

The declared boundary: a name, the member declarations the boundary is claimed for, the kind-typed ports with the role each plays — input, config, param, output, conditional — the exits where values leave the calculus, and, per conditional port, the decider: the name of the declaration that decides its cases, so a validity domain is read off the boundary rather than excavated from a constructor choice. Roles carry binding time: a param is a source this tier leaves for the tier below to bind, and Contract.discharges is the decidable tier relation — every inherited parameter bound or restated, never forgotten, and no exit lost on the way up. Contract.agrees is the decidable scope judgment: the declared boundary is the one the members actually compute, in both directions. #kind_contract_decide and #kind_discharges_decide reflect both into kernel-checked theorems. At scale the obligation moves off the author's memory: #kind_contracts sweeps every contract declared under a namespace — membership is by type, so declaring a boundary enrolls it — and #kind_contracts_decide is the same sweep as a hard gate, adding each passing boundary's kernel receipt. A deliberate falsification probe opts out explicitly with @[kindCounterexample], and the sweeps count the exemptions in their pinned headers.

Lean code for Definition17.1.1●1 definition

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

complete

structure PropertyKindCalculus.Provenance.Contract (ν κ : Type) : Type

structure PropertyKindCalculus.Provenance.Contract
  (ν κ : Type) : Type

**A declared boundary** (header, "The declared boundary"): the interface an author
claims for a scope — a rendered name, the members claimed for, the ports with the role
and binding time each carries, and the exits where values leave the calculus. It is the
statement a membership choice can be wrong about: `Contract.agrees` holds exactly when
the boundary those members compute is the boundary declared here, so a member added or
dropped changes a difference list rather than passing silently. Same port vocabulary as
the graph's own interface, because it is a claim about that interface and not a second
notation for it.

Fields

name : String

The rendered name of what the boundary belongs to — an algorithm, an application.

members : List Lean.Name

The scope: the declarations whose harvested graphs the boundary is claimed for,
by the names the environment resolves. Not compared by `agrees`, which sees only the
graph they produced — they are what *selects* that graph, and stating them here is what
makes the selection a declaration rather than a habit of each call site.

ports : List (PropertyKindCalculus.Provenance.Port ν κ)

The declared interface, with each port's role and binding time.

exits : List ν

The declared exits: where the contract says values leave the calculus.

deciders : List (ν × Lean.Name)

The deciders of the conditional ports: for a `conditional` port, the name of the
declaration that decides its cases — the `KindAdmissible` instance, domain predicate,
or validity check a consumer consults. The role states that cases exist; the decider
states *which*, by name, where a consumer reads it. One entry per decided port,
checked by `#kind_contract` to name a conditional port and an existing declaration; a
conditional port with no entry remains a declared case whose predicate is stated
elsewhere.

aggregations : List (ν × PropertyKindCalculus.Provenance.AggregationClass)

The aggregation classes of the produced ports: for an `output` or `conditional`
port, how its value behaves when the computation is distributed over a carving of a
batch axis — the declared mereology of the boundary (`AggregationClass`). One entry
per classed port, checked by `#kind_contract` to govern a produced port and, where
the class names a tolerance, condition, sortal, transport, or law, to name an
existing declaration (a tolerance additionally a `Quantity` at the port's kind). A
produced port with no entry makes no distribution claim — and the license to shard
it is then nobody's to derive.

suppliers : List (ν × Lean.Name)

The suppliers of the module-valued ports: for a port whose kind is a *signature*
(the `→`-joined port form of a functional argument), the name of the module this
tier binds to it. One entry per supplied port, checked by `#kind_contract` to govern
a signature port and to name an existing declaration whose own kind signature is the
declared one — so *which* module a deployment bound is declared and checked, not
implicit in a call site. A signature port with no entry remains a parameter: which
module answers it is then the tier below's to declare.

role : PropertyKindCalculus.Provenance.BoundaryRole

The role: a model boundary — the default, what a requirement governs — or a
specification boundary, what a requirement is checked against: a contract whose one
member computes the bound. Read by `#kind_requirement`, which refuses a requirement that
governs a specification or is checked against a model, and by the requirement-coverage
census, which asks every produced port of a model boundary for a requirement and asks
nothing of a specification.

Proof for Definition 17.1.1

uses 0

A four-list structure over node and kind types, plus the decider association list; the judgments are structural recursions decided by evaluation in a probe and by kernel reduction (decide) in a theorem. Nothing about it is trusted from construction — the doctrine is to decide the object.