§02a Jupiter — Base Analysis — Externally-observable properties
Mars® Spec › §02a Jupiter — Base Analysis › Externally-observable properties
← Verdict, gap analysis, and outputs · Section index
8. Externally-observable properties
The following externally-observable properties are the verification surface for this layer. An independent inspector verifies compliance by confirming that each applicable property is exhibited by the deployment.
Properties marked (load-bearing) are the primary structural distinguishers: a deployment that exhibits only prior-art features will not exhibit them. SA1, SA2, SA4, SA6, SA8, and SA9 are the most load-bearing analysis-method properties; R1, R4, R5, R7, and R8 are the most load-bearing discrete-representation properties.
Analysis methods:
| Property | Observable condition |
|---|---|
| SA1 — Order-typed analysis/lift artifact (load-bearing) | Produced formulae, symbols, and findings are tagged by order, not as a flat concept enumeration |
| SA2 — Audit-binding recomputation witness (load-bearing) | Independent inspector re-derives lifted form and verdict from source under the governing specification |
| SA3 — Multi-source provenance | Result cites one or more domain models × knowledge bases × data sources × specifications |
| SA4 — Cross-method corroboration signal (load-bearing) | Deterministic↔probabilistic divergence recorded as a measure contributing to the verdict; present when both families are deployed |
| SA5 — Composable-battery / single-method invariance | Analysis-artifact structure is invariant whether deterministic-only, probabilistic-only, symbolic-only, empirical-only, or mixed |
| SA6 — Gap and reinforcement (load-bearing) | Typed gaps by locus and reinforcement routing emitted in lieu of unsupported verdicts |
| SA7 — Perspective ablation | Same artifact and governing specification analyzed under different perspectives produce observably different analyses and verdicts |
| SA8 — Order-decomposition invariance (load-bearing) | Analysis, lift, and verdict structure follow the orders of whatever order-decomposed model is provided |
| SA9 — Reverse-composition (load-bearing) | Presenting no governing specification yields a composed specification from available artifacts, bound to and recomputable from those artifacts |
| SA10 — Pre-invocation signal admission gated on registration | A signal from an unregistered source is observably not admitted as a battery input; it may appear in Field 6 but does not contribute to the IR or the verdict |
| SA11 — Pre-invocation signal order-typing enforced | A signal from a source declaring specific orders enters the IR as a fully order-typed element in those orders; a signal from an order-agnostic source enters as untyped-pending and requires disambiguation before IR-level consumption |
| SA12 — Witness chain spans pre-invocation links | The multi-stage witness chain carries pre-invocation signal links prepended before the raw-input link; each pre-invocation link carries its witness class annotation; W1 links are independently re-derivable; W2/W3 links carry auditable-attestation provenance with the recomputability gap explicitly declared |
| SA13 — 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 contributing to the verdict |
| SA14 — 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 in the outputs; no conforming verdict is issued while the gap is open |
| SA15 — Signal-absent posture declared in scope | Where any registered source is absent (optional, suppressed, or not registered), the declared-scope invariant (Field 5) reflects the corresponding pre-invocation coverage exclusion; the certificate does not claim pre-invocation coverage it does not have |
| SA16 — W1 / non-W1 distinction observable | A downstream consumer can determine from the witness chain which pre-invocation links are W1 (fully recomputable) and which are W2 or W3 (auditable but not recomputable); the distinction is carried as an observable witness-class annotation on each link, not inferred |
Discrete representations:
| Property | Observable condition |
|---|---|
| R1 — Order-typed representation (load-bearing) | Representation tagged by order, not flat concept enumeration |
| R2 — Genus invariance | Output structure invariant across representation kind (structure follows order shape; representation kind is carrier only) |
| R3 — Multi-source formation including data-source-alone | Formed from {model, spec, KB, data source} in any combination including data source alone |
| R4 — Audit-binding recomputation witness (formation and use) (load-bearing) | Independently re-derivable from source under orders; traversal and use also verifiable |
| R5 — Composed order-structured program (load-bearing) | Executable composed discrete program observably composing orders; in layered embodiment, observably executing as order-governed traversal under a model as map with specification override layer |
| R6 — Reuse without limitation / infrastructure-agnosticism | Single output consumed by two or more distinct consumers without re-derivation; not predicated on any deployment-trust infrastructure |
| R7 — Order-attributed emergent output (load-bearing) | Emergent higher-order output order-typed and re-derivable from source under the orders |
| R8 — Cross-model composition by order (load-bearing) | Composition of same-order representations admitted by order’s common structure; cross-model higher-order order yields witness-bound emergent output |
| R9 — Subject-directed determination identifying the responsible order | Finding is order-typed, audit-bound, re-derivable, and identifies the responsible order — not a black-box score with post-hoc explanation |
| R10 — Reflexive artifacts re-derivable; self-modification order-bounded | Triage decision or cache hit re-derives under the orders; ill-typed self-modification is rejected |
Intermediate representations and multi-stage pipelines:
| Property | Observable condition |
|---|---|
| IR1 — Order-shape contract enforced at each IR stage | Each IR stage carries order-type assignments per element; elements in the same order’s owner-set share a uniform structure at that stage; the contract is satisfied stage-locally, not deferred to the final form |
| IR2 — Partial type states observable | An IR element in provisional or untyped-pending state carries an observable type-state tag; it is not silently promoted to fully-typed; disambiguation records are present for provisionally-typed elements |
| IR3 — Multi-stage witness chain present and chainable | Each stage in the pipeline contributes an observable witness link; the chain from raw input through each IR to the final form is independently traversable; any link’s content hash is verifiable against its stage artifact |
| IR4 — Convergence criterion declared and applied | The convergence criterion governing promotion from probabilistic IR to discrete form is present in the deployment registration and in the scope invariant (Field 5); resolved elements carry convergence records; unresolved elements are carried as provisionally-typed with convergence measures |
| IR5 — Declared-irreducible entries present where applicable | Elements that cannot be fully resolved to a discrete form carry declared-irreducible entries with irreducibility basis and scope impact; they are not silently omitted, silently promoted, or absorbed into the verdict without scope declaration |
| IR6 — 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; the record is observably not a certificate and does not satisfy the grounded-verdict invariant |
| IR7 — Symbolic execution precondition enforced | Symbolic execution does not proceed over provisionally-typed or untyped-pending IR elements; those elements are either resolved first or declared-irreducible before symbolic execution of their paths is attempted |
| IR8 — Path-exploration strategy declared and coverage recorded | The deployed path-exploration strategy and its parameters are present in the scope invariant (Field 5); the coverage record identifies explored paths, bounded paths, and governing-specification predicate coverage; unexplored paths are recorded as coverage-bounded declared-irreducible entries |
| IR9 — 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; the layer assignment determines what each method operates over and what it produces |
Battery execution and verdict discipline (§3a):
| Property | Observable condition |
|---|---|
| B1 — Mechanical tri-state status (load-bearing) | Verdict status CERTIFY/REFUSE/REFER determined solely from (passed, has-falsifier) tuples across the declared pass set; invariant to pass execution order; identical inputs reproduce identical status |
| B2 — Per-pass audit with execution provenance | Audit chain records execution_stratum, cache-hit, substrate-version, typed falsifier, battery-method-identity, and orders-acted-upon per pass; chain is append-only, hash-chained, and tamper-evident; a pass record missing the orders-acted-upon field is structurally deficient |
| B3 — Pass soundness-anchor independence from model-internal signals | No declared pass carries a model-internal signal as its soundness anchor; a pass whose result cannot be reproduced from the declared soundness anchor without internal deployment access is observably non-conforming |
| B4 — Re-entrance cycle detection | Submitting a composition invoking the same (analysis-spec-identity, pass-name) pair twice in one session produces REFUSE with a cycle descriptor identifying the repeated tuple and its prior position |
| B5 — Pre-emission gating | Introducing a provenance gap on any predicate in the bundle (per the applicable boundary section) or an authority conflict produces pipeline termination and a REFER record; no subsequent pass executes after termination |
| B6 — Open declared pass set | Additional passes may be declared and registered with soundness anchors and ordering constraints; the composition discipline applies identically to the extended set; no deployment may remove a registered pass without re-registering under the amended declared pass set |
| B7 — Procedural-confidence recomputability | An independent inspector re-derives the procedural-confidence value from the PassRecord set using the declared weights and normalization procedure; the re-derived value matches the issued value |
| B8 — Audit chain tamper evidence | Modifying any prior pass record produces an observable chain hash mismatch at the next link |
| B9 — Anchor-inheritance records present in CertifiedBundle (load-bearing) | Each CertifiedBundle carries per-obligation soundness anchor-inheritance records tied to the order-structure of the discrete representation; a bundle missing anchor-inheritance records is observably structurally deficient; the anchor trail distinguishes the composed verdict from a verdict aggregation without a soundness lineage |
| B10 — CertifiedBundle co-required fields complete | A CertifiedBundle is admitted by downstream gates only when all five co-required fields are present: typed predicates, scope certificate, composed discrete program (where produced), verdict with anchor-inheritance records, and audit chain pointer; absence of any field is a structural deficiency refusable at gate |
| B11 — Falsifier absoluteness under DDIL state | Presenting a pass with a non-null falsifier under any execution_stratum and any ddil_state produces REFUSE; no deployment configuration produces REFER in place of REFUSE when a falsifier is present; the absoluteness of this rule is independently observable by submitting falsifier-bearing passes under degraded or disconnected ddil_state values |
| B12 — Stale substrate cache rejection | A cache lookup serving a PassRecord produced under a mismatched substrate-version tuple is observably refused and triggers re-execution; no stale PassRecord is admitted as a valid cache hit |
Traversability (§4b):
| Property | Observable condition |
|---|---|
| V1 — Traversal witness present and chainable (load-bearing) | Each traversal act produces an observable traversal witness link in the multi-stage witness chain carrying all minimum required fields (§4b.4); an independent inspector re-derives the full traversal path — inputs, transformation sequence, positions reached, surfaced content, and analysis act outputs — from the witness without deployment access; a traversal act whose witness is absent or incomplete is observably non-conforming |
| V2 — Governing structural invariant satisfied (load-bearing) | Every traversal act, regardless of its mathematical form or pipeline layer, satisfies all five conditions of the governing structural invariant (§4b intro): declared inputs bound to aspect structure, declared and registered parameters, recomputable outputs, order-typed and aspect-keyed outputs, and a traversal witness link in the chain; a traversal mechanism that satisfies the invariant by a different mathematical route than the enumerated classes is governed; one that does not satisfy the invariant is observably non-conforming regardless of output resemblance |
| V3 — Transformation sequence declared and recomputable | Each controlled embedding transformation in the sequence carries its transformation class identity, declared parameters, pre-transformation embedding content hash, and post-transformation embedding content hash; re-applying the declared transformation to the pre-transformation embedding reproduces the post-transformation embedding within the declared tolerance; a transformation without a pre/post hash binding is not a governed transformation act |
| V4 — Analysis act outputs order-typed and aspect-keyed (load-bearing) | Every traversal-driven analysis act produces an output that declares the domain aspect(s) at which it was performed, the orders and perspectives in effect, and carries a binding to the traversal witness that supplied the content; an act that produces a verdict without an aspect-keyed, witness-bound output is observably non-conforming |
| V5 — Traversal-surfaced content aspect-indexed | KB entries, data source fields, and query library entries surfaced by traversal carry the domain aspect identifier that binds them to the governing domain model; content without an aspect identifier binding is not admitted as traversal-surfaced content and is not a valid input to a traversal-driven analysis act |
| V6 — Steering-conflict recorded, not silently resolved | Where multiple steering inputs conflict, a steering-conflict entry is present in the traversal witness; no silent resolution occurs; the conflict is observable and carried through the witness chain |
| V7 — Higher-order analysis gap emitted on undeclared relationship | Where traversal reveals two or more aspects in proximity whose cross-order or cross-perspective relationship record is absent or undeclared, a typed gap referral with locus higher-order-analysis is observably emitted carrying the aspect identifiers, orders, perspectives, and traversal witness hash; no conforming verdict is issued over the undeclared relationship without the gap referral |
| V8 — Cross-artifact consistency gap emitted on governing artifact conflict | Where traversal reveals that two or more governing artifacts assert inconsistent or contested values at the same domain aspect, a typed gap referral with locus cross-artifact-consistency is observably emitted carrying the aspect identifier, the conflicting artifact identities and versions, their asserted values, and the traversal witness hash; this gap is distinct from the KB ↔ data source divergence signal (§03-iii §2.12) |
| V9 — Formal specification battery invocation observably distinct | Where a formal specification is the target of a dedicated traversal-driven battery, the invocation record is observably distinct from a target-analysis invocation; the verdict produced identifies the specification itself as the target, not an external artifact |
| V10 — Traversal witness in chain at correct position | The multi-stage witness chain carries traversal witness links after IR stage links and before analysis act links; the domain model version and governing specification version are present in each traversal witness link; an analysis act whose traversal witness is absent from the chain or whose domain model version does not match the current domain model registry entry is observably non-conforming |
| V11 — Precomputed traversal artifacts governed identically | A precomputed traversal artifact carries a conforming traversal witness satisfying all minimum required fields; serving a precomputed result without a conforming traversal witness is not a governed traversal act and is observably distinguishable from one |
Additional structural properties:
| Property | Observable condition |
|---|---|
| G2 — Interaction-protocol lift to order-typed form present in witness chain | Where the target is interaction-mediated (§02b §2.1 Class A — interaction-mediated), the multi-stage witness chain carries: (i) a protocol-specification lift link — the interaction-protocol specification as of the analysis instant, content-addressed, positioned before the analysis-act links; and (ii) a trace-record lift link — the complete interaction trace including all observable external-state transitions, positioned immediately after the protocol-specification lift link; an inspector re-derives the order-typed representation from these two links without live interaction; a witness chain for an interaction-mediated target that carries analysis-act links without the preceding protocol-specification lift link and trace-record lift link is observably non-conforming |
| G3 — Divergence signal aggregation function declared and recomputable | Where the battery produces more than one divergence signal, the analysis battery record carries the aggregation function identity and parameters; an independent inspector applying the declared function to the recorded per-pair signals reproduces the composite contribution |
| G7 — Field 3 evidence references resolve to analysis battery record entries | Each evidence reference in Field 3 resolves to a specific method entry in the analysis battery record with a matching content hash; a Field 3 entry whose evidence reference does not resolve is observably non-conforming |
| G8 — Source registration records in registry with versioning and tamper-evidence | The specification registry carries pre-invocation signal source registration records meeting content-addressability, append-only, and tamper-evidence requirements; each certificate’s analysis battery record carries the source registration version in effect at analysis time; a scope-breaking source registration update triggers cascading revocation of affected certificates |
| G1, G4–G6, G9–G11 — See §02b §8 | Properties G1, G4, G5, G6, G9, G10, and G11 govern certificate-level behavior (pipeline-composed target certification, bootstrap provenance failure, registry conflict handling, composite certificate chains, bounded-analysis records, reverse-composed specification lifecycle, and admissibility relation registration). Their normative definitions are in §02b §8 (Additional structural properties and Governing ground truth and bootstrap). |
Governing ground truth and bootstrap (§2):
| Property | Observable condition |
|---|---|
| T1 — Bootstrap binary-falsifiability (load-bearing) | Presenting a candidate specification whose declared inter-rater agreement statistic value falls below the registered threshold produces a typed rejection record and no emitted specification; presenting a candidate that fails SMT ground-discharge produces a typed rejection record and no emitted specification; no partial emission or operator-override path exists |
| T2 — Emitted specification bundle co-presence (load-bearing) | Every registered governing specification carries all four bundle components (compiled predicates, SMT discharge record, faithfulness anchor, scope-of-applicability certificate); a registry query for any emitted specification returns all four; a bundle missing any component is refused at registration with a typed rejection identifying the absent component |
| T3 — Composed chain scope monotone narrowing | Where three specifications are composed through aligned typed interfaces, the composed scope is verifiably ⊆ each constituent sub-scope; a composition that widens any constituent scope fails the typed-interface alignment check |
| T4 — Composed chain rule-trace concatenation | The rule trace of the composed chain carries identifiable per-specification trace segments in order: analysis specification trace, then interpretation-generation trace, then interpretation-analysis trace; an inspector can attribute each fired predicate to its constituent specification |
| T5 — Single-specification deployment scope | A deployment operating only the analysis specification cannot claim the composed-chain scope, rule-trace, or faithfulness-anchor-lineage properties; those properties are observably absent from its certificates |
| T6 — Bootstrap rejection record present on failure | A failed bootstrap attempt produces an observable typed rejection record in the audit trail carrying stage, candidate identity, measured value, threshold, and timestamp; the rejection record is registered and tamper-evident |
| Federated authority reconcile (§3a.3 AR-gate): |
| Property | Observable condition |
|---|---|
| F1 — PeerFinding messages registered in audit chain (load-bearing) | Every received PeerFinding is recorded in the receiving agent’s audit chain with message_id, source_agent_id, artifact_content_hash, and verdict_status; an agent that does not record received PeerFindings is observably non-conforming |
| F2 — No-unverified-propagation invariant enforced (load-bearing) | A local re-verification PassRecord precedes any inter-agent consensus record in the audit chain for every peer-supplied finding; under adversarial-peer simulation, an agent that emits CERTIFY based on a peer CERTIFY without a local re-verification PassRecord exhibits an observable conformance defect |
| F3 — Divergence detection triggers AR-gate without exception | A receiving agent that holds a distinct verdict status from a peer for the same artifact under the same content hash does not emit CERTIFY; the AR-gate is triggered; a deployment that permits CERTIFY emission despite a known peer divergence is observably non-conforming |
| F4 — ReconciliationEvent emitted with stable divergence_id | Every AR-gate trigger produces a ReconciliationEvent carrying a stable divergence_id; re-emissions for the same divergence instance carry the same divergence_id; an inspector can reconstruct the full history of a divergence instance from divergence_id across all participating agents’ audit chains |
| F5 — CERTIFY suppressed while gap Open or In-resolution | No CertifiedBundle for the artifact under the same artifact_content_hash and source_spec_id/version is present in the registry while the corresponding governing-conflict gap record (§01 §12.4) is in Open or In-resolution state; the suppression is independently observable by querying the registry and the gap record |
| F6 — Resolution outcome typed and registered | The outcome of divergence resolution is one of the four enumerated types (ratify_amend, admit_after_review, refuse_with_justification, escalate); the outcome record is appended to the gap record and to the audit chain of each participating agent; an outcome record missing the outcome type is structurally deficient |
| F7 — ratify_amend triggers delta-attestation and soundness-declaration re-discharge | A ratify_amend outcome observably enters the delta-attestation lifecycle (§02b §5); if the amendment is scope-breaking, prior CertifiedBundles are observably revoked; the soundness declaration content hash (§01 §7 Component E) is recomputed and the bundle version identifier updated; no prior bundle carrying the old soundness-declaration hash is admitted as current |
| F8 — Partition-recovery bounds declared and observed | The deployment registration carries a declared handshake bound and a declared consistency-recovery bound — registered parameters of the runtime configuration record (canonical defaults: 2 seconds and 60 seconds), with declared justification where longer; the partition-recovery audit record carries measured handshake and consistency-recovery durations against the declared bounds; a partition-era CERTIFY is annotated as partition_era_provisional and is not admitted as a stable verdict until re-discharged post-recovery |
| F9 — Capability advertisement verified by adversarial-peer test | A deployment advertising AUTHORITY_RECONCILE/1.0 passes all seven AR-gate requirement tests (F1–F8 and the upward-strict-stronger rule) under adversarial-peer simulation; partial implementation advertising the full capability is observably non-conforming |
Calibration attestation gate (§5a.6):
| Property | Observable condition |
|---|---|
| CA1 — 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 |
| CA2 — 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; a calibration record referencing an unregistered or unattested benchmark is non-conforming |
| CA3 — 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 |
| CA4 — 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 under an amended manifest version |
| CA5 — 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 |
| CA6 — 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; the new calibration record is registered before the amended manifest version takes effect |
| CA7 — Benchmark version binding enforced | A calibration record produced under a benchmark version whose governing specification, KB variant consistency map, or domain model version binding has been superseded produces a stale-benchmark finding; the certificate carries a stale-benchmark falsifier annotation in Field 6 |
| CA8 — 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 |