Internet-Draft Carrier Identity Core July 2026
Le Expires 26 January 2027 [Page]
Workgroup:
Network Working Group
Internet-Draft:
draft-le-carrier-identity-core-00
Published:
Intended Status:
Informational
Expires:
Author:
T. Le

Carrier Identity Core: A Proof-Bearing Kernel for Content-Derived Node Identity and Structural Graphs

Abstract

This document specifies Carrier Identity Core, a minimal, proof-bearing identity kernel for content-derived node identity, canonical references, and finite structural graphs.

It defines a finite-sequence substrate, a self-contained frame and hash interface, staged formation of immutable lanes, node bodies and proof-bearing occurrences, Qualified Node Keys, canonical reference construction, exact structural theorem schemas, and structural graph validity.

Informative derivations of the exact structural theorem schemas are provided in an informative appendix.

This document does not define computational security experiments, evidence records, proof admission, resource evaluation, consensus, liveness, finality, governance, or operational protocol behavior.

Status of This Memo

This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79.

Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet-Drafts is at https://datatracker.ietf.org/drafts/current/.

Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress."

This Internet-Draft will expire on 26 January 2027.

▲

Table of Contents

1. Introduction

This document specifies Carrier Identity Core, a minimal, proof-bearing identity kernel for content-derived node identity, canonical references, and finite structural graphs. The kernel separates three questions that content-addressed systems commonly conflate: whether an object is validly formed, whether its identifier is unique, and whether a structural graph over such objects is valid. Each question is answered at a distinct layer with distinct obligations. The kernel is minimal in the sense that it defines only the formation, identity, reference, and graph-validity layers required to separate structural validity from exactness and operational policy.

Formation is a structural obligation: every lane, body, transcript, identifier, and Qualified Node Key carries a proof-bearing formation witness, and a carrier system exists only when identity construction is total over every declared body type. Identifier uniqueness is not assumed from formation: it is a conditional theorem that holds exactly when named hash-injectivity premises hold, and an exactness certificate names the lanes for which those premises have been proved. Structural graph validity is derived from canonical body references alone and is independent of exactness, admission, evidence, and consensus.

Admission, trust, evidence, governance, consensus, resource accounting, and computational security are intentionally outside this core. An importing specification can add such judgments over core values within the extension boundary (Appendix D); the formation rules, identity construction, canonical reference interpretation, and graph truth defined here are not subject to redefinition there. Typical uses include content-derived node identifiers in provenance graphs, artifact graphs, and transparency structures, and importing protocols that need a stable identity kernel separate from admission, evidence, and governance.

2. Terminology

Table 1
Term Meaning in this specification
Carrier A lane-indexed node body whose canonical construction determines a content-derived identifier. The formal type realizing a carrier is Body.
Substrate The radix, alphabet, frame codec, and stable-binding digest width fixed before any lane is declared.
Lane authority A finite nominal lane type together with one proof-bearing primitive binding for each lane. A lane plays the role of a sort in a many-sorted signature; the name "lane" is retained for its derived vocabulary (lane-bound hashing, lane descriptor).
Reference authority A lane authority extended with one proof-bearing reference binding for each lane.
Closed lane binding The pair consisting of a lane's primitive binding and reference binding. Neither component is replaceable.
Node body The proof-independent tuple that contributes to identity.
Occurrence A node body paired with an opaque proof object. The proof object is not an identity input.
Hash purpose One of the four lane-bound-hash roles: parameter, content, references, or identifier. The transcript tag is not a hash purpose.
Lane-bound hashing Hashing of an explicit hash-purpose tag frame, lane-descriptor frame, and message under the suite fixed by the lane.
Qualified Node Key The dependent pair (lane, identifier). It is the structural graph key.
Canonical references A duplicate-free, strictly ordered finite sequence of Qualified Node Keys admitted by a lane.
Structural graph A finite Qualified-Node-Key map to node bodies with edges derived only from body references.
Kernel The set of formation rules, identity constructions, canonical reference rules, structural graph validity conditions, and exact theorem schemas defined by this document.
Exactness certificate A proof-bearing layer over a carrier system that names lanes proven to satisfy the four exact-body-binding hash-injectivity premises.

3. Conventions and Definitions

Definitions, equations, typed records, theorem schemas, and explicitly labeled requirements are normative within this document. Examples, notes, and informative references are not normative.

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals, as shown here.

Lowercase uses of "must", "should", or "may" are descriptive only and do not carry requirement strength unless the corresponding uppercase BCP 14 keyword is used.

The normative requirements in this document apply to specifications that claim conformance to Carrier Identity Core. They do not by themselves impose interoperability requirements on implementations unless an importing specification explicitly adopts them.

The formation dependency order, the core and exactness invariants, and the extension boundary (Appendices A through D) are normative. The ASCII equivalence table and the theorem-schema derivations (Appendices E and F) are informative.

The theorem schemas stated in the main body are normative. The derivations in the informative derivation appendix do not add normative requirements.

Normative references are incorporated only to the extent stated below.

4. Core Conformance Requirements

This section summarizes the normative formation requirements defined in this document. The full definitions in the corresponding sections are authoritative.

  1. A Substrate MUST satisfy FrameCodecWellFormed.
  2. A StableRuleBinding MUST have non-empty owner_id, rule_id, and revision.
  3. A HashSuite MUST have positive output_length.
  4. Each lane MUST have exactly one primitive binding and exactly one reference binding.
  5. Each primitive binding MUST satisfy LanePrimitiveBindingWellFormed.
  6. The four hash-purpose tags MUST be pairwise distinct.
  7. The transcript tag MUST be distinct from every hash-purpose tag.
  8. The index encoder, parameter encoder, context encoder, and payload encoder MUST be injective.
  9. The parameter encoder, context encoder, and payload encoder outputs, and all digest-length strings, MUST lie in D_frame.
  10. Canonical references MUST be duplicate-free and strictly ordered by referenceBytes.
  11. The reference accumulator MUST be injective on canonical reference sequences.
  12. A CarrierSystem MUST provide a body inhabitant for every lane.
  13. A CarrierSystem MUST provide a construction-formation witness for every typed body.
  14. StructuralGraphValid MUST require graph scope, body-construction validity, key consistency, closure validity, and internal acyclicity.
  15. An ExactnessCertificate MUST name only lanes satisfying ExactBodyBindingPremises.
  16. An importing specification MUST NOT redefine, override, weaken, strengthen, or shadow any core definition within the extension boundary (Appendix D), including but not limited to the illustrative names listed there.

The informative appendices do not add conformance requirements.

5. Scope and independence

Carrier Identity Core defines exactly:

  1. a finite-sequence substrate;
  2. a self-contained frame and hash interface;
  3. staged, proof-bearing formation of immutable lanes;
  4. node bodies and proof-bearing occurrences;
  5. transcript, identifier, Qualified Node Key, and canonical reference construction;
  6. finite structural graphs, closure, and internal acyclicity;
  7. exact structural theorem schemas whose premises are stated inside this document; and
  8. an optional exactness-certificate layer that names a proof-certified subset of lanes satisfying the exact-body-binding premises.

Detailed derivations of the exact structural theorem schemas appear in the derivation appendix and are informative. They do not alter the normative theorem schemas stated in the main body.

The core does not define:

This document has no semantic dependency on another specification. A separate specification MAY import these definitions, but MUST NOT alter their formation, identity, reference interpretation, or graph truth.

Admission, trust, evidence, resource accounting, consensus, finality, governance, and operational liveness are outside the scope of this document.

ParseFrame is used in the substrate well-formedness laws and derived frame laws but not in identity construction or structural theorem conclusions after substrate formation. It is retained, together with LaneBindingValid and Occurrence with its projections (packOccurrence, laneOfOccurrence, bodyOfOccurrence), as export surface for importing specifications; none of these is consumed by any later construction in this core.

This core is compared informatively with [RFC6920], [RFC8949], [RFC8785], [RFC9052], [RFC9162], [RFC9562], [FIPS180-4], and [SP800-185]; nothing is imported from any of them.

5.1. Mathematical notation

The following constructors are primitive mathematical notation:

A finite non-empty nominal Type is a finite non-empty set of names with decidable equality; equality of lanes is propositional equality in the model, and implementations require a decidable equality procedure. A finite sequence R is duplicate-free iff for all i < j < |R|, R[i] ≠ R[j]. For m : FinMap K V, domain(m) := { k : K | m[k] is defined }.

Type, Prop, Bool, Nat
Set A                 set of values of type A
FinSet A              finite set of values of type A
FinSeq A              finite sequence of values of type A
FinMap K V            finite partial map from K to V
Option A := None | Some(A)
DepPair (x : A). B(x) dependent pair
transport_h(x)        equality transport of x along a bound witness h

For R : FinSeq A, r ∈ R means ∃ j < |R|. R[j] = r.

For a finite sequence s, |s| is its length, ε is the empty sequence, and s ‖ t is concatenation. Equality is typed equality.

Equality appearing in formulas is typed propositional equality, not judgmental equality of a particular proof assistant. Definitional equality is used only for unfolding records, projections, and local aliases. When equality between values of dependent types is required, an explicit witness h is bound and transport_h is used. For h : x = y and v : B(x), transport_h(v) : B(y) denotes equality substitution along that specific witness h; a theorem using transport binds h explicitly. A function displayed with an arrow is total unless a partial arrow ⇀ is shown. A record is telescopic when a later field type depends only on preceding fields.

