Appendix B — Conformance Checklist

Normative

Purpose

This checklist enumerates every numbered property defined in the Mars® Protocol. An implementation is conformant with a given section if and only if every numbered property listed for that section is satisfied by the implementation, verifiable by an independent qualified third-party inspector through external-observation differential testing — without internal access to the system and without trust in the deploying organization.

A qualified independent inspector is defined as: a person or entity with no contractual relationship with the licensee, no access to the licensee’s internal systems or source code, and sufficient technical competence to execute the testing protocol described for each property.

Verification posture for universal-absence properties. Properties asserting universal absence — no path bypasses, no configuration produces, no override exists — are verified by falsification, not by proof: external-observation testing can refute such a property with a single counterexample but cannot prove it over all possible inputs and configurations. A conformance assessment against a universal-absence property is therefore evidence of non-refutation under the executed test corpus (including adversarial differential testing and the implementation’s declared-surface attestations); a counterexample discovered at any later time defeats conformance from the moment of discovery. This posture is uniform across the checklist and is the same falsifiability discipline the specification imposes on the artifacts it governs.

Precedence. Each property is defined in the property table of its normative section; this appendix is the normative aggregation of those tables, adding the Inspector-verifiable classification and the licensing-tier assignment. On any conflict between a section’s property table and this appendix concerning a property’s definition or observable condition, the section table governs. On the Inspector-verifiable classification and the Required-for tier assignment, this appendix governs. Any divergence between the two is a defect to be repaired, not a latitude to be exploited; conformance may not be claimed under the weaker of two divergent statements.

How to read this table

Property — the identifier as it appears in the normative text
Section — the normative section in which the property is defined
Description — the observable behavior the property asserts
Inspector-verifiable — whether an independent inspector can verify this property by external-observation differential testing alone (Y), or whether it requires access to retained evidence (E), or both (Y/E)
Required for — the minimum Triad layer a deployment must license to be required to satisfy this property

§01 Juno — Domain Modeling

Property	Section	Description	Inspector-verifiable	Required for
D0	§01 §14	No model artifact distinct from the language — every use or amendment is an observably well-typed composition; no path bypasses the type system	Y	Juno
D1	§01 §14	Order-typed terms — DSL terms carry order-types observable on the terms and on the lowered artifact; every term of an order instantiates the order’s shape	Y	Juno
D2	§01 §14	Rejection by order-type — engine rejects a composition solely because of the terms’ order-types, emitting a typed error	Y	Juno
D3	§01 §14	Perspective-typed terms — DSL terms carry perspective tags observable on the terms and on the lowered artifact; cross-perspective relationship records are present and typed	Y	Juno
D4	§01 §14	Variant-typed terms — DSL terms carry variant identifiers; lossy variants carry explicit information-loss records in the lowered artifact	Y	Juno
D5	§01 §14	Higher-order type extension — introducing a higher-order output observably extends the set of compositions that type-check	Y	Juno
D6	§01 §14	Deterministic, auditable lowering — identical well-typed input lowers to an identical artifact, bound to source by a recomputation witness an inspector can re-derive	Y/E	Juno
D7	§01 §14	NL-free checking/lowering — the same artifact is produced regardless of any natural-language surface upstream; NL is absent from the checking and lowering paths	Y	Juno
D8	§01 §14	Context-free reuse — the lowered artifact and type-check result are consumed by two or more distinct consumers without re-derivation	Y	Juno
D9	§01 §14	Dimension-aware lifecycle — a change between two revisions is reported by order-typed, perspective-tagged, or variant-typed element, not by text line; an edit regenerates only the affected dimension portion	Y/E	Juno
D10	§01 §14	Synthesized higher-order output is type-checked and auditable — a higher-order synthesis producing an emergent output observably type-checks and is re-derivable from the composition provenance record; the declared input selection is observable in the provenance record	Y/E	Juno
D11	§01 §14	Unconstrained input selection in higher-order synthesis — a higher-order synthesis drawing from a single order alone, a single perspective alone, a cross-dimension combination, or a prior higher-order output all produce type-checked, auditable outputs under the same mechanism	Y/E	Juno
D12	§01 §14	NL-free path independent of upstream authoring — the checking and lowering paths contain no NL-interpretation step irrespective of upstream authoring method	Y	Juno
D13	§01 §14	Relational metrics are typed, scaled, and mechanism-recorded — each relational metric record carries metric type, value, scale declaration, and mechanism record; substituting a different mechanism produces an observably different mechanism record	Y/E	Juno
D14	§01 §14	Cross-order and cross-perspective metrics present — the formal model artifact contains relational metric records with element pairs drawn from different orders and from different stakeholder perspectives	E	Juno
D15	§01 §14	Embedding fine-tuning benchmark gate — a fine-tuned embedding model used for relational quantification carries a model-behavior certificate against the governed benchmark; a model without such a certificate is not used	Y	Juno
D16	§01 §14	Variant consistency map present and versioned — a variant consistency map is present for every declared variant entity with overlapping content; conflict entries are recorded and traceable to gap signals; map version is bound to model version	E	Juno
D17	§01 §14	Variant map navigability — an inspector can enter the model at any variant and traverse to the corresponding expression in any other variant via the consistency map; the traversal is entry-point-agnostic	Y	Juno
D18	§01 §14	Variant verification independence — each verified variant entity carries a verification record naming independent sources; the generating model is not the sole verification source	E	Juno
D19	§01 §14	Verification-gap entries recorded — variant entities where declared verification sources did not converge are present in the consistency map as `verification-gap` entries, not silently omitted or promoted	E	Juno
D20	§01 §14	Update-scoped re-verification — a model element change triggers re-verification only for variant entities referencing the changed element; unchanged pairs are not re-verified; the scope is traceable from the change record	Y/E	Juno
D21	§01 §14	Input-mode provenance in domain specification — the domain specification carries the input mode(s) used and their provenance; inferential candidates carry confidence annotations; escalation records are present where ambiguities were resolved by authority	E	Juno
D22	§01 §14	Structured-data interpretation record — where structured data was used as input, the domain specification carries an interpretation record identifying legibly-mapped, inferred, and unresolved fields	E	Juno
D23	§01 §14	KB input mode provenance — where an existing KB was used as an input mode, the domain specification carries the KB version and derivation provenance; the mutual-generativity chain is recomputable from the provenance record	E	Juno
D24	§01 §14	Lossy-provenance flag propagation — a predicate, metric, or higher-order output derived from a lossy variant carries an observable lossy-provenance flag; the flag is not stripped at any point in the derivation chain	Y	Juno
D25	§01 §14	Composition provenance record completeness — every higher-order output carries a composition provenance record with all minimum required fields; the provenance record hash is verifiable	E	Juno
D26	§01 §14	Conditional attestation triggers enumerated — where boundary-closure attestation is conditional, the adjudication gate record identifies the trigger type and the corresponding record identifier for each conditionally-attested element	E	Juno
D27	§01 §14	Domain model plurality and composability — the architecture operates more than one domain model or declares the capacity to do so; domain models are independently operable; analysis over one does not require re-derivation from another	Y	Juno
D28	§01 §14	Formal specification two-face structure — a formal specification carries an observable executable face and, where declared, observable governed bindings on the metadata face; the metadata face is not required for validity or certifiability	E	Juno
D29	§01 §14	Externally-provided specification bootstrap path — where an external specification was input to domain model creation, the domain specification carries its identity, version, and issuing-body authority; the bootstrapped model’s standing declaration is observable; a formal specification is never present as an input in this record	E	Juno
D30	§01 §14	Emitted bundle five-component co-presence — a registered formal specification carries all five bundle components; a bundle missing any component is refused at registration with a typed rejection identifying the absent component	Y	Juno
D31	§01 §14	Adjudication hierarchy and agreement-statistic hard gate — the adjudication gate record identifies the adjudication form, the agreement statistic identity, computed value, registered threshold, and per-predicate attestations; below-threshold registration is non-conforming with no override path; latent adjudication carries an observable conditional-attestation status	Y/E	Juno
D32	§01 §14	Scope certificate distinctness from metadata — the scope-of-applicability certificate is a distinct signed, falsifiable registered claim; its declared input-space, context conditions, and temporal bounds are not inferable from the metadata face; an out-of-scope input is observably not covered	Y/E	Juno
D33	§01 §14	Certifying adjudication trust signal observable and inherited — the adjudication record carries a certifying or conditional trust-signal class; verdicts inherit the class in their provenance chain; an inspector distinguishes the two without deployment access; a gate equating them is non-conforming	Y/E	Juno
D34	§01 §14	Soundness declaration present, validated, and discharge-parameterizing — the bundle carries a validated, content-hashed soundness declaration included in the version identifier; the discharge engine is observably parameterized on the declaration; bespoke per-specification logic without consulting the declaration is non-conforming regardless of verdict agreement	Y/E	Juno
D35	§01 §14	Governing collection registered and activation-event-logged — a deployment operating plural artifacts or non-static activation carries a registered governing collection; the activation event log records every activation/deactivation with trigger, evaluated condition, and timestamp; past active sets are determinable from the log alone	E	Juno
D36	§01 §14	Dimension-level activation observable in recomputation witness — every witness for an operation activating a subset of orders, perspectives, or variants carries the dimension activation record naming the active set and condition basis	E	Juno
D37	§01 §14	Governing-conflict gap registered and distinct from specification-gap — a conflict between two individually-adequate artifacts at the same aspect is registered as a governing-conflict gap with extended fields; recording it only as a specification-gap is non-conforming	E	Juno
D38	§01 §14	Conflict-gap annotation required and propagated — every verdict produced while a governing-conflict gap was Open or In-resolution carries a conflict-gap annotation; a missing annotation, or a gate treating an annotated verdict as unconditionally authoritative for the conflict aspect, is non-conforming	Y/E	Juno
D39	§01 §14	Admissibility relation registered as a first-class artifact (load-bearing) — a registered, versioned, content-addressable admissibility relation artifact declares ADMIT/REJECT per order-index combination with stated basis; enforcement by an undeclared rule is non-conforming regardless of verdict agreement	Y	Juno
D40	§01 §14	ADMIT/REJECT judgment reproduced from registered admissibility relation (load-bearing) — an independent inspector re-derives the determination for any two proposed DSL terms from the registered relation alone; exercised on at least one ADMIT and one REJECT case per registered order-index combination	Y	Juno
D41	§01 §14	Typed rejection diagnosis emitted as a registered output — a rejected composition produces a typed diagnosis carrying composition identity, per-constituent order-index/perspective/variant, the violated relation entry identity, and the REJECT basis; declining to compose without a conforming diagnosis is non-conforming	Y	Juno
D42	§01 §14	Higher-order order registration extends admissibility relation — registering a higher-order order produces an observable scope-extending amendment to the relation carried by a delta-attestation object; affected compositions are REJECT before and ADMIT after; admission without a recorded extension is non-conforming	Y/E	Juno
D43	§01 §14	Order-typed soundness inheritance observable on composed artifact (load-bearing) — a composed artifact carries per-obligation order-typed soundness anchors traceable to constituent anchors under the admissibility relation; a combined soundness assertion without traceable anchors is non-conforming	E	Juno
D44	§01 §14	Construction-time conflict registered and blocking — a content contradiction surfaced during construction between a KB/data-source contribution and a model contribution, or introduced by an operator edit, at the same aspect/order/perspective, is registered as a construction-conflict gap under the canonical gap machine (distinct from elicitation ambiguity and from operation-time governing-conflict), resolved by the §12.5 taxonomy; an unresolved construction-conflict blocks boundary-closure attestation for the affected aspect exactly as an unresolved variant conflict does; a model attested closed over an aspect with an Open construction-conflict is non-conforming	Y/E	Juno
P8-1	§01 §14	Boundary-closure completeness falsifiable per dimension — an independent inspector can determine whether the formal specification covers each identified source element per order, per perspective, and per variant	Y	Juno
P8-2	§01 §14	Anchor compatibility — where the generation pipeline outputs an anchor-compatible signed record, the record is structurally compatible with Field 5 of the non-language-provenance anchor	Y	Juno
P8-3	§01 §14	Delta-cascade inheritance — coverage-narrowing amendments trigger at minimum a scope-restricting delta; no coverage-narrowing amendment can be silently applied without downstream anchors becoming stale	Y	Juno

