ZLM4 Logical Artifacts and Identities

C3-ART-001 — Logical envelope and version boundary

This edition specifies zerglang.zlm4-logical/1, not an executable binary container. Each logical record is {schema, kind, payload}. schema is exactly zerglang.zlm4-logical/1; kind selects one closed payload schema below. Unknown versions, kinds, fields, or term tags are rejected. References are typed {kind, sha256} pairs and must name records of the declared kind. External content references are {format, sha256, bytes}: exact format identifier, lowercase SHA-256 hex, and canonical unsigned decimal byte count.

The companion zlm4-logical.schema.json is the normative structural schema (JSON Schema draft-07). It is a repository specification asset, not a runtime loader. JSON shape validation establishes neither typing nor authority; all relational/semantic rules in this edition additionally apply. Every referenced preimage required by a judgment must be available and validated. Opaque unavailable content can be displayed as a reference, not admitted as checked content. Limits are explicit implementation/profile limits, never silent truncation of a proof or a dependency closure.

ZLM1, ZLM2, and ZLM3 imports retain their original format/edition semantics. ZLM4 records can reference their exact bytes and checked semantic projections; they do not rewrite their version, domain tags, contract modes, or trust labels. Physical ZLM4 section layout, ABI handles, loader integration, and byte packing are deferred. The identity framing below is fully specified independently.

C3-ART-002 — Record families and required meaning

Kind	Payload and admission meaning
authority	Exact source bytes, package-relative path, named UTF-8 byte ranges
declaration	Qualified name, universe count, earlier dependencies, typed definition/axiom/inductive form
environment	Kernel version, imported environments, ordered declarations, named axiom profiles
statement	Checked environment and proposition term; no author assertion of its truth
proof	Expected statement reference and completed term; footprint is derived, not supplied here
model	Environment, paradigm, input/trace/outcome/observation types, logical semantics and observation terms, numeric profile, assumptions, external sources, disclosed trust
bridge	Exact external subject/contract/implementation, model and observation map, mode, obligation statements, adequacy proofs or named trust
extraction	Computational term/environment, contract, representation relation, target artifact, preservation evidence/trust
intent	Authority, input/output types, static candidate-effect bound, policy, individually identified prose requirements
request	Intent, typed input content, context roles/disclosure policy, policy, generator configuration, budgets, parent and nonce
formalization	Intent/authority, authenticated proposer, checked contract/environment, complete requirement mappings, obligations, assumptions, unresolved items
policy	Approval delegation, evidence choices, axiom/trust allowlists, providers/operations, capability requirements, resource limits
approval	Request, exact formalization/authority/policy, principal, delegation provenance, approval or denial
generation	Request, provider/model/protocol, recipe/parameters, sent context, response and usage
implementation	Formalization, revision/predecessor, checked code or typed operation-plan product
admission	Request/approval/formalization/implementation, predecessor, evidence, checker identity, required live capabilities
execution	Request/admission, phase/outcome, typed output if any, consumed resources, action/uncertainty receipts, diagnostic, predecessor

Resource records use canonical unsigned decimal strings for attempts, revisions, elapsed milliseconds, input/output tokens, model micro-cost, proof steps, proof-memory bytes, context/artifact bytes, and actions. billing_unit names the cost unit. Counters use the same units as limits; peak memory is recorded as a high-water mark. Amounts never use floating point. The host enforces each limit, aggregate parent limits, and reservation rules before dispatch.

C3-ART-003 — Terms and dependency closure

Core terms are tagged objects: var(index), const(name,levels), sort(level), pi(domain,body), lam(domain,body), app(function,argument), and let(type,value,body). Binder names are erased using zero-based de Bruijn indices (zero is the innermost binder); indices/counts are unsigned decimal strings. Universe parameters also use zero-based declaration-local indices. Level tags are zero, param(index), succ(of), max(left,right), and imax(left,right). These tags encode syntax, not a trusted inferred type.

An environment resolves a constant name to exactly one declaration, constructor, or generated recursor. Conflicting definitions of a qualified name are rejected; identical imported declaration identities may be shared. Environment imports and declaration dependencies form acyclic graphs. The single checked inductive cluster is encoded as one declaration: its parameters, index telescope, sort, and ordered constructors with field telescopes and result indices. Generated names are I.constructor and I.rec; collisions are rejected. References to the family’s own name within that cluster are admitted only by the inductive rules, not by general forward recursion.

Telescope term indices refer to preceding parameters/indices/fields in their declared order. Constructor fields see fixed parameters and earlier fields; constructor result indices see those same bindings. The family index telescope is not an extra implicit constructor parameter list. The generated recursor’s argument order is fixed parameters, motive, constructor branches in declaration order, indices, then the scrutinee. No implicit parameters survive serialization.

Environment profile definitions are named unions of exact axiom declarations and earlier profile names; profile union cycles and rebinding standard names are rejected. Check each declaration’s type, body, universe scope, and actual references. Claimed dependency lists must equal the direct referenced global declaration set, excluding names generated inside the current inductive cluster. An interface-only signature is not a completed declaration record.

C3-ART-004 — Canonical identity encoding

Canonical JSON for this profile admits strings, booleans, null, arrays, and objects; JSON numbers are forbidden. Natural numbers are decimal strings matching 0|[1-9][0-9]*. Input strings must be valid Unicode scalar sequences; unpaired surrogates are invalid. Do not normalize Unicode. Preserve prose bytes after UTF-8 decoding/encoding; no newline or whitespace normalization.

