Network Working Group T. Le Internet-Draft 25 July 2026 Intended status: Informational Expires: 26 January 2027 Carrier Identity Core: A Proof-Bearing Kernel for Content-Derived Node Identity and Structural Graphs draft-le-carrier-identity-core-00 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. Le Expires 26 January 2027 [Page 1] Internet-Draft Carrier Identity Core July 2026 Copyright Notice Copyright (c) 2026 IETF Trust and the persons identified as the document authors. All rights reserved. This document is subject to BCP 78 and the IETF Trust's Legal Provisions Relating to IETF Documents (https://trustee.ietf.org/ license-info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document. Code Components extracted from this document must include Revised BSD License text as described in Section 4.e of the Trust Legal Provisions and are provided without warranty as described in the Revised BSD License. Table of Contents 1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 3 2. Terminology . . . . . . . . . . . . . . . . . . . . . . . . . 4 3. Conventions and Definitions . . . . . . . . . . . . . . . . . 5 4. Core Conformance Requirements . . . . . . . . . . . . . . . . 6 5. Scope and independence . . . . . . . . . . . . . . . . . . . 7 5.1. Mathematical notation . . . . . . . . . . . . . . . . . . 9 6. Substrate . . . . . . . . . . . . . . . . . . . . . . . . . . 9 6.1. Parameterized frame codec . . . . . . . . . . . . . . . . 9 6.2. Base record . . . . . . . . . . . . . . . . . . . . . . . 10 6.3. Stable semantic bindings . . . . . . . . . . . . . . . . 11 7. Primitive lane authority . . . . . . . . . . . . . . . . . . 12 7.1. Hash suites and hash purposes . . . . . . . . . . . . . . 12 7.2. Primitive lane binding . . . . . . . . . . . . . . . . . 13 7.3. Lane authority record . . . . . . . . . . . . . . . . . . 15 8. Reference authority and system formation . . . . . . . . . . 16 8.1. Qualified Node Keys over a lane authority . . . . . . . . 17 8.2. Reference binding . . . . . . . . . . . . . . . . . . . . 17 8.3. Reference authority . . . . . . . . . . . . . . . . . . . 18 8.4. Bodies and occurrences . . . . . . . . . . . . . . . . . 19 8.5. Identity construction before final closure . . . . . . . 20 8.6. Construction validity and non-circular preimage languages . . . . . . . . . . . . . . . . . . . . . . . . 21 8.7. Final carrier system . . . . . . . . . . . . . . . . . . 23 9. Canonical references, body projections, and ReferenceBytesInjective . . . . . . . . . . . . . . . . . 27 10. Exact structural laws . . . . . . . . . . . . . . . . . . . . 28 10.1. Hash injectivity on a named language . . . . . . . . . . 29 10.2. Theorem IdentifierTranscriptBinding . . . . . . . . . . 30 10.3. Theorem TranscriptDecomposition . . . . . . . . . . . . 30 10.4. Theorems ExactParameterRecovery, ExactContentRecovery, ExactReferencesRecovery . . . . . . . . . . . . . . . . 30 10.5. Theorem ExactBodyBinding . . . . . . . . . . . . . . . . 31 Le Expires 26 January 2027 [Page 2] Internet-Draft Carrier Identity Core July 2026 10.6. Theorem QualifiedKeyUniqueness . . . . . . . . . . . . . 31 10.7. Exactness certificates . . . . . . . . . . . . . . . . . 32 11. Structural graphs . . . . . . . . . . . . . . . . . . . . . . 33 11.1. Graph scope and state . . . . . . . . . . . . . . . . . 34 11.2. Derived edges . . . . . . . . . . . . . . . . . . . . . 34 11.3. Key consistency, scope, and closure . . . . . . . . . . 34 11.4. Paths and internal acyclicity . . . . . . . . . . . . . 35 11.5. Structural graph validity . . . . . . . . . . . . . . . 35 12. Security Considerations . . . . . . . . . . . . . . . . . . . 36 13. IANA Considerations . . . . . . . . . . . . . . . . . . . . . 38 14. References . . . . . . . . . . . . . . . . . . . . . . . . . 38 14.1. Normative References . . . . . . . . . . . . . . . . . . 38 14.2. Informative References . . . . . . . . . . . . . . . . . 39 Appendix A. Formation dependency order . . . . . . . . . . . . . 40 Appendix B. Core invariants . . . . . . . . . . . . . . . . . . 41 Appendix C. Exactness invariants (require ExactnessCertificate) . . . . . . . . . . . . . . . . . . 42 Appendix D. Extension boundary . . . . . . . . . . . . . . . . . 42 Appendix E. ASCII Equivalents for Formal Tooling . . . . . . . . 44 Appendix F. Derivations of the Core Theorem Schemas . . . . . . 45 F.1. Premise abbreviations . . . . . . . . . . . . . . . . . . 45 F.2. Frame laws and framed-segment decomposition . . . . . . . 45 F.3. Transcript decomposition . . . . . . . . . . . . . . . . 46 F.4. Identifier binding, component recovery, and body binding . . . . . . . . . . . . . . . . . . . . . . . . . 46 F.5. Qualified-key transport . . . . . . . . . . . . . . . . . 46 F.6. Reference and closed-graph consequences . . . . . . . . . 47 Author's Address . . . . . . . . . . . . . . . . . . . . . . . . 47 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 Le Expires 26 January 2027 [Page 3] Internet-Draft Carrier Identity Core July 2026 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 +=============+=============================================+ | 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 | A finite nominal lane type together with | | authority | 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 | A lane authority extended with one proof- | | authority | bearing reference binding for each lane. | +-------------+---------------------------------------------+ | Closed lane | The pair consisting of a lane's primitive | | binding | 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 | Le Expires 26 January 2027 [Page 4] Internet-Draft Carrier Identity Core July 2026 | | object. The proof object is not an | | | identity input. | +-------------+---------------------------------------------+ | Hash | One of the four lane-bound-hash roles: | | purpose | parameter, content, references, or | | | identifier. The transcript tag is not a | | | hash purpose. | +-------------+---------------------------------------------+ | Lane-bound | Hashing of an explicit hash-purpose tag | | hashing | frame, lane-descriptor frame, and message | | | under the suite fixed by the lane. | +-------------+---------------------------------------------+ | Qualified | The dependent pair (lane, identifier). It | | Node Key | is the structural graph key. | +-------------+---------------------------------------------+ | Canonical | A duplicate-free, strictly ordered finite | | references | sequence of Qualified Node Keys admitted by | | | a lane. | +-------------+---------------------------------------------+ | Structural | A finite Qualified-Node-Key map to node | | graph | 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 | A proof-bearing layer over a carrier system | | certificate | that names lanes proven to satisfy the four | | | exact-body-binding hash-injectivity | | | premises. | +-------------+---------------------------------------------+ Table 1 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. Le Expires 26 January 2027 [Page 5] Internet-Draft Carrier Identity Core July 2026 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. Le Expires 26 January 2027 [Page 6] Internet-Draft Carrier Identity Core July 2026 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 Le Expires 26 January 2027 [Page 7] Internet-Draft Carrier Identity Core July 2026 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: * computational security experiments; * evidence records; * obligation registries; * proof admission; * resource evaluation; * semantic comparison; * fork classification; * lineage, transition choice, recovery, or branch preference; * governance; or * consensus, liveness, and finality. 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. Le Expires 26 January 2027 [Page 8] Internet-Draft Carrier Identity Core July 2026 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: Le Expires 26 January 2027 [Page 9] Internet-Draft Carrier Identity Core July 2026 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: Le Expires 26 January 2027 [Page 10] Internet-Draft Carrier Identity Core July 2026 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 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. Le Expires 26 January 2027 [Page 12] Internet-Draft Carrier Identity Core July 2026 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: Le Expires 26 January 2027 [Page 13] Internet-Draft Carrier Identity Core July 2026 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,β) Le Expires 26 January 2027 [Page 14] Internet-Draft Carrier Identity Core July 2026 ∧ (∀ 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 ⟹ λ = μ ⟩ Le Expires 26 January 2027 [Page 15] Internet-Draft Carrier Identity Core July 2026 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 Le Expires 26 January 2027 [Page 16] Internet-Draft Carrier Identity Core July 2026 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]) ∀ (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) Le Expires 26 January 2027 [Page 35] Internet-Draft Carrier Identity Core July 2026 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. Le Expires 26 January 2027 [Page 36] Internet-Draft Carrier Identity Core July 2026 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. Le Expires 26 January 2027 [Page 37] Internet-Draft Carrier Identity Core July 2026 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 Le Expires 26 January 2027 [Page 38] Internet-Draft Carrier Identity Core July 2026 [RFC2119] Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, DOI 10.17487/RFC2119, March 1997, . [RFC8174] Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174, May 2017, . 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, April 2013, . 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, December 2020, . 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, June 2020, . 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, August 2022, . 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, December 2021, . Comparison point for finite authenticated graph structures; no log protocol or Merkle construction is imported. Le Expires 26 January 2027 [Page 39] Internet-Draft Carrier Identity Core July 2026 [RFC9562] Davis, K., Peabody, B., and P. Leach, "Universally Unique IDentifiers (UUIDs)", RFC 9562, DOI 10.17487/RFC9562, May 2024, . 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, August 2015, . 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, December 2016, . 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, November 2015, . 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: Le Expires 26 January 2027 [Page 40] Internet-Draft Carrier Identity Core July 2026 * lane formation does not mention references or Qualified Node Keys; * reference formation depends on a completed lane authority; * non-vacuous construction closure depends on completed primitive and reference bindings; and * no formation proof is introduced outside the record that owns it. 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. Le Expires 26 January 2027 [Page 41] Internet-Draft Carrier Identity Core July 2026 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 Le Expires 26 January 2027 [Page 42] Internet-Draft Carrier Identity Core July 2026 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 Le Expires 26 January 2027 [Page 43] Internet-Draft Carrier Identity Core July 2026 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. +=========+===========+==============================+ | 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 | Le Expires 26 January 2027 [Page 44] Internet-Draft Carrier Identity Core July 2026 +---------+-----------+------------------------------+ | κ | kappa | Carrier system variable | +---------+-----------+------------------------------+ | β | beta | Substrate variable | +---------+-----------+------------------------------+ | α | alpha | Lane authority variable | +---------+-----------+------------------------------+ | ⟨x,y⟩ | | Dependent pair / record | +---------+-----------+------------------------------+ | ⟦x⟧ | [[x]] | Parameterized definition | +---------+-----------+------------------------------+ | |s| | length(s) | Sequence length | +---------+-----------+------------------------------+ |