§02a Jupiter — Base Analysis

Analysis methods

Property	Section	Description	Inspector-verifiable	Required for
SA1	§02a §8	Order-typed analysis/lift artifact — produced formulae, symbols, and findings are tagged by order, not as a flat concept enumeration	Y	Jupiter
SA2	§02a §8	Audit-binding recomputation witness — independent inspector re-derives lifted form and verdict from source under the governing specification	E	Jupiter
SA3	§02a §8	Multi-source provenance — result cites one or more domain models × knowledge bases × data sources × specifications	E	Jupiter
SA4	§02a §8	Cross-method corroboration signal — deterministic↔probabilistic divergence recorded as a measure contributing to the verdict; present when both families are deployed	E	Jupiter
SA5	§02a §8	Composable-battery / single-method invariance — analysis-artifact structure is invariant whether deterministic-only, probabilistic-only, or mixed	Y	Jupiter
SA6	§02a §8	Gap and reinforcement — typed gaps by locus and reinforcement routing emitted in lieu of unsupported verdicts	Y	Jupiter
SA7	§02a §8	Perspective ablation — same artifact and governing specification analyzed under different perspectives produce observably different analyses and verdicts	Y	Jupiter
SA8	§02a §8	Order-decomposition invariance — analysis, lift, and verdict structure follow the orders of whatever order-decomposed model is provided	Y	Jupiter
SA9	§02a §8	Reverse-composition — presenting no governing specification yields a composed specification from available artifacts, bound to and recomputable from those artifacts	Y/E	Jupiter
SA10	§02a §8	Pre-invocation signal admission gated on registration — a signal from an unregistered source is observably not admitted as a battery input	Y	Jupiter
SA11	§02a §8	Pre-invocation signal order-typing enforced — a signal from a source declaring specific orders enters the IR as a fully order-typed element; a signal from an order-agnostic source enters as untyped-pending	Y	Jupiter
SA12	§02a §8	Witness chain spans pre-invocation links — the multi-stage witness chain carries pre-invocation signal links prepended before the raw-input link; each carries its witness class annotation; W1 links are independently re-derivable	E	Jupiter
SA13	§02a §8	Cross-phase corroboration present when conditions met — where a deterministic pre-invocation signal and a probabilistic battery method evaluated the same conformance question, a `pre-invocation-cross-phase` entry is present in the analysis battery record	E	Jupiter
SA14	§02a §8	Signal-required gap referral issued on absence — where a `signal-required` source produces no signal, a typed gap referral at the pre-invocation signal locus is present; no `conforming` verdict is issued while the gap is open	Y	Jupiter
SA15	§02a §8	Signal-absent posture declared in scope — where any registered source is absent, Field 5 reflects the corresponding pre-invocation coverage exclusion	E	Jupiter
SA16	§02a §8	W1/non-W1 distinction observable — a downstream consumer can determine from the witness chain which pre-invocation links are W1 and which are W2 or W3; the distinction is carried as an observable witness-class annotation on each link	Y	Jupiter

Discrete representations

Property	Section	Description	Inspector-verifiable	Required for
R1	§02a §8	Order-typed representation — representation tagged by order, not flat concept enumeration	Y	Jupiter
R2	§02a §8	Genus invariance — output structure invariant across representation kind	Y	Jupiter
R3	§02a §8	Multi-source formation including data-source-alone — formed from {model, spec, KB, data source} in any combination including data source alone	Y	Jupiter
R4	§02a §8	Audit-binding recomputation witness (formation and use) — independently re-derivable from source under orders; traversal and use also verifiable	E	Jupiter
R5	§02a §8	Composed order-structured program — executable composed discrete program observably composing orders	Y	Jupiter
R6	§02a §8	Reuse without limitation / infrastructure-agnosticism — single output consumed by two or more distinct consumers without re-derivation; not predicated on any deployment-trust infrastructure	Y	Jupiter
R7	§02a §8	Order-attributed emergent output — emergent higher-order output order-typed and re-derivable from source under the orders	Y/E	Jupiter
R8	§02a §8	Cross-model composition by order — composition of same-order representations admitted by order’s common structure; cross-model higher-order order yields witness-bound emergent output	Y/E	Jupiter
R9	§02a §8	Subject-directed determination identifying the responsible order — finding is order-typed, audit-bound, re-derivable, and identifies the responsible order	Y/E	Jupiter
R10	§02a §8	Reflexive artifacts re-derivable; self-modification order-bounded — triage decision or cache hit re-derives under the orders; ill-typed self-modification is rejected	Y	Jupiter

Conformance certificate

Property	Section	Description	Inspector-verifiable	Required for
SC1	§02b §8	Differential admission/refusal at downstream gate — gate admits when certificate passes all checks; refuses when any check fails	Y	Jupiter
SC2	§02b §8	Recomputation-witness verification — re-derived verdict matches Field 4 verdict	E	Jupiter
SC3	§02b §8	Cryptographic-signature verification — the tamper-evident binding (Field 9) verifies over all invariant fields; a binding covering only a subset fails	Y	Jupiter
SC4	§02b §8	Falsifier-cascade observation — upon falsifier-condition occurrence, revocation cascades to downstream consumers within declared retention window	Y	Jupiter
SC5	§02b §8	Symmetric target-class enumeration — same certificate format applies to all three target classes	Y	Jupiter
SC6	§02b §8	Triad path declaration — Field 3 carries path identifier from typed enumeration with matching evidence reference	E	Jupiter
SC7	§02b §8	Interaction-protocol substitution — where target is interaction-mediated, verified target is the interaction protocol; certification path is interaction-protocol conformance testing	Y	Jupiter
SC8	§02b §8	Refusal of self-attestation — where deployment policy declares verifier independence, certificates with coincident verifier and target identities are refused with structural diagnostic	Y	Jupiter
SC9	§02b §8	Modality-agnostic conformance verification — same certificate structure and triad apply across non-linguistic modalities	Y	Jupiter
SC10	§02b §8	Target-of-analysis symmetry — interpretation verified by same mechanism as program	Y	Jupiter
SC11	§02b §8	Provenance-agnostic linguistic-artifact conformance — same process irrespective of producer	Y	Jupiter

Intermediate representations and multi-stage pipelines

Property	Section	Description	Inspector-verifiable	Required for
IR1	§02a §8	Order-shape contract enforced at each IR stage — each IR stage carries order-type assignments per element; the contract is satisfied stage-locally, not deferred to the final form	E	Jupiter
IR2	§02a §8	Partial type states observable — an IR element in provisional or untyped-pending state carries an observable type-state tag; not silently promoted to fully-typed	Y	Jupiter
IR3	§02a §8	Multi-stage witness chain present and chainable — each stage contributes an observable witness link; the chain from raw input through each IR to the final form is independently traversable	E	Jupiter
IR4	§02a §8	Convergence criterion declared and applied — the convergence criterion is present in the deployment registration and in Field 5; resolved elements carry convergence records	Y/E	Jupiter
IR5	§02a §8	Declared-irreducible entries present where applicable — elements that cannot be fully resolved carry declared-irreducible entries with irreducibility basis and scope impact; not silently omitted or promoted	E	Jupiter
IR6	§02a §8	Bounded-analysis record issued when no grounded verdict is possible — where the full analysis question is irreducible, a bounded-analysis record is issued rather than a certificate	Y	Jupiter
IR7	§02a §8	Symbolic execution precondition enforced — symbolic execution does not proceed over provisionally-typed or untyped-pending IR elements	Y	Jupiter
IR8	§02a §8	Path-exploration strategy declared and coverage recorded — the deployed strategy and parameters are present in Field 5; the coverage record identifies explored, bounded, and unexplored paths	E	Jupiter
IR9	§02a §8	Battery method layer classification observable — each method in the deployed battery is identifiably assigned to its layer (pre-IR, IR-level, or post-IR) in the analysis battery record	E	Jupiter

Additional structural properties