6. Substrate

6.1. Parameterized frame codec

For an alphabet A, a frame codec is:

FrameCodec[A] := ⟨
  input_language : Set (FinSeq A),
  frame : FinSeq A → FinSeq A,
  parse : FinSeq A ⇀ FinSeq A × FinSeq A
⟩

For a codec c, write D_c := c.input_language. It is well formed exactly when:

FrameCodecWellFormed(c) :=
  (∀ a ∈ D_c. ∀ rest.
     c.parse(c.frame(a) ‖ rest) = Some(a, rest))
  ∧ (∀ raw,a,rest.
     c.parse(raw) = Some(a, rest)
       ⟹ a ∈ D_c ∧ raw = c.frame(a) ‖ rest)

Because c.parse is a partial function, it is single-valued. Round-trip therefore derives the following laws for admitted frame inputs; they are not independent formation axioms:

FrameLeftCancellation(c) :=
  ∀ a,b ∈ D_c. ∀ x,y.
    c.frame(a) ‖ x = c.frame(b) ‖ y
      ⟹ a = b ∧ x = y

FrameInjective(c) :=
  ∀ a,b ∈ D_c.
    c.frame(a) = c.frame(b) ⟹ a = b

FrameCodecWellFormed(c) entails FrameLeftCancellation(c): parsing the same raw sequence through the two round-trip equations yields the same unique result. FrameInjective(c) follows by applying left cancellation with x = y = ε.

Two consequences follow from FrameCodecWellFormed: admitted frame outputs are prefix-free over D_frame, and no admitted frame output is empty when D_frame contains more than one element. This core does not constrain frame(x) for x outside D_frame; implementations SHOULD reject inputs outside D_frame before framing.

6.2. Base record

A substrate is the following telescopic record:

Substrate := ⟨
  radix : Nat,
  radix_at_least_two : radix ≥ 2,
  binding_digest_length : Nat,
  binding_digest_length_positive : binding_digest_length > 0,
  frame_codec : FrameCodec[{0,…,radix−1}],
  frame_codec_formation : FrameCodecWellFormed(frame_codec)
⟩

For a fixed β : Substrate, define:

Σ_β := {0,…,β.radix−1}
Σ*_β := FinSeq Σ_β
Σ^n_β := { s ∈ Σ*_β | |s| = n }
D_frame,β := β.frame_codec.input_language
Frame_β := β.frame_codec.frame
ParseFrame_β := β.frame_codec.parse

The natural-number order on Σ_β = {0,…,radix−1} induces a strict total lexicographic order <lex on Σ*_β. For s, t : Σ*_β, s <lex t holds iff either s is a proper prefix of t, or there exists k < min(|s|, |t|) with s[j] = t[j] for all j < k and s[k] < t[k].

6.3. Stable semantic bindings

A stable binding is a finite value, never a function value:

StableRuleBinding_β := ⟨
  owner_id : Σ*_β,
  rule_id : Σ*_β,
  revision : Σ*_β,
  digest : Σ^{β.binding_digest_length}_β
⟩

StableRuleBindingWellFormed_β(b) :=
  b.owner_id ≠ ε
  ∧ b.rule_id ≠ ε
  ∧ b.revision ≠ ε

A type, function, or predicate may be paired with a stable identity:

BoundType_β := ⟨
  binding : StableRuleBinding_β,
  carrier : Type
⟩

BoundFunction_β[A,B] := ⟨
  binding : StableRuleBinding_β,
  apply : A → B
⟩

BoundPredicate_β[A] := ⟨
  binding : StableRuleBinding_β,
  holds : A → Prop
⟩

The semantic value is selected by the binding record that contains it. A function value, predicate value, or host-language object identity is never a canonical role key.

7. Primitive lane authority

7.1. Hash suites and hash purposes

For a base β, a hash suite is:

HashSuite_β := ⟨
  suite_binding : StableRuleBinding_β,
  output_length : Nat,
  output_length_positive : output_length > 0,
  hash : Σ*_β → Σ^{output_length}_β
⟩

HashSuiteWellFormed_β(σ) :=
  StableRuleBindingWellFormed_β(σ.suite_binding)
  ∧ σ.output_length > 0

No injectivity, collision resistance, or computational property follows from this definition.

The finite type HashPurpose has exactly four distinct constructors:

identifierPurpose
parameterPurpose
contentPurpose
referencesPurpose

The transcript tag is a separate lane field. It is not a fifth hash purpose and has no lane-bound-hash domain.

7.2. Primitive lane binding

For a base β, a finite nominal type Λ, and λ : Λ, the primitive lane binding is the following telescopic record:

LanePrimitiveBinding⟦β,Λ⟧(λ) := ⟨
  lane_registry_binding : StableRuleBinding_β,
  lane_descriptor : Σ*_β,
  lane_descriptor_binding : StableRuleBinding_β,

  hash_suite : HashSuite_β,
  proof_parameter : BoundType_β,
  proof_object : BoundType_β,
  context : BoundType_β,
  payload : BoundType_β,
  index : BoundType_β,

  transcript_tag : Σ*_β,
  transcript_tag_binding : StableRuleBinding_β,
  hash_purpose_tags : BoundFunction_β[HashPurpose, Σ*_β],
  covered_lbh_domain : HashPurpose → BoundPredicate_β[Σ*_β],

  index_width : Nat,
  index_encoder :
    BoundFunction_β[index.carrier, Σ^{index_width}_β],
  parameter_encoder :
    BoundFunction_β[proof_parameter.carrier, Σ*_β],
  context_encoder :
    BoundFunction_β[context.carrier, Σ*_β],
  payload_encoder :
    BoundFunction_β[payload.carrier, Σ*_β],

  identity_context_bytes : Σ*_β,
  identity_context_binding : StableRuleBinding_β
⟩

The identity_context_bytes field is an explicit identity input. This core does not define its semantics. An importing specification MUST NOT assume that this field cryptographically commits any unstated semantics unless that specification defines an explicit conformance rule for the field.

The primitive binding is well formed when:

LanePrimitiveBindingWellFormed⟦β,Λ⟧(λ,b) :=
  StableRuleBindingWellFormed_β(b.lane_registry_binding)
  ∧ b.lane_descriptor ∈ D_frame,β
  ∧ StableRuleBindingWellFormed_β(b.lane_descriptor_binding)
  ∧ HashSuiteWellFormed_β(b.hash_suite)

  ∧ StableRuleBindingWellFormed_β(b.proof_parameter.binding)
  ∧ StableRuleBindingWellFormed_β(b.proof_object.binding)
  ∧ StableRuleBindingWellFormed_β(b.context.binding)
  ∧ StableRuleBindingWellFormed_β(b.payload.binding)
  ∧ StableRuleBindingWellFormed_β(b.index.binding)

  ∧ b.transcript_tag ∈ D_frame,β
  ∧ StableRuleBindingWellFormed_β(b.transcript_tag_binding)
  ∧ StableRuleBindingWellFormed_β(b.hash_purpose_tags.binding)
  ∧ (∀ p : HashPurpose.
       b.hash_purpose_tags.apply(p) ∈ D_frame,β)
  ∧ (∀ p,q : HashPurpose.
       b.hash_purpose_tags.apply(p)
         = b.hash_purpose_tags.apply(q)
       ⟹ p = q)
  ∧ (∀ p : HashPurpose.
       b.transcript_tag ≠ b.hash_purpose_tags.apply(p))
  ∧ (∀ p : HashPurpose.
       StableRuleBindingWellFormed_β(
         b.covered_lbh_domain(p).binding))

  ∧ b.index_width > 0
  ∧ StableRuleBindingWellFormed_β(b.index_encoder.binding)
  ∧ StableRuleBindingWellFormed_β(b.parameter_encoder.binding)
  ∧ StableRuleBindingWellFormed_β(b.context_encoder.binding)
  ∧ StableRuleBindingWellFormed_β(b.payload_encoder.binding)

  ∧ (∀ i,j : b.index.carrier.
       b.index_encoder.apply(i) = b.index_encoder.apply(j)
       ⟹ i = j)
  ∧ (∀ u,v : b.proof_parameter.carrier.
       b.parameter_encoder.apply(u) = b.parameter_encoder.apply(v)
       ⟹ u = v)
  ∧ (∀ c,d : b.context.carrier.
       b.context_encoder.apply(c) = b.context_encoder.apply(d)
       ⟹ c = d)
  ∧ (∀ x,y : b.payload.carrier.
       b.payload_encoder.apply(x) = b.payload_encoder.apply(y)
       ⟹ x = y)

  ∧ (∀ u : b.proof_parameter.carrier.
       b.parameter_encoder.apply(u) ∈ D_frame,β)
  ∧ (∀ c : b.context.carrier.
       b.context_encoder.apply(c) ∈ D_frame,β)
  ∧ (∀ x : b.payload.carrier.
       b.payload_encoder.apply(x) ∈ D_frame,β)
  ∧ (∀ z : Σ^{b.hash_suite.output_length}_β.
       z ∈ D_frame,β)

  ∧ b.identity_context_bytes ∈ D_frame,β
  ∧ StableRuleBindingWellFormed_β(
       b.identity_context_binding)

