§03-iii Minerva — Evidence Gathering — Inspector verification (property table)
Mars® Spec › §03-iii Minerva — Evidence Gathering › Inspector verification (property table)
5. Inspector verification (property table)
The following properties are externally observable by a qualified inspector without access to internal system state.
| Property | Observable indicator | Load-bearing |
|---|---|---|
| S1 Recomputable grounded verdict | An independent inspector re-derives the verdict from the three-invariant witness without trust in the deployment | Yes |
| S2 Order-structured traversal | Traversal path is over aspect-typed primitives structured by orders; not raw chunks or generic index | Yes |
| S3 Multi-guide traversal | Removing or substituting a guide produces an observably different traversal | — |
| S4 Combinatorial multi-source evidence | Evidence gathered combinatorially; structure is invariant across number and kind of sources | — |
| S5 Gap-on-insufficiency | System emits a gap rather than asserting an unsupported verdict when evidence is insufficient | — |
| S6 Order-decomposition invariance | Traversal, evidence, and verdict structure are invariant across domain; follow the orders of whatever order-decomposed model is provided | Yes |
| S7 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 | Yes |
| S8 Perspective-guide ablation | Same artifact and same governing specification under different perspective specifications produce observably different traversals, witnesses, and verdicts | Yes |
| S9 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 | — |
| S10 Bounded reversible pondering | Controlled 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 | — |
| S11 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; multi-directional exploration is observable in the traversal trace | Yes |
| S12 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 | Yes |
| S13 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 | Yes |
| S14 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 | Yes |
| S15 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 | Yes |
| S16 Evidence freshness bound enforced | Every operational-data evidence entry carries an as-of timestamp; an entry whose age (verdict time minus as-of time) exceeds the aspect’s declared evidence-freshness bound is not admitted as grounding evidence — the verifier re-retrieves within bound or emits a typed evidence-staleness gap (locus data, subtype freshness); an aspect drawing on a moving source without a declared freshness bound is refused at registration; a KB currency contract older than the bound does not launder stale state | Yes |
| S17 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, not a broken witness — the witness is provably complete-as-of-issuance and lawfully-redacted-thereafter | Yes/E |
| S18 Access classification and entitlement-scoped traversal | Each evidence entry carries an access classification inherited from its source and propagated unstripped into the witness and verdict; re-derivation over an entry above the inspector’s entitlement yields a typed entitlement-restricted result preserving structural verifiability without disclosing content; traversal retrieving from a source outside its declared entitlement scope is refused at the source boundary and recorded as a typed entitlement gap (locus data, subtype entitlement) | Yes/E |