Property	Section	Description	Inspector-verifiable	Required for
G1	§02b §8	Pipeline-composed target requires topology record and stage witness chain — Field 1 carries a pipeline-topology record and Field 7 carries a stage-level witness chain through the aggregation step	E	Jupiter
G2	§02a §8	Interaction-protocol lift to order-typed form present in witness chain — the witness chain carries a protocol-specification lift link and a trace-record lift link before the analysis-act links	E	Jupiter
G3	§02a §8	Divergence signal aggregation function declared and recomputable — the analysis battery record carries the aggregation function identity and parameters; an independent inspector applying the declared function reproduces the composite contribution	E	Jupiter
G4	§02b §8	Bootstrap provenance failure consequences declared — where a bootstrap provenance component is absent or unverifiable, the certificate carries a conditionally-conforming or non-conforming verdict with a falsifier annotation	Y/E	Jupiter
G5	§02b §8	Registry conflict resolved or declared — where two certificates share the same target, governing specification, certification path, and overlapping validity windows, both carry a cross-certificate conflict flag	Y	Jupiter
G6	§02b §8	Composite-of-composites carries chain references, not inlined chains — the parent’s composition provenance record carries a content hash reference to the constituent’s chain	E	Jupiter
G7	§02a §8	Field 3 evidence references resolve to analysis battery record entries — each evidence reference in Field 3 resolves to a specific method entry with a matching content hash	E	Jupiter
G8	§02a §8	Source registration records in registry with versioning and tamper-evidence — the specification registry carries pre-invocation signal source registration records; each certificate’s analysis battery record carries the source registration version in effect at analysis time	E	Jupiter
G9	§02b §8	Bounded-analysis record required fields present and registered — a bounded-analysis record carries the full required field set (§02b §3); it is registered in the specification registry; downstream gates treat it as a non-passing result	Y/E	Jupiter
G10	§02b §8	Superseded reverse-composed specification version handled per delta-attestation — where a reverse-composed specification undergoes a scope-breaking update, prior certificates are observably revoked	Y	Jupiter
G11	§02b §8	Admissibility relation registered and ADMIT/REJECT reproduced from it — the governing domain model’s admissibility relation is present as a registered artifact; an independent inspector re-derives the ADMIT or REJECT determination for any proposed composition from the registered relation alone; a bundle whose anchor trail cannot be traced through a registered admissibility relation is structurally deficient	E	Jupiter

Battery execution and verdict discipline

Property	Section	Description	Inspector-verifiable	Required for
B1	§02a §8	Mechanical tri-state status (load-bearing) — verdict status CERTIFY/REFUSE/REFER is determined solely from (passed, has-falsifier) tuples across the declared pass set; invariant to execution order; identical inputs reproduce identical status	Y	Jupiter
B2	§02a §8	Per-pass audit with execution provenance — the audit chain records execution stratum, cache-hit, substrate version, typed falsifier, battery-method identity, and orders-acted-upon per pass; append-only, hash-chained, tamper-evident	E	Jupiter
B3	§02a §8	Pass soundness-anchor independence from model-internal signals — no declared pass carries a model-internal signal as its soundness anchor; a pass not reproducible from its declared anchor without internal access is non-conforming	Y/E	Jupiter
B4	§02a §8	Re-entrance cycle detection — invoking the same (analysis-spec-identity, pass-name) pair twice in one session produces REFUSE with a cycle descriptor	Y	Jupiter
B5	§02a §8	Pre-emission gating — a provenance gap or authority conflict produces pipeline termination and a REFER record; no subsequent pass executes after termination	Y	Jupiter
B6	§02a §8	Open declared pass set — additional passes may be declared and registered with soundness anchors and ordering constraints; the composition discipline applies identically; no pass removal without re-registration	Y	Jupiter
B7	§02a §8	Procedural-confidence recomputability — an independent inspector re-derives the procedural-confidence value from the PassRecord set using declared weights and normalization; the re-derived value matches the issued value	E	Jupiter
B8	§02a §8	Audit chain tamper evidence — modifying any prior pass record produces an observable chain hash mismatch at the next link	Y	Jupiter
B9	§02a §8	Anchor-inheritance records present in CertifiedBundle (load-bearing) — each bundle carries per-obligation soundness anchor-inheritance records tied to the order-structure; the anchor trail distinguishes a composed verdict from an aggregation without soundness lineage	E	Jupiter
B10	§02a §8	CertifiedBundle co-required fields complete — all five co-required fields present (typed predicates, scope certificate, composed discrete program where produced, verdict with anchor-inheritance records, audit chain pointer); absence of any field is refusable at gate	Y	Jupiter
B11	§02a §8	Falsifier absoluteness under DDIL state — a non-null falsifier produces REFUSE under any execution stratum and any DDIL state; no configuration produces REFER in place of REFUSE when a falsifier is present	Y	Jupiter
B12	§02a §8	Stale substrate cache rejection — a cache lookup serving a PassRecord produced under a mismatched substrate-version tuple is refused and triggers re-execution	Y	Jupiter

Traversability

Property	Section	Description	Inspector-verifiable	Required for
V1	§02a §8	Traversal witness present and chainable (load-bearing) — each traversal act produces a witness link carrying all minimum required fields; an independent inspector re-derives the full traversal path from the witness without deployment access	E	Jupiter
V2	§02a §8	Governing structural invariant satisfied (load-bearing) — every traversal act satisfies all five conditions of the governing structural invariant regardless of mathematical form or pipeline layer; satisfaction by a different mathematical route is governed; non-satisfaction is non-conforming regardless of output resemblance	Y/E	Jupiter
V3	§02a §8	Transformation sequence declared and recomputable — each controlled transformation carries class identity, declared parameters, and pre/post embedding content hashes; re-application reproduces the result within declared tolerance	E	Jupiter
V4	§02a §8	Analysis act outputs order-typed and aspect-keyed (load-bearing) — every traversal-driven analysis act declares its aspects, orders, and perspectives, and binds to the traversal witness that supplied the content	E	Jupiter
V5	§02a §8	Traversal-surfaced content aspect-indexed — surfaced KB entries, data source fields, and query library entries carry the domain aspect identifier; content without the binding is not admitted as traversal-surfaced	E	Jupiter
V6	§02a §8	Steering-conflict recorded, not silently resolved — conflicting steering inputs produce a steering-conflict entry in the traversal witness carried through the chain	E	Jupiter
V7	§02a §8	Higher-order analysis gap emitted on undeclared relationship — proximate aspects with an absent cross-order or cross-perspective relationship record produce a typed gap referral with locus higher-order-analysis; no conforming verdict without it	Y	Jupiter
V8	§02a §8	Cross-artifact consistency gap emitted on governing artifact conflict — inconsistent governing-artifact assertions at the same aspect produce a typed gap referral with locus cross-artifact-consistency, distinct from the KB↔data-source divergence signal	Y	Jupiter
V9	§02a §8	Formal specification battery invocation observably distinct — a specification-targeted battery invocation is distinct from a target-analysis invocation; its verdict identifies the specification itself as the target	E	Jupiter
V10	§02a §8	Traversal witness in chain at correct position — traversal links sit after IR stage links and before analysis act links, carrying domain model and governing specification versions; a version mismatch against the registry is non-conforming	E	Jupiter
V11	§02a §8	Precomputed traversal artifacts governed identically — a precomputed traversal artifact carries a conforming traversal witness; serving a precomputed result without one is not a governed traversal act	Y/E	Jupiter

Bootstrap and composed chain

Property	Section	Description	Inspector-verifiable	Required for
T1	§02a §8	Bootstrap binary-falsifiability (load-bearing) — a candidate specification below the registered agreement threshold, or failing SMT ground-discharge, produces a typed rejection and no emitted specification; no partial emission or override path	Y	Jupiter
T2	§02a §8	Emitted specification bundle co-presence (load-bearing) — every registered governing specification carries all four bundle components; a bundle missing any component is refused at registration with a typed rejection identifying the absent component	Y	Jupiter
T3	§02a §8	Composed chain scope monotone narrowing — a composed scope is verifiably a subset of each constituent sub-scope; a composition widening any constituent scope fails the typed-interface alignment check	Y/E	Jupiter
T4	§02a §8	Composed chain rule-trace concatenation — the composed rule trace carries identifiable per-specification trace segments in order; each fired predicate is attributable to its constituent specification	E	Jupiter
T5	§02a §8	Single-specification deployment scope — a deployment operating only the analysis specification cannot claim composed-chain scope, rule-trace, or faithfulness-anchor-lineage properties; they are observably absent from its certificates	Y	Jupiter
T6	§02a §8	Bootstrap rejection record present on failure — a failed bootstrap attempt produces a registered, tamper-evident typed rejection record carrying stage, candidate identity, measured value, threshold, and timestamp	E	Jupiter

Federated authority reconcile

Property	Section	Description	Inspector-verifiable	Required for
F1	§02a §8	PeerFinding messages registered in audit chain (load-bearing) — every received PeerFinding is recorded with message id, source agent id, artifact content hash, and verdict status	E	Jupiter
F2	§02a §8	No-unverified-propagation invariant enforced (load-bearing) — a local re-verification PassRecord precedes any inter-agent consensus record for every peer-supplied finding; CERTIFY based on a peer CERTIFY without local re-verification is a conformance defect	Y/E	Jupiter
F3	§02a §8	Divergence detection triggers AR-gate without exception — an agent holding a verdict distinct from a peer’s for the same artifact and content hash does not emit CERTIFY; the AR-gate is triggered	Y	Jupiter
F4	§02a §8	ReconciliationEvent emitted with stable divergence id — every AR-gate trigger produces a ReconciliationEvent with a stable divergence id enabling reconstruction of the full divergence history across all participating agents’ audit chains	E	Jupiter
F5	§02a §8	CERTIFY suppressed while gap Open or In-resolution — no CertifiedBundle for the affected artifact is present in the registry while the governing-conflict gap is Open or In-resolution; observable by registry and gap-record query	Y	Jupiter
F6	§02a §8	Resolution outcome typed and registered — the divergence resolution outcome is one of the four enumerated types, appended to the gap record and each participating agent’s audit chain	E	Jupiter
F7	§02a §8	ratify_amend triggers delta-attestation and soundness-declaration re-discharge — a ratify_amend outcome enters the delta-attestation lifecycle; scope-breaking amendments revoke prior bundles; the soundness-declaration hash is recomputed and no prior-hash bundle is admitted as current	Y/E	Jupiter
F8	§02a §8	Partition-recovery bounds declared and observed — declared handshake and consistency-recovery bounds; measured durations recorded; a partition-era CERTIFY is annotated provisional and not admitted as stable until re-discharged post-recovery	E	Jupiter
F9	§02a §8	Capability advertisement verified by adversarial-peer test — a deployment advertising AUTHORITY_RECONCILE passes all AR-gate requirement tests under adversarial-peer simulation; partial implementation advertising full capability is non-conforming	Y	Jupiter

Calibration attestation gate