covered_lbh_domain is a plain function on the finite four-constructor type HashPurpose. It is equivalent in definition to four separate bound predicates, one per purpose, and therefore does not introduce a higher-order or recursive binding that would violate Section 6.3. The transcript-tag distinctness conjunct formalizes the separation stated in Section 7.1: no hash-purpose tag equals the transcript tag, so domain-separation of lane-bound hashing is strict. Hash-purpose tags need not be distinct across lanes, because the framed lane descriptor provides cross-lane domain separation.

This core permits empty lane descriptors, transcript tags, or identity context bytes when they are admitted by D_frame; importing specifications MAY require non-empty administrative values. If the index carrier has more values than radix^index_width, no injective fixed-width index encoder exists and the primitive binding cannot be well formed.

7.3. Lane authority record

A lane authority is:

LaneAuthority := ⟨
  base : Substrate,
  lanes : finite non-empty nominal Type,
  primitive_binding_of :
    (λ : lanes) → LanePrimitiveBinding⟦base,lanes⟧(λ),
  primitive_formation_proof :
    ∀ λ : lanes.
      LanePrimitiveBindingWellFormed⟦base,lanes⟧(
        λ, primitive_binding_of(λ)),
  lane_descriptor_unique :
    ∀ λ,μ : lanes.
      primitive_binding_of(λ).lane_descriptor
        = primitive_binding_of(μ).lane_descriptor
      ⟹ λ = μ
⟩

This record is finite and well founded. It does not mention Qualified Node Keys, references, bodies, or a completed carrier system.

For α : LaneAuthority, define:

Σ_α := Σ_{α.base}
Σ*_α := Σ*_{α.base}
Σ^n_α := Σ^n_{α.base}
D_frame,α := D_frame_{α.base}
Frame_α := Frame_{α.base}
Lane_α := α.lanes
primitiveBindingOf_α := α.primitive_binding_of

laneBytes_α(λ) := primitiveBindingOf_α(λ).lane_descriptor
hashSuite_α(λ) := primitiveBindingOf_α(λ).hash_suite
IdSpace_α(λ) := Σ^{hashSuite_α(λ).output_length}_α

ProofParameter_α,λ :=
  primitiveBindingOf_α(λ).proof_parameter.carrier
Proof_α,λ := primitiveBindingOf_α(λ).proof_object.carrier
Context_α,λ := primitiveBindingOf_α(λ).context.carrier
Payload_α,λ := primitiveBindingOf_α(λ).payload.carrier
Index_α,λ := primitiveBindingOf_α(λ).index.carrier

transcriptTag_α,λ :=
  primitiveBindingOf_α(λ).transcript_tag
tag_α,λ(p) :=
  primitiveBindingOf_α(λ).hash_purpose_tags.apply(p)
D_LBH,α(λ,p) :=
  primitiveBindingOf_α(λ).covered_lbh_domain(p).holds
D_LBH_binding,α(λ,p) :=
  primitiveBindingOf_α(λ).covered_lbh_domain(p).binding

L_α,λ := primitiveBindingOf_α(λ).index_encoder.apply
encodeParameter_α,λ :=
  primitiveBindingOf_α(λ).parameter_encoder.apply
encodeContext_α,λ :=
  primitiveBindingOf_α(λ).context_encoder.apply
encodePayload_α,λ :=
  primitiveBindingOf_α(λ).payload_encoder.apply
identityContextBytes_α,λ :=
  primitiveBindingOf_α(λ).identity_context_bytes

8. Reference authority and system formation

8.1. Qualified Node Keys over a lane authority

For α : LaneAuthority:

QualifiedNodeKey_α :=
  DepPair (λ : Lane_α). IdSpace_α(λ)

Reference_α := QualifiedNodeKey_α

For q = ⟨λ,i⟩:

idBytes_α,λ(i) := i

ReferenceFrameValid_α(q) :=
  laneBytes_α(λ) ∈ D_frame,α
  ∧ idBytes_α,λ(i) ∈ D_frame,α

referenceBytes_α(q) :=
  Frame_α(laneBytes_α(λ))
  ‖ Frame_α(idBytes_α,λ(i))

referenceBytes_α represents the typed pair; it does not define dependent-pair equality.

8.2. Reference binding

For α : LaneAuthority and λ : Lane_α:

LaneReferenceBinding⟦α⟧(λ) := ⟨
  reference_shape : BoundPredicate_{α.base}[QualifiedNodeKey_α],
  reference_accumulator :
    BoundFunction_{α.base}[
      FinSeq QualifiedNodeKey_α,
      Σ*_α]
⟩

For a candidate reference binding b : LaneReferenceBinding⟦α⟧(λ):

CanonicalReferencesFor⟦α⟧(λ,b) :=
  { R : FinSeq Reference_α |
      (∀ r ∈ R. ReferenceFrameValid_α(r))
      ∧ (∀ r ∈ R. b.reference_shape.holds(r))
      ∧ R is duplicate-free by typed Reference_α equality
      ∧ (∀ i,j. i < j < |R| ⟹
           referenceBytes_α(R[i])
             <lex referenceBytes_α(R[j])) }

LaneReferenceBindingWellFormed⟦α⟧(λ,b) :=
  StableRuleBindingWellFormed_{α.base}(
    b.reference_shape.binding)
  ∧ StableRuleBindingWellFormed_{α.base}(
    b.reference_accumulator.binding)
  ∧ (∀ R,S : CanonicalReferencesFor⟦α⟧(λ,b).
       b.reference_accumulator.apply(R)
         = b.reference_accumulator.apply(S)
       ⟹ R = S)

The accumulator law is scoped to canonical references. It does not claim injectivity on arbitrary sequences.

ReferenceFrameValid_α(q) holds for every q : QualifiedNodeKey_α formed from a valid lane authority: laneBytes_α(λ) ∈ D_frame,α follows from LanePrimitiveBindingWellFormed (lane descriptor in frame), and idBytes_α,λ(i) = i ∈ D_frame,α holds because identifiers are digests of fixed output length and LanePrimitiveBindingWellFormed requires every digest-length string to lie in D_frame,α. Duplicate-freeness in CanonicalReferencesFor is implied by the strict <lex order together with injectivity of referenceBytes_α; these two conditions are stated explicitly so that Section 8.2 stands independently of Section 9.

8.3. Reference authority

A reference authority is:

ReferenceAuthority := ⟨
  lane_authority : LaneAuthority,
  reference_binding_of :
    (λ : lane_authority.lanes) →
      LaneReferenceBinding⟦lane_authority⟧(λ),
  reference_formation_proof :
    ∀ λ : lane_authority.lanes.
      LaneReferenceBindingWellFormed⟦lane_authority⟧(
        λ, reference_binding_of(λ))
⟩

This is the first formation stage that may mention Qualified Node Keys. It depends on a completed lane authority and does not feed back into lane formation.

For χ : ReferenceAuthority, write αχ := χ.lane_authority and define:

Lane_χ := Lane_αχ
QualifiedNodeKey_χ := QualifiedNodeKey_αχ
Reference_χ := Reference_αχ
referenceBindingOf_χ := χ.reference_binding_of

CanonicalReferences_χ,λ :=
  CanonicalReferencesFor⟦αχ⟧(
    λ, referenceBindingOf_χ(λ))

referenceAdmitted_χ,λ :=
  referenceBindingOf_χ(λ).reference_shape.holds
refsAccumulator_χ,λ :=
  referenceBindingOf_χ(λ).reference_accumulator.apply

The complete lane binding is the finite pair:

ClosedLaneBinding⟦χ⟧(λ) := ⟨
  primitive : LanePrimitiveBinding⟦αχ.base,Lane_χ⟧(λ),
  references : LaneReferenceBinding⟦αχ⟧(λ)
⟩

closedBindingOf⟦χ⟧(λ) := ⟨
  primitive := primitiveBindingOf_αχ(λ),
  references := referenceBindingOf_χ(λ)
⟩

8.4. Bodies and occurrences

For χ : ReferenceAuthority and λ : Lane_χ:

Body_χ,λ := ⟨
  parameter : ProofParameter_αχ,λ,
  context : Context_αχ,λ,
  payload : Payload_αχ,λ,
  index : Index_αχ,λ,
  references : CanonicalReferences_χ,λ
⟩

Occurrence_χ,λ := ⟨
  body : Body_χ,λ,
  proof : Proof_αχ,λ
⟩

Body_χ := DepPair (λ : Lane_χ). Body_χ,λ
Occurrence_χ := DepPair (λ : Lane_χ). Occurrence_χ,λ

Packing and projections are definitional. Proof objects are excluded from every construction below.

8.5. Identity construction before final closure

For χ : ReferenceAuthority, λ : Lane_χ, p : HashPurpose, and message : Σ*_αχ:

LBHInput_χ,λ(p,message) :=
  Frame_αχ(tag_αχ,λ(p))
  ‖ Frame_αχ(laneBytes_αχ(λ))
  ‖ message

LaneHashInputValid_χ,λ(p,message) :=
  tag_αχ,λ(p) ∈ D_frame,αχ
  ∧ laneBytes_αχ(λ) ∈ D_frame,αχ
  ∧ D_LBH,αχ(λ,p)(LBHInput_χ,λ(p,message))