Object keys are ASCII and serialized in ascending unsigned ASCII byte order; duplicates are rejected before object construction. Arrays preserve their specified order. There is no insignificant whitespace. String escaping uses \" for quote, \\ for backslash, lowercase \u00xx for U+0000–U+001F, and literal UTF-8 for every other scalar (including slash and U+2028/U+2029). Short escapes such as \n are accepted as input spelling but canonicalize to the specified six-byte escape. Booleans/null use lowercase JSON tokens.

Let B be the UTF-8 canonical JSON of the complete envelope, with no ID or signature field. Its identity is lowercase hex SHA-256 of:

UTF8("ZERGLANG-ZLM4-ID") || 0x00 ||
UTF8("1") || 0x00 || UTF8(kind) || 0x00 ||
ASCII(decimal(byte_length(B))) || 0x00 || B

The version and kind are domain separators. The record cannot contain its own ID in the hash preimage. Signatures/authenticated receipt bindings are external to the identified record and, if used, bind its typed ID plus the policy scope. An unsigned principal string is not authentication. Host admission must verify approval provenance using its authenticated principal/delegation mechanism; cross-host claims need an explicitly admitted authentication profile.

Two records have the same identity only when their canonical envelopes match, subject to the hash collision assumption. This is syntactic identity, not logical equivalence, English equivalence, or proof of authorship. Definitional equality can relate differently identified statements only through a checked comparison in the exact environment; it does not rewrite their identities.

C3-ART-005 — Canonical ordering and authority binding

Set-like arrays (imports, direct dependencies, profile axiom/base sets, trust and capability lists) are duplicate-free and sorted by UTF-8 bytes of their canonical element encoding. Ordered declarations, constructor fields, requirements, argument lists, observations, events, and plan output bindings retain source/semantic order. Plan nodes use the stable topological ordering defined by the runtime; predecessor lists are sorted node-ID sets. Effect sets use the fixed Core-3 effect order, not arbitrary lexical order. Identity canonicalization must not reorder program effects, proof applications, or requirements. It must not beta-normalize terms or erase proof bodies.

Authority paths are normalized package-relative paths without empty, dot, parent, absolute, or backslash-separated components. They identify provenance within the sealed package, not permission to open an ambient filesystem path. Authority ranges are half-open UTF-8 byte offsets, within the exact source and on scalar boundaries; names are unique. Requirement fragments must resolve to the selected authority. Formalizations map every requirement exactly once to obligations or an explicit policy-admitted assumption, or report it unresolved. No mapping may name a nonexistent requirement or obligation. Unresolved entries prevent admission. An approval must bind the request’s selected intent, authority, policy, and exact formalization. Its delegation must authorize the principal and scope; independent-approval requirements compare the authenticated approver with the authenticated formalization proposer. Policy assurance pairs are conjunctive as specified in C3-INTENT-006, not alternatives.

C3-ART-006 — Evidence and revision binding

Proof evidence binds an actual checked Proof record and its checker-derived axiom footprint. Non-proof evidence instead binds an exact test/check/measurement or trust artifact with its own semantics and provenance. An evidence kind must match the obligation and policy; a test record cannot be cast to proof. Every pre-effect obligation must have passed evidence for admission. Only explicitly post-effect runtime-check/empirical obligations may be pending; their required enforcement remains part of the admitted execution contract. Failed, missing, unsupported, or inconclusive pre-evidence prevents admission.

Revision zero has no predecessor. Subsequent implementation revisions increase by one and reference the preceding implementation under the same formalization. Admission revisions likewise bind the exact new candidate and prior admission when replacing an admitted revision. A candidate that was never admitted may be retried without fabricating a prior admission. Replans bind the recorded current-state input and outstanding obligations through the request’s Flow activity context; the accepted contract is unchanged. Execution receipts form an acyclic predecessor chain and never overwrite history.

completed requires an admitted implementation, declared-type output, no unresolved external effects, and all required postchecks passed in the recorded events. indeterminate must identify the uncertain actions. Other terminal outcomes have a diagnostic and no success output. Shape-valid evidence or receipts not satisfying these relationships are rejected, not trusted because their hashes match.

C3-ART-007 — Invalidation and projections

Change	Consequence
Prose/range/requirement meaning	New authority/intent and interpretation approval; unchanged standalone proofs can survive
Formal statement/environment/axioms	Recheck dependent proof and policy bindings
Implementation or typed-plan composition	New implementation identity; recheck affected verification/admission
Model, observation map, numeric profile	Recheck bridge-dependent claims
Generator provenance only	New provenance; do not call an unchanged theorem false, but revalidate policy/cache eligibility
Revoked live capability	Prevent new dispatch; historical proof/approval records remain immutable

Public interfaces expose only authorized names, signatures, statement IDs, assumption summaries, evidence kinds/status, and public lineage. Semantic/private projections include bodies only with content-access authority. Do not export private prompts, inputs, proof bodies, source fragments, or capability handles by default. Hashes can reveal equality of confidential content and are themselves subject to publication policy. An omitted private preimage is explicitly unavailable, not an empty body that an external checker may treat as verified.

The canonical runtime projection is specified by C3-RUN-007. Physical ZLM4 packing and executable loaders cannot be introduced under an old version or by accepting unknown fields.