Property	Section	Description	Inspector-verifiable	Required for
CA1	§02a §5a.6	Gate runs at deployment registration — every deployment registration includes a calibration record in the specification registry; a deployment with no calibration record is refused at registration with a typed diagnostic	Y	Jupiter
CA2	§02a §5a.6	Benchmark is a certified registered artifact — the benchmark artifact version referenced by the calibration record is present in the specification registry with a valid attestation record	Y	Jupiter
CA3	§02a §5a.6	Miscalibration narrows Field 5 — a certificate issued under a manifest with a miscalibrated class carries a typed scope restriction in Field 5 referencing the calibration record identity; an inspector reproduces the scope restriction by retrieving the calibration record	E	Jupiter
CA4	§02a §5a.6	Miscalibration falsifier present in Field 6 — a certificate with a miscalibrated-class finding carries a falsifier annotation in Field 6 with a declared re-calibration window; the falsifier fires if the window expires without a resolved calibration record	Y	Jupiter
CA5	§02a §5a.6	Gate not suppressible — submitting a deployment configuration that disables calibration gate runs, or a manifest sub-record declaring calibration suppression, is refused at deployment registration with a typed structural diagnostic	Y	Jupiter
CA6	§02a §5a.6	Autonomous re-run on amendment — a scope-breaking amendment to the deployment manifest that changes a declared function produces an automatic calibration gate re-run registered before the amended manifest version takes effect	Y	Jupiter
CA7	§02a §5a.6	Benchmark version binding enforced — a calibration record produced under a benchmark version whose version bindings have been superseded produces a stale-benchmark finding; the certificate carries a stale-benchmark falsifier annotation in Field 6	Y	Jupiter
CA8	§02a §5a.6	Calibration response mode declared — the deployment manifest runtime configuration record carries a calibration response mode declaration; an inspector confirms the certificate issuance behavior matches the declared mode	E	Jupiter

§02b Jupiter — Delta-Attestation, Deployment Manifest, ON_CHAIN_ANCHOR

Property	Section	Description	Inspector-verifiable	Required for
DA1	§02b §8	Refusal-to-register on absent delta-attestation — submitting an amended artifact version without a corresponding delta-attestation object is refused at registration	Y	Jupiter
DA2	§02b §8	Recomputable delta-classification — the delta-classification field value is reproduced by applying the declared classification function to the structural-difference record; no inspector access to system internals required	Y	Jupiter
DA3	§02b §8	Recomputable attestation hash — the attestation hash is reproduced from the recorded authority signatures over Fields (a)–(d)	Y	Jupiter
DA4	§02b §8	Class-specific differential cascade behavior — amendments of each of the four classification values produce observably distinct cascade behaviors	Y	Jupiter
DA5	§02b §8	Typed cascade record propagation — upon a scope-restricting or scope-breaking amendment, typed cascade records naming each affected downstream artifact are present in the audit trail within the declared retention window	Y/E	Jupiter
DA6	§02b §8	EUF-CMA-secure signatures — the cryptographic signature on the delta-attestation object verifies under the declared scheme; tampered field content produces a failing verification	Y	Jupiter
DA7	§02b §8	Cross-portfolio cascade execution — a scope-breaking amendment to a registered artifact produces observable invalidation of downstream non-language-provenance anchors, conformance certificates, actuation anchors, and scope-of-applicability certificates within the declared retention window	Y	Jupiter
DA8	§02b §8	Refusal of monotonic-non-cascade configuration — submitting a deployment configuration declaring that amendments to registered artifacts never require downstream re-discharge is refused at deployment registration	Y	Jupiter

Deployment manifest

Property	Section	Description	Inspector-verifiable	Required for
DR1	§02b §6	Manifest present and conforming at registration — every registered deployment carries a manifest record; a deployment without a manifest is refused at registration with a typed diagnostic	Y	Jupiter
DR2	§02b §6	Selector procedure reproducibility — for any selection event log entry, an inspector re-running the selector procedure against the recorded (operation context, state snapshot) pair reproduces the selected artifact identity	Y	Jupiter
DR3	§02b §6	State surface completeness — for a state-dependent selector, every input the procedure reads at selection time is covered by the state surface declaration and present in the state snapshot; a procedure reading undeclared state is observably non-conforming	E	Jupiter
DR4	§02b §6	Governing selector constraint enforcement — a governing selector that resolves to a revoked or unregistered governing collection version produces a gate refusal with typed diagnostic; no certificate is issued under an unregistered governing artifact	Y	Jupiter
DR5	§02b §6	Battery configuration consistency — the battery configuration declared in the battery selector’s selection event log entry matches the analysis battery record carried in the certificate’s Field 7 recomputation witness	E	Jupiter
DR6	§02b §6	Runtime configuration gate enforcement — an operation under DDIL conditions produces the behavior declared in the runtime configuration record; no deployment may produce behavior inconsistent with its declared runtime configuration	Y	Jupiter
DR7	§02b §6	Manifest amendment cascade — a scope-breaking amendment to any manifest component produces immediate cascade invalidation of all certificates issued under the prior manifest version; cascade records are present in the audit trail within the declared retention window	Y	Jupiter
DR8	§02b §6	Retention window enforcement — selection event log entries for any operation covered by a non-revoked certificate, or within 7 years post-revocation, are retrievable by an inspector	E	Jupiter
DR9	§02b §6	Downward retention override refused — a manifest declaring a retention window override below the mandatory minimum is refused at deployment registration with a typed diagnostic	Y	Jupiter
DR10	§02b §6	Monotonic-non-cascade configuration refused — a manifest or manifest sub-record declaring monotonic non-cascade is refused at deployment registration with a typed structural diagnostic	Y	Jupiter

ON_CHAIN_ANCHOR (verification-gated ledger commitment)

Property	Section	Description	Inspector-verifiable	Required for
L1	§02b §8	Verify-then-commit inversion — no state transition hash reaches the target ledger without a prior CERTIFY verdict from the procedural-verification gate; a REFER or REFUSE verdict produces no ledger write; a CERTIFY verdict produces exactly one ledger write of the audit-record chain hash	Y	Jupiter
L2	§02b §8	Only the hash lands on-chain — the on-chain entry is exactly the chain hash of the audit record; state transition content, audit-record content, specification content, and predicate content are absent from the ledger entry and not reconstructible from it	Y	Jupiter
L3	§02b §8	Bidirectional linkage present after commitment — the audit record’s `chaincode_commitment.txid` is populated after a successful ledger write; traversal works from audit record to ledger entry and back; a CERTIFY record with a null `txid` is structurally incomplete	Y/E	Jupiter
L4	§02b §8	Hash verification by independent party — a party other than the deployment operator recomputes the audit-record hash and confirms it matches the on-chain value; a mismatch is observable without deployment access	Y	Jupiter
L5	§02b §8	Structural orthogonality of internal and external tamper evidence — internal hash-chain tamper-evidence and on-chain external attestation are both maintained and independently distinguishable; removing either while retaining the other is observably non-conforming	Y/E	Jupiter
L6	§02b §8	DDIL edge-queue causal ordering preserved — queued commitments are submitted to the ledger in the causal order of verdict issuance; the on-chain sequence matches the audit-chain sequence	Y/E	Jupiter
L7	§02b §8	CERTIFY verdict immutability under DDIL — a CERTIFY verdict issued under DDIL conditions is not downgraded to REFER or withheld pending reconnection; only the external attestation is deferred, within the reconnection window	Y/E	Jupiter

Model moderation

Property	Section	Description	Inspector-verifiable	Required for
BC1	§02b §5.5	Behavioral-condition gate genus invariance — a runtime or post-hoc gate for any registered behavioral-condition representation carries the identical structure (bracket declaration, order-type, representation kind, content hash, dual-locus invariance, delta-attestation lifecycle); a behavioral gate implementing this structure under a different condition name is observably this architecture, not a distinct one	Y/E	Jupiter
MD1	§02b §5.5	Behavioral modification detection for externally-hosted models — an externally-hosted model’s registration declares a drift-equivalence threshold; a drift finding at or above the threshold produces immediate new-model treatment identical to a detected hash change with no modification record; registration without the declared threshold is refused	Y	Jupiter

§02c Jupiter — Integrated Boundary (inbound boundary, composition gate)

Property	Section	Description	Inspector-verifiable	Required for
IB1	§02c §11	Admit/refuse differential by anchor presence — predicate with and without anchor produces distinct outcomes	Y	Jupiter
IB2	§02c §11	Admit/refuse differential by signature validity — predicate with tampered anchor signature is refused	Y	Jupiter
IB3	§02c §11	Admit/refuse differential by registered identity — predicate with unregistered program_id, spec_id, or interp-gen-spec_id is refused on each	Y	Jupiter
IB4	§02c §11	Causal-closure recomputation — predicate with modified engineering-result content hash is refused	Y	Jupiter
IB5	§02c §11	Co-signature requirement on interaction-mediated steps — interaction-mediated execution record without co-signature produces causal-closure failure	Y	Jupiter
IB6	§02c §11	R1 — no cross-store arithmetic — attempt cross-store score comparison without registered calibration mapping produces module-construction refusal	Y	Jupiter
IB7	§02c §11	Mechanical tri-state of composition gate — pass sets with known (passed, has_falsifier) distributions produce CERTIFY/REFUSE/REFER deterministically	Y	Jupiter
IB8	§02c §11	Pipeline termination on AR-gate / PV-gate — authority conflict or missing faithfulness attestation produces no subsequent pass execution and a single REFER record	Y	Jupiter
IB9	§02c §11	Audit chain tamper evidence — modification of a prior pass record produces a chain hash mismatch	Y	Jupiter
IB10	§02c §11	Re-entrance detection at the inbound boundary — composition invoking same (analysis-spec-identity, pass-name) twice in one session produces REFUSE with cycle descriptor; inbound-boundary observation of the re-entrance discipline (§02a §3a.4), cf. B4	Y	Jupiter
IB11	§02c §11	Substrate version guard — cached result with mismatched substrate_version_tuple is rejected	Y	Jupiter
IB12	§02c §11	Battery-method-identity linkage — PassRecord battery_method_identity traces to a §02a battery method entry in the multi-stage witness chain	E	Jupiter
IB13	§02c §11	Procedural-confidence recomputability — procedural-confidence value is re-derived from PassRecord set using declared weights and normalization; observed match with issued value	E	Jupiter
IB14	§02c §11	R2 — no implicit equivalence — inter-domain predicate composition outside registry produces refuse and knowledge-gap referral	Y	Jupiter
IB15	§02c §11	Falsifier-cascade on spec amendment — scope-breaking specification amendment produces scope-of-applicability certificate invalidation within retention window	Y	Jupiter
IB16	§02c §11	Any-link withdrawal invalidation — withdrawal of one interface link produces immediate invalidation of all composed certificates traversing that link	Y	Jupiter
IB17	§02c §11	Atomicity of partial re-discharge — re-discharge of a proper subset of composition hops produces COMPOSITION-PATH-INVALID refusal	Y	Jupiter
IB18	§02c §11	Scope monotone narrowing — composed scope ⊆ scope of each individual interface along the composition path	E	Jupiter
IB19	§02c §11	Outbound-boundary declaration — governing specification carries an output-class routing declaration; actuation anchor is deployed for all output classes routed to non-linguistic effects	E	Jupiter
IB20	§02c §4.3	Persistent-state writes declared and actuation-gated — a certified output routed to persistent state whose content can influence a subsequent governed invocation is an emitted effect under the actuation anchor and gate; a routing declaration omitting such a class is incomplete and the write is an ungoverned effect	Y	Jupiter