LBH_χ,λ(p,message) :=
  hashSuite_αχ(λ).hash(LBHInput_χ,λ(p,message))

For b : Body_χ,λ:

ParameterMessage_χ,λ(b) :=
  Frame_αχ(encodeParameter_αχ,λ(b.parameter))

ContentMessage_χ,λ(b) :=
  Frame_αχ(encodeContext_αχ,λ(b.context))
  ‖ Frame_αχ(encodePayload_αχ,λ(b.payload))

ReferencesMessage_χ,λ(b) :=
  refsAccumulator_χ,λ(b.references)

ParameterDigest_χ,λ(b) :=
  LBH_χ,λ(parameterPurpose, ParameterMessage_χ,λ(b))

ContentDigest_χ,λ(b) :=
  LBH_χ,λ(contentPurpose, ContentMessage_χ,λ(b))

ReferencesDigest_χ,λ(b) :=
  LBH_χ,λ(referencesPurpose, ReferencesMessage_χ,λ(b))

The transcript contains six framed segments and one fixed-width index segment, ordered as shown:

Transcript_χ,λ(b) :=
    Frame_αχ(transcriptTag_αχ,λ)
  ‖ Frame_αχ(laneBytes_αχ(λ))
  ‖ Frame_αχ(identityContextBytes_αχ,λ)
  ‖ Frame_αχ(ParameterDigest_χ,λ(b))
  ‖ Frame_αχ(ContentDigest_χ,λ(b))
  ‖ L_αχ,λ(b.index)
  ‖ Frame_αχ(ReferencesDigest_χ,λ(b))

IdentifierMessage_χ,λ(b) :=
  Frame_αχ(Transcript_χ,λ(b))

identifier_χ,λ(b) :=
  LBH_χ,λ(identifierPurpose, IdentifierMessage_χ,λ(b))

qualifiedNodeKey_χ,λ(b) :=
  ⟨λ, identifier_χ,λ(b)⟩

Because IdentifierMessage frames the entire transcript, the assembled transcript is itself an identity-relevant frame input; its admissibility is exactly the IdentifierFrameValid conjunct of BodyConstructionValid. The reference accumulator output is used directly as a lane-bound-hash message and is not framed; it is therefore not required to lie in D_frame.

The fixed-width index is not additionally framed.

8.6. Construction validity and non-circular preimage languages

For b : Body_χ,λ:

ParameterFrameValid_χ,λ(b) :=
  encodeParameter_αχ,λ(b.parameter) ∈ D_frame,αχ

ContentFrameValid_χ,λ(b) :=
  encodeContext_αχ,λ(b.context) ∈ D_frame,αχ
  ∧ encodePayload_αχ,λ(b.payload) ∈ D_frame,αχ

TranscriptFrameValid_χ,λ(b) :=
  transcriptTag_αχ,λ ∈ D_frame,αχ
  ∧ laneBytes_αχ(λ) ∈ D_frame,αχ
  ∧ identityContextBytes_αχ,λ ∈ D_frame,αχ
  ∧ ParameterDigest_χ,λ(b) ∈ D_frame,αχ
  ∧ ContentDigest_χ,λ(b) ∈ D_frame,αχ
  ∧ ReferencesDigest_χ,λ(b) ∈ D_frame,αχ

IdentifierFrameValid_χ,λ(b) :=
  Transcript_χ,λ(b) ∈ D_frame,αχ

BodyConstructionValid_χ,λ(b) :=
  ParameterFrameValid_χ,λ(b)
  ∧ ContentFrameValid_χ,λ(b)
  ∧ TranscriptFrameValid_χ,λ(b)
  ∧ IdentifierFrameValid_χ,λ(b)
  ∧ LaneHashInputValid_χ,λ(
       parameterPurpose, ParameterMessage_χ,λ(b))
  ∧ LaneHashInputValid_χ,λ(
       contentPurpose, ContentMessage_χ,λ(b))
  ∧ LaneHashInputValid_χ,λ(
       referencesPurpose, ReferencesMessage_χ,λ(b))
  ∧ LaneHashInputValid_χ,λ(
       identifierPurpose, IdentifierMessage_χ,λ(b))

Given LanePrimitiveBindingWellFormed for the lane's primitive binding, the conjuncts ParameterFrameValid, ContentFrameValid, TranscriptFrameValid, and the first two conjuncts of each LaneHashInputValid instance (the purpose-tag and lane-descriptor frame memberships) are theorems that follow from LanePrimitiveBindingWellFormed alone. The contingent content of BodyConstructionValid_χ,λ(b) is exactly IdentifierFrameValid_χ,λ(b) together with the four D_LBH memberships.

The exact preimage languages range over all typed bodies. They are not filtered by BodyConstructionValid:

ParameterPreimageLanguage_χ,λ :=
  { LBHInput_χ,λ(parameterPurpose, ParameterMessage_χ,λ(b)) |
      b : Body_χ,λ }

ContentPreimageLanguage_χ,λ :=
  { LBHInput_χ,λ(contentPurpose, ContentMessage_χ,λ(b)) |
      b : Body_χ,λ }

ReferencesPreimageLanguage_χ,λ :=
  { LBHInput_χ,λ(referencesPurpose, ReferencesMessage_χ,λ(b)) |
      b : Body_χ,λ }

IdentifierPreimageLanguage_χ,λ :=
  { LBHInput_χ,λ(identifierPurpose, IdentifierMessage_χ,λ(b)) |
      b : Body_χ,λ }

ConstructionDomainClosed_χ(λ) :=
  ParameterPreimageLanguage_χ,λ
    ⊆ { x | D_LBH,αχ(λ,parameterPurpose)(x) }
  ∧ ContentPreimageLanguage_χ,λ
    ⊆ { x | D_LBH,αχ(λ,contentPurpose)(x) }
  ∧ ReferencesPreimageLanguage_χ,λ
    ⊆ { x | D_LBH,αχ(λ,referencesPurpose)(x) }
  ∧ IdentifierPreimageLanguage_χ,λ
    ⊆ { x | D_LBH,αχ(λ,identifierPurpose)(x) }

8.7. Final carrier system

A carrier system is:

CarrierSystem := ⟨
  reference_authority : ReferenceAuthority,
  body_inhabitant :
    ∀ λ : Lane_{reference_authority}.
      Body_{reference_authority,λ},
  construction_formation_proof :
    ∀ λ : Lane_{reference_authority}.
    ∀ b : Body_{reference_authority,λ}.
      BodyConstructionValid_{reference_authority,λ}(b)
⟩

body_inhabitant prevents system formation from succeeding only because a lane's body type is empty. It establishes one structural body per lane; it does not assert an accepted occurrence, inhabit the proof-object type, or import admission semantics. construction_formation_proof is a genuine witness over every typed body. It is not a proposition defined and then silently assumed. The inhabitant forces ProofParameter_λ, Context_λ, Payload_λ, and Index_λ to be inhabited for every lane; CanonicalReferences_λ is always inhabited by ε. Proof_λ may be empty, in which case Occurrence_λ is uninhabited for that lane.

This universal obligation is intentional. Body_χ,λ is the carrier of bodies for which the lane claims that identity construction is total; it is not an unrestricted raw-value universe later filtered by operational reachability or admission. A realization with D_frame,αχ = Σ*_{αχ} can usually discharge the frame clauses directly. A bounded frame domain already discharges encoder-output and digest admissibility at lane formation (Section 7.2); if D_frame,αχ cannot contain them, LanePrimitiveBindingWellFormed fails before any CarrierSystem is attempted. The residual construction-formation obligation is that every assembled transcript remains in D_frame,αχ and that the four lane-bound-hash domains cover their preimage languages. A realization that combines an unbounded carrier with a frame domain too small to contain every resulting construction does not form a CarrierSystem.

Forming a CarrierSystem does not by itself establish HashInjectiveOn for any lane or hash purpose. HashSuiteWellFormed places no injectivity requirement on hash; a lane whose hash is a constant function can still form a valid CarrierSystem. Identity uniqueness (Section 10) requires this as a separate, additional hypothesis. The exactness-certificate layer in Section 10.7 names lanes for which that additional hypothesis has been supplied.

One instance κ : CarrierSystem is fixed for the remainder of the document. It is arbitrary but fixed: every construction and theorem schema below is parametric in κ and may be instantiated with any carrier system. Let χκ := κ.reference_authority and ακ := χκ.lane_authority. The following unqualified aliases are local to this same κ:

Σ := Σ_ακ
Σ* := Σ*_ακ
Σ^n := Σ^n_ακ
D_frame := D_frame,ακ
Frame := Frame_ακ
ParseFrame := ParseFrame_{ακ.base}

StableRuleBinding := StableRuleBinding_{ακ.base}
BoundType := BoundType_{ακ.base}
BoundFunction := BoundFunction_{ακ.base}
BoundPredicate := BoundPredicate_{ακ.base}
HashSuite := HashSuite_{ακ.base}

StableRuleBindingWellFormed :=
  StableRuleBindingWellFormed_{ακ.base}
HashSuiteWellFormed := HashSuiteWellFormed_{ακ.base}

