Source changed 2026-10-03 08:25:59 UTC · snapshot created 2026-10-03 08:26:43 UTC · last check 2026-10-03 09:20:09 UTC
A.6.0:7 - Conformance Checklist
Exact declaration object. The text identifies one U.Signature episteme and one exact EntityOfConcernRef.
Identity. Content, EntityOfConcern, and effective U.ReferenceScheme remain recoverable.
Minimum content.SubjectKind and RangedValueKind, together with Vocabulary, Laws, and Applicability, carry semantic content rather than empty publication rows. ResultKind, SliceSet, and ExtentRule appear only when their declared distinctions are current.
Optional slice-dependent membership.SliceSet names the addressable U.ContextSlice values to inspect and ExtentRule determines Extension(SubjectKind, slice) only when the same declared kind can have different members across those slices; neither field stands for a generic interval, range, changing dataset, or set representation.
Vocabulary boundary. A declared token is not treated as durable U-kind admission without E.24.UK and its direct pattern.
Relation declaration. A RelationSignature identifies one exact already admitted direct relation kind. An admitted derived relation kind has direct subject settlement for participant meanings, base-definition and named-substrate dependencies, obtaining, applicability, and occurrence identity. A predicate-definition episteme is not treated as that RelationSignature, and the declaration does not assert an occurrence. Every worked case that uses a RelationSignature also names the already admitted relation kind, direct governor and predicate, participant meanings, Applicability, occurrence-identity rule, and one ordinary affirmative or negative assertion. A hypothetical domain-local relation kind is labelled and fully settled before the example uses it.
Direct relation-pattern governance. The direct relation pattern defines or constrains obtaining and occurrence identity.
Typed-declaration boundary. Reused participant meanings are declared inside a RelationSignature by A.6.5 SlotSpecs with exact SlotKind, ValueKind, and refMode. Operation arguments and results remain A.6.1 declaration content. Mathematical operands and field order remain representation-side under A.6.3.RT; C.29 opens only when a named mathematical lens changes the declared lens use or next comparison action. An operand-to-participant correspondence is stated only for an already governed relation claim.
Semantic locality. Meaning uses the effective reference scheme; applicability uses the exact claim scope and only qualifiers current for the declaration, such as a relevant time interval, selected CHR:ReferencePlane, or genuinely current model-use structure.
Dependency truth. Every import names the provider and exact term or law without which interpretation or law replay fails; every provide entry names a dependent declaration that relies on the introduced term or law. Citations and list order do not qualify. SM-1 through SM-4 hold, and a replay cycle is distinguished from a semantic-prohibition verdict.
Realization boundary. Mechanism behavior and admission conditions remain with A.6.1.
Progressive elaboration. A direct assertion is enough when the task only asks whether the predicate holds; a signature opens when at least two named consumers share declaration content; occurrence identity opens only for a later same-occurrence reference, comparison, qualification, history/change claim, or relation participation. A log or assertion identifier alone opens none of them.
CGUS boundary. Judge any condition-governed unfolding claim through A.22.CGUS, using the independently identified structure and continuation conditions stated in §4.
Profile boundary. FormalSubstrate and PrincipleFrame remain profiles of U.Signature rather than new root kinds. A PrincipleFrame names its postulates and the observable distinctions needed to check them, leaves operation and gate admission with their subject patterns, and uses F.9 for a relation between two exact F.17 local senses, citing a Bridge only when its direct predicate obtains.
Changed object. Changed exact claim content carried by the U.ClaimGraph, exact EntityOfConcern, or effective reference scheme identifies another episteme. Judge A.6.0 membership for that episteme independently, and assert edition, refinement, supersession, or another continuity relation only when its own predicate obtains. A changed use, identifier, publication form, carrier, provider currentness, or G.11 refresh state does none of those things by itself.
F.19 self-application and reader use. Apply F.19 by value to every materially changed technical declaration, mantra, checklist instruction, and worked case; revalidate the changed span with its meaning-dependent neighbours. The cold intended reader must be able to recover the same governed object, subject pattern, admissible use, and practical claim or action, including any result that changes that use. Keep ordinary technical wording when it already carries the needed distinctions; unpack terms or add an explanation only when recovery needs it. Use E.10:11 item 16 when the value-substitution question is selected. State a nearby non-use or contrasting case only when F.19:4’s full guard test warrants it. A Plain label without that reader-visible recovery does not pass.
Case-level witness. Each worked case names its exact EntityOfConcern, the direct pattern that defines or constrains the claim being made, and what the practitioner can now write, decide, or inspect. State the nearest category error it rejects only when F.19:4’s full guard test warrants that contrast. A domain label or the presence of several case headings is not evidence of cross-domain fit.