§02c Jupiter — Actuation (outbound boundary)

Property	Section	Description	Inspector-verifiable	Required for
J1	§02c §11	Structural-invariant refusals — each of the nine refusal conditions (§02c §4.3) is independently exercisable; each produces a distinguishable typed refusal reason	Y	Jupiter
J2	§02c §11	Non-trivial transformation — null-transformation causal-binding witness for non-pass-through actuation class produces gate-check failure under condition 6	Y	Jupiter
J3	§02c §11	Procedural-confidence floor — CertifiedBundle with PassRecord inputs deriving below-floor value produces refuse under condition 7	Y	Jupiter
J4	§02c §11	Model-internal confidence rejection — deployment configuration naming a softmax or log-likelihood signal as gating input is rejected at load time	Y	Jupiter
J5	§02c §11	Causal-binding re-derivation — anchor with modified originating predicate content hash produces condition 6 failure	Y	Jupiter
J6	§02c §11	R3 — authority action required — certified output routed to a consequence-bearing operation without recorded authority action produces downstream-consumer guard refusal	Y	Jupiter
J7	§02c §11	R4 — no model confidence gating — configuration naming model-internal confidence class is rejected at load with configuration-rejection diagnostic	Y	Jupiter
J8	§02c §11	R5 — scope match required — consumer bridging program input range outside certified scope produces re-analysis trigger, not admission	Y	Jupiter
J9	§02c §11	R5 — divergence-rate metric recomputability — divergence-rate metric re-derived from audit trail matches published metric without internal inspection	E	Jupiter
J10	§02c §11	R3 over R5 priority — input triggering both R3 and R5 simultaneously produces R3 refusal record; R5 not consulted	Y	Jupiter
J11	§02c §11	R3 over R4 priority — input triggering both R3 and R4 simultaneously produces R3 refusal record; R4 not consulted	Y	Jupiter
J12	§02c §11	R4 over R5 priority — input triggering both R4 and R5 simultaneously produces R4 refusal record; R5 not consulted	Y	Jupiter
J13	§02c §11	Named-authority standing coverage check — co-signature from authority whose declaration does not cover the actuation class produces gate-check failure under condition 8	Y	Jupiter
J14	§02c §11	Named-authority standing lifecycle — scope-restricting — amendment narrowing authorized-actuation-classes produces scope-restricting cascade on in-flight actuation anchors referencing that authority	Y	Jupiter
J15	§02c §11	Named-authority standing lifecycle — revocation — revocation of standing declaration produces immediate invalidation of in-flight actuation anchors referencing the revoked authority	Y	Jupiter
J16	§02c §11	Concurrent non-weakening — deployment registry carries all five refusals; priority-order enforcement is observable by constructing inputs triggering pairs of refusals at different priority levels	Y	Jupiter
AC1	§02c §4.4	Accumulation record present and order-structured — each admitted effect in an accumulation-governed class appends an order-typed, witness-bound entry (class, order tags, effect hash, target, timestamp, anchor reference) to the declared scope’s hash-chained accumulation record	E	Jupiter
AC2	§02c §4.4	Joint-inadmissibility refusal at the accumulating effect — a sequence of individually-admissible effects that is jointly out-of-bounds under a declared accumulation predicate is refused at the accumulating effect with typed refusal accumulation-bound-exceeded identifying the violated predicate and contributing entries	Y	Jupiter
AC3	§02c §4.4	Declared accumulation scope enforced — accumulation scopes and windows are registered parameters of the runtime configuration record; an actuation class with declared accumulation predicates operating without the accumulation gate is non-conforming	Y/E	Jupiter
AC4	§02c §4.4	Decomposition foreclosure — a macro-effect decomposed into individually-admissible micro-effects is refused at the bound regardless of per-effect admissibility; per-effect-only gating does not practice accumulation governance	Y	Jupiter

§02c Jupiter — Non-Language Bridge

Non-language bridge enforcement constraints

Property	Section	Description	Inspector-verifiable	Required for
NB1	§02c §2.3	No cross-store score comparison — cross-store retrieval score comparison without a registered calibration mapping is refused; cross-store traversal position comparison is refused without a registered mapping covering the embedder pair	Y	Jupiter
NB2	§02c §3	No implicit cross-domain ontology equivalence — cross-domain predicate composition proceeds only through registered cross-domain typed interfaces; string match, vocabulary overlap, or operator assertion does not satisfy the requirement	Y	Jupiter
NB3	§02c §6	No origination of decisions reserved for named human authority — no deployment configuration may route certified output to a consequence-bearing co-signature-required operation without a recorded authority action	Y	Jupiter
NB4	§02c §6	No model-internal confidence as gating signal — no configuration may name a model-internal confidence class as a gating signal; gating rests on procedural-confidence derived from PassRecord set under a registered derivation-binding witness	Y	Jupiter
NB5	§02c §6	No silent scope extrapolation — a certified predicate may not be re-used at a downstream consumer bridging program whose input range falls outside the predicate’s scope-of-applicability certificate; re-analysis is triggered on scope exit	Y	Jupiter

§02d Jupiter — Discrete Composition

Base properties R5, R7, R8, R9, R10 are enumerated under §02a (Discrete representations); this section carries the §02d-specific extensions.

Property	Section	Description	Inspector-verifiable	Required for
R5a	§02d §6	Composition witness present and chainable — carries constituent representation identities, per-constituent formation witness, composition locus records, composed-program content hash, emergent-output attribution records, and use-verification records; chains from constituent IR witness links through the composition step	E	Jupiter
R5a2	§02d §6	Use-verification records present — a traversal or evaluation over a composed program yields a use-verification record from which the path taken through the order-governed structure is independently re-derivable; absence is a structural incompleteness	Y/E	Jupiter
R5b	§02d §6	Reuse without limitation — a single composed discrete program is consumed by two or more distinct consumers without re-derivation; consumer verification proceeds against the composition witness without trust in the composing deployment	Y	Jupiter
R5c	§02d §6	Override-layer conflicts recorded in Field 6 — a specification-override conflict with a governing-specification conformance predicate produces a falsifier annotation with condition subtype `override-conflict`; no suppression without recording is admitted	E	Jupiter
R5d	§02d §6	Data-source-alone formation — formation from a data source alone proceeds by semantic analysis and data sampling; the resulting representation is order-typed and carries a recomputation witness traceable to the source’s schema, keys, constraints, or sampled content	Y/E	Jupiter
R5e	§02d §6	Formation-method independence — the witness kind follows the formation method (justification record for interpretive or non-deterministic methods, replay record for deterministic); the order-governed, witness-bound result is produced regardless of formation method	E	Jupiter
R5f	§02d §6	Probabilistic and hybrid modes governed — a probabilistic composition carries a recomputation witness from which the posterior or output is re-derivable under the declared update procedure; probabilistic mode is not a separate architecture	E	Jupiter
R5-map	§02d §6	Traversal witness present per step — each model-as-map traversal step carries model version identity, entry and exit orders, walk rule identity, and override-layer contribution; `no-override` is explicitly declared where the override layer contributes nothing	E	Jupiter
R5-map-b	§02d §6	Independent re-derivability of traversal — each traversal step is re-derivable from the declared model version and walk rule; a step whose outcome cannot be re-derived from those artifacts is observably non-conforming	E	Jupiter
R8a	§02d §6	Distinct order identities not equated — composition at distinct order identities without a registered cross-domain typed interface is refused with a structural violation record; no implicit equivalence is admitted	Y	Jupiter
R8b	§02d §6	Model-pair compatibility record verified — the inspector retrieves both model versions and confirms shared order-shape specifications are identical; a record failing this verification is observably a composition defect	E	Jupiter
R8c	§02d §6	Modality-agnostic combinatorial order analysis — a non-discrete cross-model composition applies the same per-order common structure, shape-identity sameness criterion, and composition witness obligations; omission is non-conforming and not a distinct architecture	E	Jupiter
R9a	§02d §6	Responsible-order attribution survives verification — the finding is re-derivable from the declared order-typed evidence and derivation trace; a finding that does not survive re-derivation is a false grounding reportable at Field 4	E	Jupiter
R9b	§02d §6	Reflexive artifacts order-typed and bounded — triage decisions, cache-hit determinations, and self-modification assessments carry responsible-order attributions and are independently re-derivable; ill-typed self-modifications are refused with a typed gap referral identifying the violated order constraint	Y/E	Jupiter

§02e Jupiter — Pre-Invocation

AIGP boundary integration conditions

Property	Section	Description	Inspector-verifiable	Required for
E1	§02e §10.1	Pre-execution admission verdict received and typed — the Mars® inbound boundary receives a typed ADMIT/REFUSE/REFER verdict before model execution proceeds; an absent or untyped verdict gates execution	Y	Jupiter
E2	§02e §10.2	Order-typed enriched prompt received — the prompt handed to the model is order-typed per the governing specification; an unenriched prompt is not admitted	Y	Jupiter
E3	§02e §10.3	Output validation verdict received — a PASS/FAIL/CONDITIONAL verdict is received after model output and before evidence-gathering verification proceeds	Y	Jupiter
E4	§02e §10.4	Retained admission witnesses carried in Field 7 — the conformance certificate’s recomputation witness chain carries the pre-invocation admission witness links; Field 7 without pre-invocation links does not satisfy the chain requirement where AIGP is deployed	E	Jupiter
E5	§02e §11	AIGP substitution completeness — where AIGP is not deployed, all four AIGP-provided inputs are satisfied by declared substitutions present in the deployment registration	E	Jupiter
E6	§02e §2	Pre-invocation / post-invocation boundary respected — no governance act classified as pre-invocation proceeds after model output production; no governance act classified as post-invocation is performed before model output production	Y	Jupiter
E7	§02e §2	Streaming release gated — no output increment is released before a validation verdict except under the declared incremental-validation mode with running verdicts and increment-level witness links; a mid-stream REFUSE halts release and produces a typed partial-emission event propagated to all consumers of the released prefix; release under neither mode is non-conforming	Y	Jupiter