Lane := Lane_χκ
QualifiedNodeKey := QualifiedNodeKey_χκ
Reference := Reference_χκ
Body_λ := Body_χκ,λ
Occurrence_λ := Occurrence_χκ,λ
Body := Body_χκ
Occurrence := Occurrence_χκ
CanonicalReferences_λ := CanonicalReferences_χκ,λ

primitiveBindingOf(λ) := primitiveBindingOf_ακ(λ)
referenceBindingOf(λ) := referenceBindingOf_χκ(λ)
ClosedLaneBinding(λ) := ClosedLaneBinding⟦χκ⟧(λ)
bindingOf(λ) := closedBindingOf⟦χκ⟧(λ)

laneBytes(λ) := laneBytes_ακ(λ)
hashSuite(λ) := hashSuite_ακ(λ)
IdSpace(λ) := IdSpace_ακ(λ)
ProofParameter_λ := ProofParameter_ακ,λ
Proof_λ := Proof_ακ,λ
Context_λ := Context_ακ,λ
Payload_λ := Payload_ακ,λ
Index_λ := Index_ακ,λ

transcriptTag_λ := transcriptTag_ακ,λ
tag_λ := tag_ακ,λ
D_LBH(λ,p) := { x | D_LBH,ακ(λ,p)(x) }
D_LBHBinding(λ,p) := D_LBH_binding,ακ(λ,p)
L_λ := L_ακ,λ
encodeParameter_λ := encodeParameter_ακ,λ
encodeContext_λ := encodeContext_ακ,λ
encodePayload_λ := encodePayload_ακ,λ
identityContextBytes_λ := identityContextBytes_ακ,λ
referenceAdmitted_λ := referenceAdmitted_χκ,λ
refsAccumulator_λ := refsAccumulator_χκ,λ

ReferenceFrameValid := ReferenceFrameValid_ακ
referenceBytes := referenceBytes_ακ
LBHInput_λ := LBHInput_χκ,λ
LaneHashInputValid_λ := LaneHashInputValid_χκ,λ
LBH_λ := LBH_χκ,λ
ParameterMessage_λ := ParameterMessage_χκ,λ
ContentMessage_λ := ContentMessage_χκ,λ
ReferencesMessage_λ := ReferencesMessage_χκ,λ
ParameterDigest_λ := ParameterDigest_χκ,λ
ContentDigest_λ := ContentDigest_χκ,λ
ReferencesDigest_λ := ReferencesDigest_χκ,λ
Transcript_λ := Transcript_χκ,λ
IdentifierMessage_λ := IdentifierMessage_χκ,λ
identifier_λ := identifier_χκ,λ
qualifiedNodeKey_λ := qualifiedNodeKey_χκ,λ
BodyConstructionValid_λ := BodyConstructionValid_χκ,λ

ParameterPreimageLanguage_λ :=
  ParameterPreimageLanguage_χκ,λ
ContentPreimageLanguage_λ := ContentPreimageLanguage_χκ,λ
ReferencesPreimageLanguage_λ :=
  ReferencesPreimageLanguage_χκ,λ
IdentifierPreimageLanguage_λ :=
  IdentifierPreimageLanguage_χκ,λ
ConstructionDomainClosed(λ) :=
  ConstructionDomainClosed_χκ(λ)

The proof-bearing consequences are:

LanePrimitiveWellFormed(λ) :=
  LanePrimitiveBindingWellFormed⟦ακ.base,Lane⟧(
    λ, primitiveBindingOf(λ))

LanePrimitiveFormation(λ) :
  LanePrimitiveWellFormed(λ) :=
    ακ.primitive_formation_proof(λ)

ReferenceBindingWellFormed(λ) :=
  LaneReferenceBindingWellFormed⟦ακ⟧(
    λ, referenceBindingOf(λ))

ReferenceBindingFormation(λ) :
  ReferenceBindingWellFormed(λ) :=
    χκ.reference_formation_proof(λ)

LaneWellFormed(λ) :=
  LanePrimitiveWellFormed(λ)
  ∧ ReferenceBindingWellFormed(λ)

LaneFormation(λ) : LaneWellFormed(λ) :=
  ⟨LanePrimitiveFormation(λ),
   ReferenceBindingFormation(λ)⟩

LaneBindingValid(λ,b) :=
  b = bindingOf(λ) ∧ LaneWellFormed(λ)

BodyInhabitant(λ) : Body_λ :=
  κ.body_inhabitant(λ)

BodyConstructionFormation(λ,b) :
  BodyConstructionValid_λ(b) :=
    κ.construction_formation_proof(λ,b)

ConstructionDomainFormation(λ) :
  ConstructionDomainClosed(λ)

ConstructionDomainFormation follows by expanding the four preimage languages and applying BodyConstructionFormation to their witness bodies. It is not circular because those languages contain every typed body without a validity filter.

9. Canonical references, body projections, and ReferenceBytesInjective

Theorem ReferenceBytesInjective states that referenceBytes is injective on frame-valid references. For q = ⟨λ,i⟩, dependent-pair equality gives lane equality before same-lane identifier equality:

ReferenceFrameValid(q₁)
∧ ReferenceFrameValid(q₂)
∧ referenceBytes(q₁) = referenceBytes(q₂)
  ⟹ q₁ = q₂

The proof uses frame cancellation, ακ.lane_descriptor_unique, and typed identifier equality. Because ReferenceFrameValid holds for every QNK in a valid lane authority (established in Section 8.2), the frame-valid premises of this injectivity theorem are always satisfied and need not be separately discharged by callers.

Packing and projections are definitional:

packBody(λ,b) := ⟨λ,b⟩
packOccurrence(λ,c) := ⟨λ,c⟩
laneOfBody(⟨λ,b⟩) := λ
laneOfOccurrence(⟨λ,c⟩) := λ
bodyOfOccurrence(⟨λ,c⟩) := ⟨λ,c.body⟩
bodyValue(⟨λ,b⟩) := b
referencesOfBody(⟨λ,b⟩) := b.references

10. Exact structural laws

The theorem schemas in this section are exact structural laws. They are normative consequences of the definitions when their stated premises hold. They do not impose formation obligations on CarrierSystem unless an ExactnessCertificate is asserted.

Exact hash injectivity is a mathematical premise, not an implementation property. Concrete instantiations cannot generally satisfy exact injectivity over infinite preimage languages with finite hash output spaces. Such instantiations rely on computational collision resistance specified outside this core.

The dependency skeleton of the exact laws is:

identifier equality
  + identifier-purpose hash injectivity
  + construction-valid identifier preimages
    ⇒ transcript equality

transcript equality
  + frame left cancellation
  + fixed-width injective index encoding
    ⇒ component-digest equality and index equality

component-digest equality
  + construction-specific hash injectivity
  + injective canonical encoders / reference accumulator
    ⇒ component source-value equality

component equality
    ⇒ body equality

No stage imports an admission, evidence, cost, computational, comparison, or policy premise.

10.1. Hash injectivity on a named language

For λ : Lane, p : HashPurpose, and a language S:

HashInjectiveOn(λ,p,S) :=
  S ⊆ D_LBH(λ,p)
  ∧ ∀ x,y ∈ S.
      hashSuite(λ).hash(x) = hashSuite(λ).hash(y)
        ⟹ x = y

The purpose-specific domain-closure conjunct is part of the premise rather than an external side condition. For the four named preimage languages, ConstructionDomainFormation(λ) supplies that conjunct; only exact hash injectivity remains an independent assumption. This premise is not implied by hash-suite formation.

HashInjectiveOn(λ,p,S) is an exact idealization. It is satisfiable only when |S| ≤ |Σ^{hashSuite(λ).output_length}|; when an identity-relevant carrier makes S infinite, the premise is uninhabitable and every theorem citing it holds vacuously. A realization discharges these theorems only computationally, by replacing each exact-injectivity premise with collision resistance of the lane’s hash suite on the corresponding language. That substitution is outside this core.

10.2. Theorem IdentifierTranscriptBinding

For a,b : Body_λ:

BodyConstructionValid_λ(a)
∧ BodyConstructionValid_λ(b)
∧ HashInjectiveOn(
    λ, identifierPurpose, IdentifierPreimageLanguage_λ)
∧ identifier_λ(a) = identifier_λ(b)
  ⟹ Transcript_λ(a) = Transcript_λ(b)

The actual identifier preimage is:

LBHInput_λ(identifierPurpose, Frame(Transcript_λ(b)))

10.3. Theorem TranscriptDecomposition

For a,b : Body_λ:

BodyConstructionValid_λ(a)
∧ BodyConstructionValid_λ(b)
∧ Transcript_λ(a) = Transcript_λ(b)
  ⟹ ParameterDigest_λ(a) = ParameterDigest_λ(b)
   ∧ ContentDigest_λ(a) = ContentDigest_λ(b)
   ∧ a.index = b.index
   ∧ ReferencesDigest_λ(a) = ReferencesDigest_λ(b)

The proof uses five applications of frame left cancellation, equality of fixed-width index prefixes, injectivity of L_λ, and frame injectivity for the final reference digest.

10.4. Theorems ExactParameterRecovery, ExactContentRecovery, ExactReferencesRecovery

For a,b : Body_λ, each component theorem explicitly includes construction validity:

BodyConstructionValid_λ(a)
∧ BodyConstructionValid_λ(b)
∧ HashInjectiveOn(
    λ, parameterPurpose, ParameterPreimageLanguage_λ)
∧ ParameterDigest_λ(a) = ParameterDigest_λ(b)
  ⟹ a.parameter = b.parameter

BodyConstructionValid_λ(a)
∧ BodyConstructionValid_λ(b)
∧ HashInjectiveOn(
    λ, contentPurpose, ContentPreimageLanguage_λ)
∧ ContentDigest_λ(a) = ContentDigest_λ(b)
  ⟹ a.context = b.context
   ∧ a.payload = b.payload

BodyConstructionValid_λ(a)
∧ BodyConstructionValid_λ(b)
∧ HashInjectiveOn(
    λ, referencesPurpose, ReferencesPreimageLanguage_λ)
∧ ReferencesDigest_λ(a) = ReferencesDigest_λ(b)
  ⟹ a.references = b.references

These conclusions additionally use the injective canonical encoders and reference accumulator carried by the formation proofs.

10.5. Theorem ExactBodyBinding 

ExactBodyBindingPremises(λ) :=
  HashInjectiveOn(
    λ, identifierPurpose, IdentifierPreimageLanguage_λ)
  ∧ HashInjectiveOn(
    λ, parameterPurpose, ParameterPreimageLanguage_λ)
  ∧ HashInjectiveOn(
    λ, contentPurpose, ContentPreimageLanguage_λ)
  ∧ HashInjectiveOn(
    λ, referencesPurpose, ReferencesPreimageLanguage_λ)

BodyConstructionValid_λ(a)
∧ BodyConstructionValid_λ(b)
∧ ExactBodyBindingPremises(λ)
∧ identifier_λ(a) = identifier_λ(b)
  ⟹ a = b

10.6. Theorem QualifiedKeyUniqueness 

BodyConstructionValid_λ(a)
∧ BodyConstructionValid_μ(b)
∧ qualifiedNodeKey_λ(a) = qualifiedNodeKey_μ(b)
∧ ExactBodyBindingPremises(λ)
  ⟹ ∃ h : λ = μ.
        transport_h(a) = b

The equality witness is bound by the conclusion. The lane-equality witness extracted from the key equality transports the construction-validity witness and the exact-body-binding premises from λ to μ before exact body binding is applied in lane μ. No proof-irrelevance or implicit choice of a lane-equality proof is assumed.

10.7. Exactness certificates

Exactness is not a formation stage. It is a proof-bearing layer over a formed carrier system. No field of LaneAuthority, ReferenceAuthority, or CarrierSystem depends on this layer, and forming a CarrierSystem does not force any lane to satisfy the exact-body-binding premises.

For χ : ReferenceAuthority, define:

D_LBH_χ(λ,p) := { x | D_LBH,χ.lane_authority(λ,p)(x) }
hashSuite_χ(λ) := hashSuite_{χ.lane_authority}(λ)

HashInjectiveOn_χ(λ,p,S) :=
  S ⊆ D_LBH_χ(λ,p)
  ∧ ∀ x,y ∈ S.
      hashSuite_χ(λ).hash(x) = hashSuite_χ(λ).hash(y)
        ⟹ x = y

For ι : CarrierSystem, write χι := ι.reference_authority. Define:

ExactBodyBindingPremises⟦ι⟧(λ) :=
  HashInjectiveOn_{χι}(
    λ, identifierPurpose, IdentifierPreimageLanguage_{χι,λ})
  ∧ HashInjectiveOn_{χι}(
    λ, parameterPurpose, ParameterPreimageLanguage_{χι,λ})
  ∧ HashInjectiveOn_{χι}(
    λ, contentPurpose, ContentPreimageLanguage_{χι,λ})
  ∧ HashInjectiveOn_{χι}(
    λ, referencesPurpose, ReferencesPreimageLanguage_{χι,λ})

ExactLanePredicate(ι) :=
  { λ : Lane_{χι} |
      ExactBodyBindingPremises⟦ι⟧(λ) }

An exactness certificate is:

ExactnessCertificate := ⟨
  base : CarrierSystem,
  exact_lanes : Set (Lane_{base.reference_authority}),
  exact_lanes_sound :
    ∀ λ ∈ exact_lanes.
      ExactBodyBindingPremises⟦base⟧(λ)
⟩

For ε : ExactnessCertificate, define:

baseOfExact(ε) := ε.base
ExactLanes(ε) := ε.exact_lanes
exactLanesSound(ε) := ε.exact_lanes_sound

Applied to a carrier system ι, ExactLanePredicate(ι) denotes the derived exact-lane predicate. Applied to an exactness certificate ε, ExactLanes(ε) denotes the carried set ε.exact_lanes. The two names are distinct; neither is an overload of the other. The soundness field makes the carried set a lower bound for the derived predicate:

λ ∈ ExactLanes(ε)
  ⟹ ExactBodyBindingPremises⟦baseOfExact(ε)⟧(λ)

and therefore:

ExactLanes(ε) ⊆ ExactLanePredicate(baseOfExact(ε)).

The layer is a certificate, not a classification. The empty set is always an admissible carried set, two exactness certificates over the same base may carry different sets, and a larger carried set carries strictly more proof content. Membership asserts a proof; non-membership asserts nothing.

For the fixed instance κ of Section 8.7, HashInjectiveOn(λ,p,S) in Section 10.1 is exactly HashInjectiveOn_{χκ}(λ,p,S), and ExactBodyBindingPremises(λ) in Section 10.5 is exactly ExactBodyBindingPremises⟦κ⟧(λ); the unqualified names are the κ-instances of the parameterized definitions.

When an exactness certificate ε with baseOfExact(ε) = κ is fixed, a theorem schema in Section 10.2–Section 10.6 that requires the four hash-injectivity premises for a lane λ may be instantiated with the single hypothesis λ ∈ ExactLanes(ε). This hypothesis unfolds to the same four HashInjectiveOn premises and does not assert that every lane of the base is exact.

11. Structural graphs

11.1. Graph scope and state 

ReferenceBoundary :=
    ClosedBoundary
  | OpenBoundary(
      allowed_external : Reference × QualifiedNodeKey → Prop)

GraphScope := ⟨
  object_domain : Set Body,
  graph_universe : Set QualifiedNodeKey,
  reference_boundary : ReferenceBoundary
⟩

GraphState := ⟨
  vertices : FinSet QualifiedNodeKey,
  body_of : FinMap QualifiedNodeKey Body,
  exact_vertex_domain : domain(body_of) = vertices
⟩

For q ∈ G.vertices, bodyAt(G,q) denotes the unique value G.body_of[q] established by exact_vertex_domain.

11.2. Derived edges 

ReferenceEdges(G) :=
  { (r,q) : QualifiedNodeKey × QualifiedNodeKey |
      q ∈ G.vertices
      ∧ r ∈ referencesOfBody(bodyAt(G,q)) }

InternalEdges(G) :=
  ReferenceEdges(G) ∩ (G.vertices × G.vertices)

The orientation is (referenced, referencing). No independent edge relation is an input.

11.3. Key consistency, scope, and closure 

KeyConsistent(G) :=
  ∀ q ∈ G.vertices.
    let packedBody := bodyAt(G,q) in
    let λ := laneOfBody(packedBody) in
    q = qualifiedNodeKey_λ(bodyValue(packedBody))

GraphInScope(G,scope) :=
  G.vertices ⊆ scope.graph_universe
  ∧ ∀ q ∈ G.vertices.
      bodyAt(G,q) ∈ scope.object_domain

ClosureValid(G,scope) :=
  match scope.reference_boundary with
    ClosedBoundary ->
      ∀ (r,q) ∈ ReferenceEdges(G). r ∈ G.vertices
    OpenBoundary(allowed_external) ->
      ∀ (r,q) ∈ ReferenceEdges(G).
        r ∈ G.vertices ∨ allowed_external(r,q)

allowed_external is a proposition over Reference × QualifiedNodeKey and is not constrained to lie within graph_universe. This is intentional: an external reference may designate a node in a different graph or universe; the open boundary predicate is supplied by the caller and may be empty, universal, or otherwise scoped as needed.

11.4. Paths and internal acyclicity 

Path(G,source,target) :=
  source ∈ G.vertices
  ∧ target ∈ G.vertices
  ∧ ∃ v : FinSeq QualifiedNodeKey.
      |v| ≥ 2
      ∧ v[0] = source
      ∧ v[|v|−1] = target
      ∧ (∀ j < |v|. v[j] ∈ G.vertices)
      ∧ (∀ j : Nat. j+1 < |v| ⟹
           (v[j],v[j+1]) ∈ InternalEdges(G))

InternallyAcyclic(G) :=
  ¬∃ q ∈ G.vertices. Path(G,q,q)

11.5. Structural graph validity 

StructuralGraphValid(G,scope) :=
  GraphInScope(G,scope)
  ∧ (∀ q ∈ G.vertices.
       let packedBody := bodyAt(G,q) in
       BodyConstructionValid_{laneOfBody(packedBody)}(
         bodyValue(packedBody)))
  ∧ KeyConsistent(G)
  ∧ ClosureValid(G,scope)
  ∧ InternallyAcyclic(G)

For a closed boundary, this establishes a finite directed acyclic graph. For an open boundary, it still establishes graph scope, body-construction validity, key consistency, closure relative to the explicit external-reference predicate, and internal acyclicity. It does not establish acyclicity after external references are resolved. An importing specification that requires global acyclicity MUST define additional closure or validation rules.

12. Security Considerations

This specification defines an abstract identity and structural-graph model. It does not by itself provide confidentiality, integrity, authenticity, availability, or denial-of-service protection. The following considerations apply:

  1. A valid CarrierSystem does not imply identifier uniqueness. Identifier uniqueness requires the exact hash-injectivity premises defined in Section 10.1 and Section 10.5. A lane whose hash function is constant can still form a valid CarrierSystem, but MUST NOT be assumed to provide collision-resistant identity binding.
  2. An ExactnessCertificate whose exact_lanes set is empty provides no exact-body-binding assurance for any lane. Its existence alone MUST NOT be interpreted as evidence that identifier uniqueness holds; assurance extends only to lanes explicitly included in exact_lanes.
  3. The exact injectivity premises are mathematical idealizations. When an identity-relevant carrier induces an infinite preimage language and the hash output space is finite, exact injectivity is unsatisfiable. Concrete instantiations therefore rely on computational collision resistance of the selected hash suite. The choice of hash function, output length, and security margin is outside the scope of this core and MUST be specified by importing protocols; hash-algorithm agility for those selections is addressed by BCP 201 [RFC7696].
  4. Implementations MUST ensure that the frame codec is deterministic and unambiguous. Ambiguous parsing or non-canonical framing can cause distinct serialized forms to produce the same logical object, or the same serialized form to be interpreted differently.
  5. Canonical references are ordered by referenceBytes to prevent reference-order malleability. The reference accumulator MUST be injective on canonical reference sequences; otherwise two distinct canonical reference sets could produce the same references digest.
  6. The four hash-purpose tags MUST remain pairwise distinct, and the transcript tag MUST remain distinct from all of them. Losing the first separation can allow one hash purpose to be confused with another; losing the second can allow a framed transcript to be confused with a lane-bound-hash input. Either failure weakens the identifier binding.
  7. StableRuleBinding digests are not validated by this core; a stable binding is a nominal anchor, not a self-verifying cryptographic credential. This core does not require owner_id, rule_id, revision, or digest values to be unique or globally meaningful; importing specifications that assign administrative, version-control, governance, or trust semantics to these fields MUST define uniqueness, validation, and binding rules. An importing specification that assigns trust, governance, or version-control semantics to these digests MUST define the binding between each digest and its semantic content.
  8. The identity_context_bytes field is an explicit identity input. This specification does not define its semantics. If an importing specification assigns security-relevant meaning to this field, that specification MUST define how the field is validated, bound, and protected against substitution.
  9. Open graph boundaries permit external references. StructuralGraphValid establishes internal acyclicity only. It does not establish acyclicity after external references are resolved. Protocols that resolve external references MUST define their own cycle-prevention rules if global acyclicity is required. External references are Qualified Node Keys over the same lane authority: they may designate nodes absent from the current graph, but they do not designate nodes of a different lane authority or identifier scheme, and cross-authority references require an explicit mapping defined outside this core.
  10. Proof objects are excluded from body identity. Two occurrences with the same body but different proofs have the same Qualified Node Key. Proof validation, admission, and trust are out of scope for this core.
  11. Identifiers are content-derived. If the selected hash suite lacks preimage resistance, or if parameter, context, payload, or reference data are low-entropy or guessable, identifiers may reveal or allow enumeration of the underlying content. Importing specifications that require confidentiality MUST specify preimage-resistance and entropy requirements or additional protective measures.
  12. Because identity is content-derived, identical bodies produce identical Qualified Node Keys. This may enable correlation across graphs, sessions, or importing protocols. If unlinkability is required, importing specifications MUST define context separation, salting, or encryption mechanisms outside this core.
  13. Implementations SHOULD impose bounded limits on frame length, reference sequence length, graph vertex and edge counts, and proof object size; validation of large structural graphs may require significant memory and processing resources, and resource limits and rejection policies are outside this core.
  14. Predicates such as D_LBH, reference_shape, and allowed_external are mathematical propositions in this core. Operational implementations MUST use decidable, bounded validation procedures when these predicates are evaluated at runtime.
  15. Because GraphState keys vertices by Qualified Node Key, two distinct bodies with the same key cannot appear as separate vertices. Detection or handling of identifier collisions requires exactness premises or additional rules outside this core.

13. IANA Considerations

This document has no IANA actions.

This specification does not create any IANA registries. Stable bindings, lane descriptors, hash-suite bindings, transcript tags, hash-purpose tags, and related identifiers are administrative or protocol-local values unless an importing specification defines a registry for them.

14. References

14.1. Normative References

[RFC2119]
Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, DOI 10.17487/RFC2119, , <https://www.rfc-editor.org/info/rfc2119>.
[RFC8174]
Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174, , <https://www.rfc-editor.org/info/rfc8174>.

14.2. Informative References

[RFC6920]
Farrell, S., Kutscher, D., Dannewitz, C., Ohlman, B., Keranen, A., and P. Hallam-Baker, "Naming Things with Hashes", RFC 6920, DOI 10.17487/RFC6920, , <https://www.rfc-editor.org/info/rfc6920>. Comparison point for content-derived naming; no syntax or registry from RFC 6920 is imported.
[RFC8949]
Bormann, C. and P. Hoffman, "Concise Binary Object Representation (CBOR)", STD 94, RFC 8949, DOI 10.17487/RFC8949, , <https://www.rfc-editor.org/info/rfc8949>. Comparison point for deterministic framing and decoding; no CBOR data model or encoding rule is imported.
[RFC8785]
Rundgren, A., Jordan, B., and S. Erdtman, "JSON Canonicalization Scheme (JCS)", RFC 8785, DOI 10.17487/RFC8785, , <https://www.rfc-editor.org/info/rfc8785>. Comparison point for canonical representation discipline; no JSON syntax or canonicalization rule is imported.
[RFC9052]
Schaad, J., "CBOR Object Signing and Encryption (COSE): Structures and Process", STD 96, RFC 9052, DOI 10.17487/RFC9052, , <https://www.rfc-editor.org/info/rfc9052>. Comparison point for protected algorithm and context binding; no COSE structure is imported.
[RFC9162]
Laurie, B., Messeri, E., and R. Stradling, "Certificate Transparency Version 2.0", RFC 9162, DOI 10.17487/RFC9162, , <https://www.rfc-editor.org/info/rfc9162>. Comparison point for finite authenticated graph structures; no log protocol or Merkle construction is imported.
[RFC9562]
Davis, K., Peabody, B., and P. Leach, "Universally Unique IDentifiers (UUIDs)", RFC 9562, DOI 10.17487/RFC9562, , <https://www.rfc-editor.org/info/rfc9562>. Comparison point for name-based identifiers that truncate digests into a fixed 128-bit format; no UUID version, format, or namespace rule is imported.
[FIPS180-4]
National Institute of Standards and Technology, "Secure Hash Standard (SHS)", NIST FIPS 180-4, DOI 10.6028/NIST.FIPS.180-4, , <https://csrc.nist.gov/pubs/fips/180-4/upd1/final>. Example family of fixed-output hash functions; this core does not select a concrete hash.
[SP800-185]
Kelsey, J., Chang, S., and R. Perlner, "SHA-3 Derived Functions: cSHAKE, KMAC, TupleHash, and ParallelHash", NIST SP 800-185, DOI 10.6028/NIST.SP.800-185, , <https://csrc.nist.gov/pubs/sp/800/185/final>. Comparison point for domain separation; no construction from SP 800-185 is imported.
[RFC7696]
Housley, R., "Guidelines for Cryptographic Algorithm Agility and Selecting Mandatory-to-Implement Algorithms", BCP 201, RFC 7696, DOI 10.17487/RFC7696, , <https://www.rfc-editor.org/info/rfc7696>. Guidance for hash-algorithm selection and agility in importing protocols; no requirement from BCP 201 is imported into this core.

Appendix A. Formation dependency order

The core is formed in the following strict order:

Substrate
  ↓
LaneAuthority
  ↓
QualifiedNodeKey over that authority
  ↓
ReferenceAuthority
  ↓
Body and identity constructions
  ↓
CarrierSystem with body inhabitant and construction-formation witness

No record field depends on a later stage. In particular:

The optional exactness layer is not a formation dependency of the records above:

CarrierSystem
  ↓ (optional)
ExactnessCertificate

It depends only on a completed CarrierSystem and the exact-body-binding premises; no earlier record depends on it.

Appendix B. Core invariants