Architectural refusals (negative-space discipline)

Property	Section	Description	Inspector-verifiable	Required for
AR1	§02e §13	No unregistered pre-invocation signal admitted as battery input — a signal from an unregistered source may not contribute to the IR, the verdict, or the witness chain	Y	Jupiter
AR2	§02e §13	No W1 claim without satisfying full recomputation-witness requirement — a source may not claim W1 witness class unless an independent inspector can re-derive the signal value without executing the original system; no source-identity exemption	Y	Jupiter
AR3	§02e §13	No asserted pre-invocation coverage without chain evidence — a certificate may not claim pre-invocation coverage in Field 5 without corresponding pre-invocation signal links in Field 7	E	Jupiter
AR4	§02e §13	No signal-required gap suppressed — where a source’s absence posture is `signal-required` and no signal is received, the battery may not issue a `conforming` verdict; the gap referral must be present and open	Y	Jupiter
AR5	§02e §13	No cross-phase corroboration claimed without both conditions satisfied — a `pre-invocation-cross-phase` entry may not appear unless both a registered W1/W2 deterministic source and a probabilistic battery method independently evaluated the same conformance question	E	Jupiter

§02e Appendix — AIGP ↔ Mars Bridge

Property	Section	Description	Inspector-verifiable	Required for
BR-H	§02e appendix §6	Witness-class honesty — no AIGP-sourced chain link is annotated W1 unless its witness record independently satisfies the §02e §5.1 recomputation-witness requirement; a blanket brand-level W1 claim is non-conforming	E	Jupiter
BR1	§02e appendix §6	A MATCH/non-conforming disagreement between AIGP and the Mars® battery is recorded as a `pre-invocation-cross-phase` divergence with both attributed contributions; neither silently overrides the other	E	Jupiter
BR2	§02e appendix §6	An AIGP VIOLATION (anti-criterion) forces REFUSE at any downstream actuation gate regardless of the battery verdict	Y	Jupiter
BR3	§02e appendix §6	Divergence between multiple AIGP/AI pre-invocation sources on the same order-typed question is recorded with per-source attribution	E	Jupiter
BR4	§02e appendix §6	Every AIGP-governed internal Mars® AI invocation contributes a pre-invocation witness link to the certificate’s recomputation witness	E	Jupiter
BR5	§02e appendix §6	No Mars® verdict rests on the self-assessment of an internal AI call; the admission of that call is governed and recorded externally	Y/E	Jupiter
BR6	§02e appendix §6	The `autonomy_level` of a Mars® generation agent bounds the actuation classes its output may drive	Y	Jupiter
BR7	§02e appendix §6	A certificate issued while AIGP runs in REPORT mode declares pre-invocation admissibility outside the certified scope in Field 5	E	Jupiter

§02f Jupiter — Post-Hoc Forensics

Property	Section	Description	Inspector-verifiable	Required for
P1	§02f §10	Per-analyst attribution — each AI analyst’s contribution to a forensic finding is attributable to that analyst by order-typed finding element; no finding element is attributable only to “the system”	E	Jupiter
P2	§02f §10	Inter-analyst divergence as a forensic signal — where two or more AI analysts diverge on the same question, a divergence record is present in the forensic output as a first-class artifact; not resolved into an aggregate before recording	E	Jupiter
P3	§02f §10	Recomputable analyst contributions — an independent inspector re-derives each analyst’s contribution and the recorded divergence from the retained witnesses without executing the deployment	E	Jupiter
P4	§02f §10	Order-typed causal attribution — each forensic finding carries a causal attribution tagged by the order(s) under which the finding and its cause are expressed; attribution is not a flat label	E	Jupiter
P5	§02f §10	Evidenced attribution — the causal attribution cites the witness evidence — methods, divergence signals, derivation steps — that supports it	E	Jupiter
P6	§02f §10	Recomputable causal attribution — an independent inspector re-derives the causal-dimension assignment from the finding and its retained witnesses; a mismatch reveals an unsound attribution	E	Jupiter
P7	§02f §10	Order-typed posture state — the adaptive posture state expresses scrutiny tagged by order and policy class, not as a single scalar	E	Jupiter
P8	§02f §10	Recomputable posture transition — an independent inspector re-derives each posture transition from the prior state, the triggering finding, and its causal attribution against retained witnesses	E	Jupiter
P9	§02f §10	Attribution-bound posture change — asked why scrutiny changed, the system returns the bound causal attribution as an evidenced, re-derivable answer	Y	Jupiter
P10	§02f §10	Order-structured longitudinal composition — the longitudinal verdict is the composition of per-interval order-typed analyses across time under the composition discipline, inheriting per-interval soundness anchors	E	Jupiter
P11	§02f §10	Recomputable longitudinal verdict — an independent inspector re-derives the longitudinal verdict from the retained per-interval witnesses	E	Jupiter
P12	§02f §10	Attribution-bound reinforcement action — the reinforcement action is observably a function of the causal attribution, not of a raw condition	Y/E	Jupiter
P13	§02f §10	Re-derivable finding-to-attribution-to-action linkage — an independent inspector re-derives the full finding→attribution→action chain from the retained witnesses	E	Jupiter
P14	§02f §10	Named-target routing — the reinforcement action names a specific governance target	E	Jupiter
P15	§02f §10	Investigate default — a finding whose attribution does not soundly determine an automatable action yields investigate, not an asserted automated action	Y	Jupiter
P16	§02f §10	Governing-bound fallback — given assets but no specification, the forensic layer uses a domain-model-as-spec or reverse-synthesized model-as-spec, declaring the fallback position used	Y	Jupiter
P17	§02f §10	Two-layer asset relation — asset-relative attribution is resolved at the join of KB governance and data-source instance-facts; neither layer alone is treated as sufficient	E	Jupiter
P18	§02f §10	Recomputable asset-relative attribution — the asset-relative attribution is re-derivable by an independent inspector against retained witnesses	E	Jupiter
P19	§02f §10	Sycophancy dual-locus invariance — a post-hoc sycophancy scoring finding carries a content hash linking it to the same registered discrete sycophancy representation as the runtime gate disposition; a finding lacking that hash is not a governed sycophancy finding	E	Jupiter

§03-i Minerva — Semantic Binding

Property	Section	Description	Inspector-verifiable	Required for
S1	§03-i §4	Domain-aspect binding — semantic-map artifact shows fields bound to domain aspects, not only to ontology classes or free-text descriptions	Y	Minerva
S2	§03-i §4	Aspect-keyed, fitness-scored query library — library entries are keyed to domain aspects and carry sample-data fitness signals, not per-utterance NL→query pairs	Y	Minerva
S3	§03-i §4	Multi-locus gap report — gap report carries events at data, domain-model, KB, and specification loci, including cross-locus events	Y	Minerva
S4	§03-i §4	Reverse-path through domain aspect — request → aspect → semantic map + library → fitness-ranked selection; not direct request-to-query generation	Y	Minerva
S5	§03-i §4	Substrate uniformity — downstream artifacts are structurally identical across store kind, characterization representation, and federation topology	Y	Minerva
S6	§03-i §4	Governed structural characterization — for a non-self-documenting source, characterization is produced by a domain-model-directed two-phase procedure, not by generic schema introspection	Y	Minerva
S7	§03-i §4	Plural data source input — semantic binding accepts multiple data sources simultaneously; semantic-map artifact and query library span all sources jointly	Y	Minerva
S8	§03-i §4	Dual-contract admission — a data source is admitted if it satisfies the admission criterion appropriate to its client class; store type alone is not an admission criterion	Y	Minerva
S9	§03-i §4	Non-embedded/embedded client class distinction — non-embedded sources accessed through a Pymnemon-conforming client; embedded sources through an Impera-conforming client; the two are structurally distinct and observably non-interchangeable	Y	Minerva
S10	§03-i §4	Subchunk-level retrieval commitment — the embedded client returns the best-match subchunk, not the enclosing chunk; the returned span carries its own subchunk identifier	Y	Minerva
S11	§03-i §4	KB traversal in query generation — query library entries produced with KB traversal input carry KB-sourced contextual metadata distinct from entries produced from domain mapping alone	E	Minerva
S12	§03-i §4	Simple-query composition — a set of single-table queries bound to one domain aspect may stand in for a composite query; the library carries both strategies with distinct construction-strategy labels	Y	Minerva
S13	§03-i §4	Time-gated query entry — a query entry carrying a temporal gate is refused as evidence when executed outside its declared gate; a time-gate-miss is recorded in the gap report	Y	Minerva
S14	§03-i §4	Reverse-path activation record — a downstream verification operation that consumed query library entries carries a reverse-path activation record in its evidence component	E	Minerva
S15	§03-i §4	Structural characterization procedure — for a non-self-documenting source, a two-phase structural inventory and upward interpretation produces the characterization; unresolved fields emit data locus gaps	Y	Minerva
S16	§03-i §4	Versioned upstream binding — each semantic-map entry and query library entry carries the upstream domain-model version, data-source characterization version, and KB version from which it was derived; staleness is determinable by version comparison without re-derivation	E	Minerva

§03-ii Minerva — Knowledge Base