The following are definitional or proof-bearing parts of κ:

  1. The substrate is formed before lanes and carries parser round-trip and parser-soundness formation; frame left cancellation and frame injectivity are derived.
  2. Every lane has exactly one primitive binding and one reference binding.
  3. Every primitive and reference binding has a formation witness.
  4. Lane descriptors are injective inside the finite lane authority.
  5. The transcript tag is separate from and distinct from the four hash-purpose tags.
  6. D_LBH(λ,p) and its stable binding are explicit lane fields for every hash purpose.
  7. Every lane has at least one typed body.
  8. Every typed body has a construction-formation witness.
  9. Every construction preimage language ranges over all typed bodies and is included in its declared lane-bound-hash domain.
  10. Proof objects are excluded from body identity.
  11. Qualified Node Key equality is dependent-pair equality, and cross-lane body transport binds its equality witness explicitly.
  12. Reference edges are derived only from canonical body references.
  13. Structural graph validity is independent of evidence, admission, and resource availability.

Appendix C. Exactness invariants (require ExactnessCertificate)

The following invariants are not part of CarrierSystem formation. They hold only when an ExactnessCertificate ε is supplied:

  1. ExactLanes(ε) contains only lanes λ for which all four HashInjectiveOn premises in ExactBodyBindingPremises⟦baseOfExact(ε)⟧(λ) hold.
  2. Membership λ ∈ ExactLanes(ε) is proof-bearing evidence for exact body binding in that lane.
  3. A lane may form a valid CarrierSystem and still be absent from a given ExactnessCertificate; absence from exact_lanes does not imply failure of ExactBodyBindingPremises.
  4. If a lane does not satisfy ExactBodyBindingPremises⟦baseOfExact(ε)⟧, it cannot belong to ExactLanes(ε) for any exactness certificate ε over that base.
  5. A lane whose hash suite is constant on a preimage language with two distinct inputs cannot belong to ExactLanes(ε), since the corresponding HashInjectiveOn premise fails.
  6. The exactness layer does not make hash injectivity computationally true; it names where the exact idealization is assumed.

Appendix D. Extension boundary

An importing specification MAY define additional judgments over values from this core. It MUST NOT redefine, override, weaken, strengthen, or shadow any type, record, function, predicate, formation rule, derived frame law, or theorem schema defined by this core. These prohibitions apply to specifications that claim conformance to Carrier Identity Core and to definitions presented as Carrier Identity definitions; they do not prohibit the reuse of generic identifiers such as Body, Reference, or Lane in unrelated contexts that are not presented as conformant Carrier Identity definitions. This prohibition applies to the complete declaration surface of the referenced version of this document; the following identity- and graph-critical names are illustrative and non-exhaustive:

Substrate
FrameCodec
FrameCodecWellFormed
FrameLeftCancellation
FrameInjective
StableRuleBinding
HashPurpose
LaneAuthority
ReferenceAuthority
CarrierSystem
Lane
bindingOf
D_LBH
LBHInput_λ
LaneHashInputValid_λ
LBH_λ
Body_λ
Occurrence_λ
BodyConstructionValid_λ
ConstructionDomainClosed
ParameterDigest_λ
ContentDigest_λ
ReferencesDigest_λ
Transcript_λ
identifier_λ
QualifiedNodeKey
qualifiedNodeKey_λ
Reference
referenceBytes
CanonicalReferences_λ
GraphState
ReferenceEdges
InternalEdges
KeyConsistent
ClosureValid
InternallyAcyclic
StructuralGraphValid
HashInjectiveOn_χ
ExactBodyBindingPremises⟦ι⟧
ExactLanePredicate
ExactLanes
ExactnessCertificate
baseOfExact

An imported relation MAY compare, admit, evaluate, or govern core values, but it does not rewrite their formation, structural identity, reference interpretation, or graph truth.

Appendix E. ASCII Equivalents for Formal Tooling

This appendix is informative.

The following ASCII equivalents are provided for tooling convenience. They do not change the normative meaning of the mathematical notation.

Table 2
Unicode ASCII Meaning
Σ Sigma Finite alphabet
Σ* SigmaStar Finite sequences over Sigma
Σ^n Sigma^n Sequences of length n
ε epsilon Empty sequence
‖ || Sequence concatenation
⇀ partial Partial function arrow
∈ in Set/sequence membership
∀ forall Universal quantifier
∃ exists Existential quantifier
⟹ implies Logical implication
⟺ iff Logical equivalence
∧ and Conjunction
¬ not Negation
⊆ subseteq Set inclusion
λ lambda Lane variable
μ mu Lane variable
χ chi Reference authority variable
κ kappa Carrier system variable
β beta Substrate variable
α alpha Lane authority variable
⟨x,y⟩ <x,y> Dependent pair / record
⟦x⟧ [[x]] Parameterized definition
|s| length(s) Sequence length
<lex lex_less Lexicographic order
− - Minus

Appendix F. Derivations of the Core Theorem Schemas

This appendix is informative. It provides condensed derivations for theorem schemas stated in the main body; the normative statements remain those in the main body. Every derivation depends only on definitions and proof-bearing formation fields from the main body and consumes no admission, evidence, resource, computational, comparison, or policy premise.

F.1. Premise abbreviations

For one fixed lane λ and bodies a,b : Body_λ, write BodiesValid(λ,a,b) for BodyConstructionValid_λ(a) ∧ BodyConstructionValid_λ(b), and write ExactBindingAssumptions(λ) for the four hash-injectivity premises of ExactBodyBindingPremises(λ) in Section 10.5. These are abbreviations only and introduce no additional premise. Each HashInjectiveOn(λ,p,S) includes the subset condition S ⊆ D_LBH(λ,p); for the named preimage languages that condition is supplied by ConstructionDomainFormation(λ).

F.2. Frame laws and framed-segment decomposition

FrameInjective (Section 6.1): for x,y ∈ D_frame with Frame(x) = Frame(y), apply parser round-trip with empty tails; ParseFrame is single-valued, so x = y. FrameLeftCancellation (Section 6.1): apply round-trip to both sides of a framed-prefix equality; the two successful parse results are equal, yielding equality of the admitted values and of the tails. By induction using left cancellation, an equality of two concatenations of the same number of framed admitted segments followed by tails yields pairwise equality of the segments and equality of the tails.

F.3. Transcript decomposition

For BodiesValid(λ,a,b) with Transcript_λ(a) = Transcript_λ(b): cancel the three lane-derived frames (transcript tag, lane descriptor, identity context bytes) and then the parameter-digest and content-digest frames. The remaining suffixes have the form L_λ(index) ‖ Frame(ReferencesDigest). Both index encodings have the fixed width declared by bindingOf(λ), so the fixed-width prefixes are equal; index-encoder injectivity gives a.index = b.index, and frame injectivity recovers references-digest equality. The frame membership of every component digest is supplied by TranscriptFrameValid, a conjunct of BodyConstructionValid. This derives the theorem of Section 10.3.

F.4. Identifier binding, component recovery, and body binding

For the theorem of Section 10.2: the identifier preimages LBHInput_λ(identifierPurpose, Frame(Transcript_λ(·))) of a and b lie in IdentifierPreimageLanguage_λ; hash injectivity on that language yields preimage equality, cancellation of the fixed purpose-tag and lane-descriptor frames yields equality of the framed transcripts, and frame injectivity — with transcript frame membership supplied by IdentifierFrameValid — yields transcript equality. For each recovery theorem of Section 10.4, hash injectivity on the corresponding preimage language yields preimage equality; cancellation of the fixed frames leaves the framed canonical encodings (parameter; context and payload) or the accumulator output (references); encoder injectivity, or accumulator injectivity on CanonicalReferences_λ supplied by ReferenceBindingWellFormed(λ), recovers the source components. The theorem of Section 10.5 composes these steps: transcript equality, digest and index equality by Appendix F.3, component recovery, and record extensionality — two records of the same telescopic record type are equal when all corresponding fields are equal.

F.5. Qualified-key transport

Let e : qualifiedNodeKey_λ(a) = qualifiedNodeKey_μ(b). Equality of dependent pairs gives h_e := congrArg(firstProjection, e) : λ = μ and, after transport, transport^{IdSpace}_{h_e}(identifier_λ(a)) = identifier_μ(b). A coherence lemma proved by path induction on h_e gives identifier_μ(transport^{Body}_{h_e}(a)) = transport^{IdSpace}_{h_e}(identifier_λ(a)); transitivity yields same-lane identifier equality in lane μ. Transporting the left body's construction-validity witness and ExactBindingAssumptions(λ) along h_e and applying exact body binding in lane μ gives transport_{h_e}(a) = b, deriving the theorem of Section 10.6. The witness is extracted from the same key equality; no proof irrelevance or hidden choice of a lane-equality proof is used.

F.6. Reference and closed-graph consequences

ReferenceBytesInjective (Section 9) follows by cancelling the lane frames, applying lane-descriptor uniqueness, and cancelling the identifier frames; its frame-valid premises hold for every Qualified Node Key in a valid lane authority. Consequently the order induced on references by referenceBytes and <lex is strict and total, so two canonical reference sequences with extensionally equal typed membership are equal: both are strictly increasing under the same order, hence share the same head and, inductively, the same tail. For a closed boundary, ClosureValid places the referenced endpoint of every derived edge in G.vertices while the referencing endpoint is internal by the definition of ReferenceEdges, so ReferenceEdges(G) = InternalEdges(G); with G.vertices finite, each body carrying a finite canonical reference sequence, and InternallyAcyclic(G) excluding every directed cycle, a valid closed structural graph is a finite directed acyclic graph in the orientation (referenced, referencing).

Author's Address

Thanh Le
Viet Nam