Property	Section	Description	Inspector-verifiable	Required for
K1	§03-ii §5	Order-typed primitives — primitives are typed by orders and organized along orders; KB is not a flat entity-relation graph. The typing is carried by the aspect identifier (§03-ii §3.2): an inspector parses any entry’s aspect identifier and recovers order type, position in the order-decomposition tree, and the issuing domain-model version. An entry whose index field is an opaque or arbitrary label — UUID, free-form tag, or category annotation — from which those three components cannot be recovered does not satisfy this property, regardless of navigability; the recovered components are what make update-scoped regeneration (D20) computable against a changed model node	Y	Minerva
K2	§03-ii §5	Aspect-bound synthetic variants — variants are bound to the same aspect as their originating primitive and are traceable to that primitive and its source span	E	Minerva
K3	§03-ii §5	N-way navigation — any representation may serve as entry point; any other as lookup target; navigation is entry-point-agnostic	Y	Minerva
K4	§03-ii §5	Per-artifact provenance — each primitive and variant carries provenance to its source span	E	Minerva
K5	§03-ii §5	Primitive-level retrieval — a typed primitive is returned and expanded along the metadata fabric; raw chunk alone is not the retrieval unit	Y	Minerva
K6	§03-ii §5	Portable order-structured package — symbolic store, embedded index, metadata fabric, extraction records, configuration artifacts, and accessor; usable without the creation pipeline	Y	Minerva
K7	§03-ii §5	Map-governed segmentation with subchunk expression — chunk boundaries occur at aspect and order transitions; subchunks are expressed as first-class entries with their own identifiers, aspect bindings, and embedding vector identifiers	Y	Minerva
K8	§03-ii §5	Bidirectional symbolic-embedding round-trip — a vector returned by embedding-space retrieval carries an identifier enabling a direct lookup of its originating primitive in the symbolic store; the round-trip does not require a secondary similarity search	Y	Minerva
K9	§03-ii §5	Controlled transformation admissibility — a transformation T applied to entry e is admissible only when D(T(e), e) ≤ δ under the declared distance function and d(prim(T(e)), prim(e)) ≤ ε; an inadmissible transformation is recorded as a boundary encounter, not applied as a traversal step	Y	Minerva
K10	§03-ii §5	Traversal-governed vs. graph-proximity distinction — KB traversal follows the order-decomposition tree and aspect-binding index; removing or substituting the domain model produces an observably different traversal path	Y	Minerva
K11	§03-ii §3.1a	Six-field variant declaration completeness — every synthetic variant registered in the KB carries all six required fields of the variant declaration record; a variant missing any field is structurally deficient and refused at registration	Y	Minerva
K12	§03-ii §3.1a	Variant consistency map present — a KB carrying synthetic variants carries an attested variant consistency map with per-element and per-pair entries for every declared variant pair	Y	Minerva
K13	§03-ii §3.1a	Per-pair attestation with κ gate — every per-pair entry in the variant consistency map carries an attestation record from a named authority with domain standing; the inter-reviewer agreement statistic meets the declared threshold	Y	Minerva
K14	§03-ii §3.1a	Conflict entry gap propagation — a conflict correspondence type in the variant consistency map produces a KB-variant-locus gap entry in the multi-locus gap report	E	Minerva
K15	§03-ii §3.1a	Pending-re-attestation exclusion from benchmark use — per-pair entries in pending-re-attestation state are excluded from benchmark use at the calibration attestation gate (§02a §5a.6)	Y	Minerva
K16	§03-ii §5	Corpus source-trust admission and propagation — each admitted corpus document carries a declared source-trust tier (attested / first-party / unattested) recorded in the extraction record and propagated unstripped into every derived primitive, variant, evidence record, and verdict; a verdict grounded at an aspect on evidence below the aspect’s declared minimum trust tier is non-conforming; a document admitted without a tier is structurally incomplete	Y	Minerva
K17	§03-ii §5	Embedder-migration conformance — a single KB index holding vectors from two or more distinct embedder versions without a registered cross-embedder calibration mapping is non-conforming; migration proceeds by atomic version cut or dual-index discipline; a traversal over a migrating KB records which index (embedder) each step drew from	Y	Minerva

§03-iii Minerva — Evidence-Gathering Verification

Property	Section	Description	Inspector-verifiable	Required for
EG1	§03-iii §5	Recomputable grounded verdict — an independent inspector re-derives the verdict from the three-invariant witness without trust in the deployment	E	Minerva
EG2	§03-iii §5	Order-structured traversal — traversal path is over aspect-typed primitives structured by orders; not raw chunks or generic index	Y	Minerva
EG3	§03-iii §5	Multi-guide traversal — removing or substituting a guide produces an observably different traversal	Y	Minerva
EG4	§03-iii §5	Combinatorial multi-source evidence — evidence gathered combinatorially; structure is invariant across number and kind of sources	Y	Minerva
EG5	§03-iii §5	Gap-on-insufficiency — system emits a typed gap rather than asserting an unsupported verdict when evidence is insufficient	Y	Minerva
EG6	§03-iii §5	Order-decomposition invariance — traversal, evidence, and verdict structure are invariant across domain; follow the orders of whatever order-decomposed model is provided	Y	Minerva
EG7	§03-iii §5	Symmetric four-artifact-class reinforcement — {model, specification, data-source, KB}-gap signals are observable in the audit trail across all four classes under a single named policy record	Y/E	Minerva
EG8	§03-iii §5	Perspective-guide ablation — same artifact and same governing specification under different perspective specifications produce observably different traversals, witnesses, and verdicts	Y	Minerva
EG9	§03-iii §5	Dual-modality discovery bridged by metadata — text-side and embedding-side modalities are each present; bridged by the metadata fabric; structure is invariant across model class, size, and generation	Y	Minerva
EG10	§03-iii §5	Bounded reversible pondering — displacement-bounded (δ-bounded) transformation returns to the original pre-transformation state within the declared numerical tolerance ε_inv; observable by inspecting transformation trace in the witness	E	Minerva
EG11	§03-iii §5	Ground-truth-anchored, measure-agnostic bounded exploration — removing the ground-truth anchor makes measurement undefined; substituting the declared control functional measure leaves engine behavior structurally unchanged; exploration does not range outside the governing-specification perimeter	Y	Minerva
EG12	§03-iii §5	Governing specification as active formal spec collection — the recomputation witness evidence record names the formal specification(s) active at operation time with their activation conditions; a single flat governing specification identity without activation conditions does not satisfy this property where multiple formal specs are in effect	E	Minerva
EG13	§03-iii §5	Attribution record — fallback rung declared — the attribution record declares which rung of the three-rung fallback hierarchy (governing specification / domain-model-as-spec / reverse-synthesized-model-as-spec) supplied the governing reference; an attribution without this declaration does not conform	E	Minerva
EG14	§03-iii §5	Two-layer join result record — where both a KB and a data source are present in the asset relation, the attribution record carries a join result record keyed by domain aspect identifier; a single-layer attribution in a two-layer context does not conform	E	Minerva
EG15	§03-iii §5	KB ↔ data-source divergence signal — where the two-layer join is in effect and KB governance and data-source instance-facts are inconsistent on the same referent under the declared consistency function, a divergence signal is present in the evidence record; absence of the signal where inconsistency exists is a conformance failure	E	Minerva
EG16	§03-iii §5	Evidence freshness bound enforced — every operational-data evidence entry carries an as-of timestamp; an entry whose age exceeds the aspect’s declared evidence-freshness bound is not admitted as grounding evidence (re-retrieve within bound or emit a typed evidence-staleness gap, locus data / subtype freshness); an aspect on a moving source without a declared bound is refused at registration; a KB currency contract older than the bound does not launder stale state	Y/E	Minerva
EG17	§03-iii §5	Redaction with integrity — redactable evidence values are committed by salted content commitment; erasure deletes the value-and-salt and records a typed redaction event while the commitment and hash chain remain intact; re-derivation over redacted evidence yields a typed redacted-evidence result (provably complete-as-of-issuance, lawfully-redacted-thereafter), not a broken witness	Y/E	Minerva
EG18	§03-iii §5	Access classification and entitlement-scoped traversal — each evidence entry carries an access classification inherited from its source and propagated unstripped into witness and verdict; re-derivation above an inspector’s entitlement yields a typed entitlement-restricted result preserving structural verifiability without content disclosure; traversal outside its declared entitlement scope is refused at the source boundary and recorded as a typed entitlement gap (locus data / subtype entitlement)	Y/E	Minerva

§03-v Minerva — Governed Services

Property	Section	Description	Inspector-verifiable	Required for
GS1	§03-v §3	Asset-relative generation — each generated artifact’s audit record cites the governing asset identities and versions at the time of its generation; an artifact with no governing-asset citation is not a governed-service artifact	E	Minerva
GS2	§03-v §3	Heterogeneous class under one discipline — the same service registration record governs generation of datasets and at least two model subclasses (analytical, probabilistic, deep-learning); separate per-subclass registrations without a unifying service registration do not satisfy this property	E	Minerva
GS3	§03-v §3	Order-typed artifact — each generated artifact carries a per-artifact order-type declaration referencing the governing domain model’s orders; a service-level tag without per-artifact typing does not satisfy this property	Y	Minerva
GS4	§03-v §3	Recomputable provenance and conformance — an independent inspector re-derives both the artifact’s governing-asset provenance and its conformance to the governing specification’s aspect structure from the retained witness, without access to the deployment	E	Minerva
GS5	§03-v §3	Governed-service audit record — each generation invocation emits an audit record in the specification registry carrying the operation identity, governing asset versions, produced artifact content hashes, and invocation timestamp; a post-hoc registration of outputs without a contemporaneous audit record does not satisfy this property	E	Minerva
GS6	§03-v §3	Operation-level governance — the registration, versioning, and audit-emission are properties of the generation operation itself; removing or substituting the specification registry yields a generation pipeline with no governed-service audit trail, observably different from the governed service	Y	Minerva
GS7	§03-v §3	Governed decision service — a query→decision API is a governed decision service subject to the four discipline requirements; its output is the decision bundle (order-typed verdict + §03-iii §2.7 witness + freshness dispositions + governing asset versions), a registered artifact enrolled in the delta-attestation lifecycle; a decision API registering no operation, emitting no audit record, or producing no recomputable decision bundle is an ungoverned decision pipeline	E	Minerva
GS8	§03-v §3	Declared freshness and degradation — a decision service on operational data declares per-aspect evidence-freshness bounds and a degradation mode (fail-closed / fail-stale-declared / fail-to-authority); the decision bundle records which mode governed each decision; silent emission of a decision whose bundle does not disclose that grounding evidence exceeded the freshness bound is non-conforming	Y/E	Minerva
GS9	§03-v §3	Decision actuation continuity — where a governed decision authorizes a downstream non-linguistic or persistent-state effect, the decision bundle is the originating verification record at the §02c actuation anchor (Field 1) and its freshness disposition propagates to the actuation gate; a fail-stale-declared decision carries its non-fresh annotation to the gate	Y	Minerva

§03-iv Minerva — Governed Artifact Production

Property	Section	Description	Inspector-verifiable	Required for
GP1	§03-iv §2	Three-invariant generation witness — generation trace, admissibility record, and coverage record are co-present in the recomputation witness for every governed data generation act; a witness omitting any invariant is structurally deficient	E	Minerva
GP2	§03-iv §2	Per-item content-hash tamper binding — recomputing the content hash of each item in the corpus as received matches the per-item hash in the generation trace; a mismatch on any item is scoped to the affected item(s) and indicates alteration of the corpus or the witness	Y/E	Minerva
GP3	§03-iv §2	Generation-time typing — each generated item carries its domain aspect identifier, order type, generation specification version, and generation-act identifier assigned at generation time, not post-hoc; where a corpus spans multiple generation acts, each item carries its own generation specification version	E	Minerva
GP4	§03-iv §2	Generation specification amendment classified — an amendment to the generation specification is classified under the four-valued delta lifecycle; a scope-restricting amendment places affected certificates in conditionally-valid state and blocks downstream use pending a consistency determination	Y	Minerva
GP5	§03-iv §2	Consistency determination witness — carries the governing specification version at determination time, the prior and amended generation specification versions, the evaluated items by content hash, and per-item admissibility records including shim identity and version sub-records where a shim was applied	E	Minerva
GP6	§03-iv §2	Scope-breaking retirement — a scope-breaking generation specification amendment retires all prior-version items and invalidates affected certificates with no consistency-determination path; a new generation act is the only path to a new certificate	Y	Minerva
GP7	§03-iv §2	Shim discipline — a generation specification shim is declared and registered before application, enrolled in the delta-attestation lifecycle, and its per-item application is recorded in the consistency determination witness; a shim-transformed item carries the amended version and a transformation record	E	Minerva
GP8	§03-iv §2	Cross-version certificate chain — every re-issued governing-data-generation certificate carries the prior certificate identity, the triggering amendment, the consistency determination witness, and the outcome in Field 3; the full amendment and consistency chain is traversable by cross-version references	E	Minerva
GP9	§03-iv §2	Capsule completeness and self-containment — a produced generation environment capsule carries the artifact manifest, dynamic input record, generation model binding, environment timestamp, and generated corpus binding; its content hash covers all components; no component requires live network resolution; every input whose value depended on live infrastructure state at generation time is recorded	E	Minerva
GP10	§03-iv §2	Capsule status declared and re-use gated — Field 5 declares capsule status (produced or absent) on every governing-data-generation certificate; a capsule-absent certificate re-used in a capsule-required context is blocked until a capsule is produced, recorded as a Field 3 update	Y	Minerva
GP11	§03-iv §3	Three-invariant benchmark witness — derivation trace, coverage record, and falsifier record are co-present in the recomputation witness for every governed benchmark generation act	E	Minerva
GP12	§03-iv §3	Test-case structural completeness — every test case carries case identity, content hash, aspect binding, order type, input, expected outcome, derivation record, and falsifier annotation; the benchmark aggregate hash is computed over lexicographically ordered case content hashes	E	Minerva
GP13	§03-iv §3	Specification-derived expected outcomes — each test case’s expected outcome is re-derivable from the governing specification clause(s) named in its derivation record; a benchmark whose cases derive from empirical observation rather than specification clauses is not a governed benchmark	Y/E	Minerva
GP14	§03-iv §3	Hash-scoped staleness — a scope-restricting or scope-breaking specification amendment flags stale only the test cases whose derivation records reference the amended clause(s); stale cases are excluded from evaluation until regenerated under the updated specification version	Y	Minerva
GP15	§03-iv §3	Three-scenario mechanism invariance — new, modified, and external models are evaluated by the identical benchmark mechanism; only the certificate path differs across the three scenarios	Y	Minerva
GP16	§03-iv §3	Declared modification record gate — a modified model without a declared modification record and registered modification artifact identity is treated as a new model and receives no delta classification; undeclared optimization cannot enter the delta path	Y	Minerva
GP17	§03-iv §3	Model-evaluation witness — evaluation trace, verdict derivation record, and benchmark version binding are co-present; per-case outcomes are drawn from the registered outcome vocabulary	E	Minerva
GP18	§03-iv §3	Modification delta cascade — a scope-restricting or scope-breaking modification delta triggers the delta-attestation cascade for downstream governed artifacts whose certificate path references the prior model version	Y	Minerva
GP19	§03-iv §3	Consumer registration and output contract — every benchmark consumer is registered with consumer identity, evaluation interface, input contract, output contract, and scope declaration; its verification result carries per-test-case outcomes, an aggregate verdict, and a recomputation witness sufficient for independent re-derivation	E	Minerva
GP20	§03-iv §3	Outcome vocabulary conformance — per-case outcome classifications are drawn from the registered vocabulary {match, mismatch, partial-match, tolerance-boundary, indeterminate} or a registered extension; a consumer with a narrower vocabulary notes the narrowing in its scope declaration	E	Minerva
GP21	§03-iv §3	Multi-consumer non-merging — where multiple consumers evaluate the same benchmark against the same model, their results are collected in a multi-consumer evaluation record without merging into a single verdict; each result is independently recomputable; the admissibility condition is a registered governing-specification parameter	E	Minerva
GP22	§03-iv §3	External documentation non-substitution — vendor safety cards, published evaluation results, and model cards do not substitute for or supplement the benchmark-derived model-behavior certificate; an external model is evaluable only through the benchmark	Y	Minerva
GP23	§03-iv §3	Train/evaluation disjointness — a model-behavior certificate is conforming only if the benchmark’s test cases and the model’s registered training corpus are disjoint under a declared similarity bound (content-hash intersection plus near-duplication threshold); contaminated cases narrow scope or cause refusal; every certificate carries a benchmark-exposure record with the disjointness result; undeclared or external training history carries an honest exposure annotation and may not claim clean-disjointness	Y/E	Minerva
GP24	§03-iv §3	Closed-loop separation — a generative-loop trajectory witness carries per-iteration train/benchmark disjointness results; a loop evaluating a candidate against a benchmark not disjoint from its own generated training partition under the declared similarity bound is overfitting-by-construction, not a governed evaluation, and is non-conforming	E	Minerva

§04 Reasoning — Governed Autonomous Reasoning

Capability-gated (§04 §1): these properties apply only to a deployment that performs autonomous acquisition or autonomous higher-order synthesis. A deployment that does neither is unaffected.

Property	Section	Description	Inspector-verifiable	Required for
AR-L1	§04 §4	Gap-driven acquisition — every autonomous acquisition action’s record cites a gap record in Open or a recorded calibration divergence existing at initiation; an acquisition action citing neither is refused, because autonomous acquisition is driven by the governed gap set, not an ungoverned internal objective	E	Reasoning
AR-L2	§04 §4	Map-governed autonomous traversal — every autonomous traversal hop records an authorizing guide and follows the bidirectional cross-reference or order-decomposition structure; substituting or removing a guide observably changes the path; a proximity-only hop with no governing guide is refused	Y/E	Reasoning
AR-L3	§04 §4	Declared autonomous synthesis input — every autonomous higher-order synthesis act carries a composition-provenance record enumerating its bounded input selection with version markers; an autonomous synthesis with an unrecorded or unbounded input selection does not conform	E	Reasoning
AR-L4	§04 §4	Registration before reuse — no loop iteration consumes an unregistered product of a prior iteration; every acquired or synthesized increment is registered (delta-attestation scope-extending amendment or gap-record closure witness) before it propagates; a loop consuming an unregistered prior product does not conform	E	Reasoning
AR-L5	§04 §4	Recomputable loop trail — for a sampled completed iteration, an independent inspector re-derives the gap-or-divergence → governed traversal → acquisition-or-synthesis → registration → resulting-version chain from retained records alone, without deployment access; an iteration whose trail cannot be re-derived does not conform	Y/E	Reasoning
AR-L6	§04 §4	Declared termination discipline — the autonomous loop carries a declared termination or continuation discipline (iteration bound, convergence criterion, resource budget, or operator-revocable standing authorization); an unbounded loop with no declared discipline does not conform	E	Reasoning
AR-L7	§04 §4	No autonomy by disclaimer — where acquisition or synthesis actions occur with no corresponding human authorization act in the retained record, the capability is treated as present and §04 §2–§3 apply regardless of how the deployment describes itself	Y/E	Reasoning

Checklist summary

Layer	Section(s)	Property count
Juno	§01	48 (D0–D44, P8-1–P8-3)
Jupiter — Base Analysis	§02a, §02b	103 (SA1–SA16, R1–R10, SC1–SC11, IR1–IR9, G1–G11, B1–B12, V1–V11, T1–T6, F1–F9, CA1–CA8)
Jupiter — Delta-Attestation	§02b §5, §8	8 (DA1–DA8)
Jupiter — Deployment Manifest	§02b §6	10 (DR1–DR10)
Jupiter — ON_CHAIN_ANCHOR	§02b §7, §8	7 (L1–L7)
Jupiter — Model Moderation	§02b §5.5	2 (BC1, MD1)
Jupiter — Integrated Boundary	§02c	20 (IB1–IB20)
Jupiter — Actuation	§02c §4, §4.4	20 (J1–J16, AC1–AC4)
Jupiter — Non-Language Bridge	§02c	5 (NB1–NB5)
Jupiter — Discrete Composition	§02d §6	14 (R5a–R5f, R5-map, R5-map-b, R8a–R8c, R9a, R9b)
Jupiter — Pre-Invocation	§02e	12 (E1–E7, AR1–AR5)
Jupiter — AIGP ↔ Mars Bridge	§02e appendix	8 (BR-H, BR1–BR7)
Jupiter — Post-Hoc Forensics	§02f §10	19 (P1–P19)
Minerva — Semantic Binding	§03-i	16 (S1–S16)
Minerva — Knowledge Base	§03-ii	17 (K1–K17)
Minerva — Evidence-Gathering	§03-iii	18 (EG1–EG18)
Minerva — Governed Production	§03-iv	24 (GP1–GP24)
Minerva — Governed Services	§03-v	9 (GS1–GS9)
Reasoning — Governed Autonomous Reasoning (capability-gated)	§04	7 (AR-L1–AR-L7)
Total		368

A full conformance certification assessment applies every property in the layer(s) licensed. Partial conformance — against a subset of properties within a licensed layer — is not a recognized conformance state.