From 8cbd0a4fab4b7a71a9f33b5f34f1c3bc865bb3c4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 29 Oct 2026 22:32:54 +0000 Subject: [PATCH 1/4] docs(vcl-ut): distinguish fixed gate rungs from open-ended Kategoria type research --- docs/status/RECON-OBLIGATIONS-2026-10-29.adoc | 68 ++++++++++++++++++- 1 file changed, 66 insertions(+), 2 deletions(-) diff --git a/docs/status/RECON-OBLIGATIONS-2026-10-29.adoc b/docs/status/RECON-OBLIGATIONS-2026-10-29.adoc index 100602a..ae078d9 100644 --- a/docs/status/RECON-OBLIGATIONS-2026-10-29.adoc +++ b/docs/status/RECON-OBLIGATIONS-2026-10-29.adoc @@ -40,7 +40,15 @@ be checked against pinned CI before upgrading any `REPORTED` status to a mutation lacks a proof, `execute_insert/update/delete` uses `{:ok, []}`. This is an *integration contract gap*, not a VCL-UT theorem. -== Safety level matrix +== Current VCL-UT gate matrix (NOT a ceiling on type systems) + +This L0–L10 is the existing, fixed *VCL-UT query safety / wire +compatibility* numbering. It is NOT the Kategoria 1–10 language-feature +taxonomy, is NOT the TypeLL 1–10 property numbering, and does NOT mean that +VCL-UT as a research programme ends at epistemic safety. The matrix below +is an audit of *today's certified decision predicates and their source +reachability*, not a catalogue of the strongest types VCL-UT may eventually +express. `Proved` here means proof of the *specified predicate* as reported in the checked Idris2 corpus, NOT the colloquial force of a level's name. @@ -69,6 +77,59 @@ VeriSimDB parser supports PROOF syntax not accepted by this gate. L7–L10 may be reachable by constructing `Statement` values through other interfaces; this is not evidence that ordinary source reaches them. +== Kategoria and the open-ended advanced-type programme + +The actual reference is +https://github.com/hyperpolymath/kategoria[Kategoria], especially +`README.adoc`, `ROADMAP.adoc`, +`routes/alpha-extend/README.adoc` and +`routes/delta-aggregate/TYPELL-BRIDGE.adoc`. +Kategoria's first ten *type-theoretic capabilities* are basic types, +ADTs, polymorphism, type classes, GADTs, dependent types, linear types, +refinements, session types, and cubical/homotopy types. These are +*not* VCL-UT safety levels. Its ten items are a first working taxonomy, +not a theorem establishing that all type systems fit one total chain. + +The TypeLL bridge explicitly documents the collision between the +Kategoria level numbers and TypeLL's distinct, query-oriented safety +numbers. In VCL-UT the compatibility-critical gate levels are *L0–L10*, +with `L10 EpistemicSafe`; in Kategoria `L10` concerns cubical types. +The similarity of ordinal names does not imply equal meanings, +correspondence, or capability. Crosswalks must map actual mechanisms to +specific proof obligations, with no inferred one-to-one alignment. + +Kategoria tests five research routes: alpha (extend Idris2), beta +(dyadic type-checker split), gamma (independent checking aspects), delta +(cross-language/prover bridge) and epsilon (new unified calculus). +Its documented cubical wall is specific to route alpha's Idris2/QTT +foundation, not a proof of universal impossibility. Its candidates for +work *beyond the first ten* include graded, effect, modal, directed, +capability, observational-equality, sized and gradual types. Some +are orthogonal alternatives or different kinds of guarantee rather +than numerically ordered successors. No future Kategoria or VCL-UT +L11+ wire tags are defined here. + +[cols="2,3,3",options="header"] +|=== +|Advanced mechanism |Potential independent VCL-UT application |Required evidence before claiming protection +|Graded / quantitative / linear types |State-indexed consumption budgets, evidence or authority attenuation |Preservation across parsing, lowering, runtime and retries; no resource duplication +|Algebraic effect and capability types |Authority- and effect-indexed admissibility for mutations, verification and federation |Actual operation effects and principal permissions must refine the declared type/effect context +|Session, choreographic and directed types |Typed multi-party operations, merge/split/federation protocols |Protocol projection, non-forgeable identities, execution fidelity and failure semantics +|Modal, temporal and epistemic types |Separate belief, verification, knowledge, disclosure and time-indexed evidence |Explicit sound warrants, independent evidence, trusted clock/source and authenticated provenance +|Cubical / higher-dimensional / observational equality |Investigate identity-preserving equivalence and transport across representations |Specify identity/equivalence model and prove bridge correctness in an appropriate kernel; do not equate isomorphism with factual identity +|Sized / total and gradual typing |Terminating proof sublanguages; guarded typed/untyped consumer interoperability |Decidable elaboration or runtime blame/error safety with explicit unchecked regions +|=== + +Research progression is therefore an *open, multi-axis assurance +programme*, not simply 'pass L10, then increment the level number'. +Each proposal needs a typed source construct, semantics, decidable or +bounded checker where applicable, a proof statement and assumptions, +source-to-IR preservation, independent runtime enforcement (or an +explicit external-evidence contract), and a negative test. +The existing normative L0–L10 discriminants remain stable. Any future +extensions must be independently specified and versioned, with no +silent reinterpretation of old safety levels. + == Proof-obligation register Status key: `REPORTED` = named Idris proof/CI gate exists; not @@ -159,7 +220,10 @@ P2 (cross-language / theorem reuse): establish checker correspondence beyond golden fixtures, schema-binding and TOCTOU invariants, evidence authentication, provenance descent, causal witness independence, and Grade/session preservation. Consider ProofTransport and JanusKey as -first proof bridge experiments, with actual assumptions exposed. +first proof bridge experiments, with actual assumptions exposed. Map +these against Kategoria's five alternative routes and TypeLL's +mechanism/property bridge; the existing VCL-UT L0–L10 matrix is only a +current implementation slice, NOT the extent of research into high-end types. P3 (maturity): incremental check caching keyed by versioned schema, subject identity, operation, evidence hash and verifier version, From eba12543a5ebe5dec124e1f95863795d6ffd125a Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 29 Oct 2026 22:46:52 +0000 Subject: [PATCH 2/4] docs(research): frame multi-space identity and type/trope distinctions without claiming equivalence --- docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc | 182 ++++++++++++++++++ 1 file changed, 182 insertions(+) create mode 100644 docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc diff --git a/docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc b/docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc new file mode 100644 index 0000000..b840033 --- /dev/null +++ b/docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc @@ -0,0 +1,182 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Research direction: types, tropes and identity across spaces +:toc: +:sectnums: + +Status: PROPOSAL / reconnaissance, 2026-10-29. This document does not +modify the normative L0–L10 safety levels, the source grammar, or the +VCLW/VCLS/VCLT wire contracts. It proposes a separate programme for +VCL-UT as an independent language and admission system, not as a +Hypatia-specific frontend. No type–trope equivalence or general +triangulation theorem is claimed. + +== Core question + +A subject can have representations, occupy roles, hold capabilities, +instantiate properties, participate in protocols, persist through time +and be described by different witnesses. These are not one kind of +identity claim. Their legitimate operations, equivalence criteria, +evidence and proof obligations can differ. The relevant research +question is: **when may a proposition or transition cross between +those spaces without conflating distinct identities or inventing +authority, evidence or preserved particularity?** + +Do not equate: + +* equality of values with numerical identity of particulars; +* equality of type inhabitants with identity of bearers; +* structural compatibility with authority to occupy a role; +* membership of a protocol state with permission to act; +* identical observations with identical origins; +* two compatible witnesses with causally independent witnesses; +* retrieval, interpretability or loss-relative licensing with real-world truth; +* two presentations meeting a sortal criterion with an unconditional, + global equivalence relation. + +Type formalisms *can* encode individual records and intensional +distinctions; tropes *can* have rigorous operations and checkers. +The distinction is about what a judgement asserts and its evidence, +not that one side is mathematics and the other is metaphor. + +== Separate objects, not assumed equivalences + +[cols="2,3,3",options="header"] +|=== +|Kind of judgement |Example question |Primary existing home +|Typed admissibility / capability |Does the source term inhabit the declared type, and is this effect or resource use allowed? |Kategoria, TypeLL, VCL-UT +|Particularity / bearer |Is this the *same situated property-instance*, preserving bearer, context and history under a transformation? |trope-particularity-workbench, trope-checker, Haec +|Storage / warrant-relative use |What is stored, what did a transformation lose, and does the use-specific floor license this invocation? |Vocarium + Hermeneia +|Sortal identity across presentations |What *criterion of identity and counting* lets us identify these as the same argument? |invariant-path (sortal layer, accepted ADR-0001) +|Epistemic standpoint |Who has which proof-relevant evidence, and what extra soundness premise makes it a factive warrant? |epistemic-types, residual-evidence-types +|Information-loss / representation |Which origins remain compatible after projection? |echo-types +|Live resource occupancy |What is the maximal live-state footprint under concurrency and reclamation? |occupancy-types +|Institutional/role occupancy |Which occupant can legitimately exercise which normative position at time t? |Separate research obligation; NOT implied by occupancy-types' memory model +|Temporal / provenance identity |What still exists, what survives a merge or split, and which provenance descendants exist? |VeriSimDB lifecycle; VCL-UT's current transition obligations +|=== + +In particular, `occupancy-types` currently concerns resource/high-water-mark +occupancy. It should not be silently treated as a proof of legitimacy +for occupants of institutional positions. + +A possible *research* judgement (notation illustrative, NOT an existing +VCL-UT syntax or new type constructor) is: + +---- +Γ ; sortal S ; context C ; time t ; evidence E + ⊢ representation r : T + ⊢ particular p borne-by b in C + ⊢ bridge(r,p) : admissible under obligation O and warrant E +---- + +The bridge is a *partial and potentially many-to-many, direction-sensitive +relation*, not an assumed coercion or equivalence. A concrete bridge +must say exactly what it preserves and what it forgets, and name the +sortal and observer when identity claims are involved. A sortal may +supply criteria of identity and counting without being identical to +a type or a trope. + +== Wider type-discipline estate: sampled implementation status + +The first ten Kategoria *type-feature* labels and the VCL-UT +*query-safety* L0–L10 labels use different numberings. Neither caps +VCL-UT research. `echidna/docs/architecture/TYPE-DISCIPLINE-EMBEDDING.adoc` +registers a larger set of disciplines; its detector and dispatch are +not themselves formal enforcement receipts. + +[cols="2,3,3",options="header"] +|=== +|Discipline / cluster |Evidence inspected |Potential VCL-UT role and unproved gap +|Parametric polymorphism |Kategoria `routes/alpha-extend/Level03_Polymorphism.idr`; TypeLL |Reusable generic inference; formal free-theorem/parametricity obligations differ from mere polymorphic syntax +|Phantom / indexed / nominal |Ephapax phantom examples; ECHIDNA taxonomy; Kategoria GADTs and dependent types |Distinguish unforgeable subject or schema tags and typed identities; phantom labels alone do not authenticate a subject +|Immutability / uniqueness / affine / linear |ECHIDNA taxonomy; Ephapax; Idris2 QTT |Versioned state and resource ownership; distinguish immutable value, binding, reference, snapshot and persistent historical identity +|Dyadic |Ephapax linear/affine architecture; Echo `Dyadic.agda`; KitchenSpeak's tensor/binding example |Do not merge unrelated dyadic meanings: two-party interaction, two-mode usage, and irreversible material binding have different properties +|Ceremonial / contextual |KitchenSpeak `COMMENTARY.adoc` contextual/ambient effect semantics; ECHIDNA `Ceremonial` detector but no dedicated ProverKind |Context-qualified protocol obligations, role permission and social pacing; no general VCL-UT ceremonial checker exists +|Echo / epistemic / residual evidence |Independent Agda projects with scoped formal cores |Identity fibres, evidence and witness/non-identification; require source-to-checker and real-world warrant bridges +|Tropical / graded / choreographic / occupancy |Dedicated Lean/Agda formal models and resource algebra; `occupancy-types` operational model |Distinct cost, occupancy and trace semantics; no implicit exchange of resource measures +|Secret / capability / effect / session |secret-types noninterference fragment; ECHIDNA taxonomy; TypeLL |Prove actual allowed flows, effects, protocol transitions, privileges and declassification conditions +|Sortal criteria / representation |invariant-path ADR-0001 and its recorded open proof debt |Check whether a presentation is the same argument under a stated sortal; formal move/quotient/equivalence certificate is not yet established +|Trope particularity / graded transformation |trope-checker calculus and checked honesty fragment; Haec lowering design |Loss-relative use judgments are formal, but faithful lowering and real-world veridicality remain independent obligations +|=== + +No claim is made that this is an exhaustive type taxonomy. Additional +candidates include higher-kinded, row, intersection, union, relevant, +ordered, bunched, refinement, Hoare, sized, gradual, cubical, +modal, deontic and observational-equality formalisms. Entries +must be classified by *mechanism*, *judgement*, *space*, *proof*, and +*operational enforcement*, not pushed into an invented L11+ ordering. + +== The trope programme is already formal, not decorative + +`trope-checker` has a typed IR and graded operation calculus with +Idris2 reference checking; its Agda `TB.Honest` development shows that +the specified honest constructors/composition do not generate +deceptive grades. `Haec` records separate lowering-correctness +obligations (O2). The October 2026 stack status identifies the +workbench as vocabulary/specification, Haec as design, and Vocarium +and Hermeneia as partial executable slices. Thus a theorem about +the grade algebra is **not** a theorem that a particular real input +was faithfully represented or that a received claim is true. + +`invariant-path`'s accepted sortal ADR provides a useful distinct +third task: determining whether two presentations are the *same* +argument under specified identity criteria. Its ADR also explicitly +reports missing equivalence-certificate machinery. Do not call this +a completed triangulation theorem. A general construction of +types ↔ tropes ↔ sortals has not been located in the inspected +repositories, so the relationship remains a research question. + +== Candidate proof obligations + +[cols="1,3,4",options="header"] +|=== +|ID |Claim to prove, with its assumptions |Needed implementation evidence +|X-01 |Lowering preserves the stated type judgement, and every runtime operation refines the typed effect/resource judgement |Typed source → IR → actual executor, negative controls +|X-02 |A type tag or schema equality cannot forge numerical subject identity, provenance or principal authority |Authenticated identity/sortal comparator, counterexamples +|X-03 |A declared trope transformation's IR grade soundly bounds its actual particularity loss |Per-construct faithful-lowering proofs and a declared observation model +|X-04 |If a sortal reports same identity under an allowed transition sequence, every permitted intermediate move preserves that sortal's invariant |Formal move relation and composition certificate or obstruction, not just hash equality +|X-05 |A position does not confer legitimacy on its occupant; authority is conditioned on independently valid occupancy evidence and interval |Institutional occupancy judgement + consumer enforcement +|X-06 |A proof receipt cannot upgrade mere claim/evidence to factive knowledge without an explicit sound-warrant premise |Bridge to epistemic-types' `SoundWarrant` / ProofTransport +|X-07 |A merge or split retains exactly its declared number and ancestry of particulars; honest fusion is distinguishable from conflation |Trope merge grades + provenance identity transition model + counterexamples +|X-08 |Combined typed and trope verdicts do not imply one another; each can fail while the other succeeds |Independent acceptance/rejection fixtures, and a formal independence proof where models allow +|X-09 |The same identity may be represented across multiple modality/role/time charts without illicit equality or a fabricated global clock |Chart-indexed witnesses, explicit partial maps, time and causal-order premises +|=== + +These are *open obligations*, not statements of proved results. +An inability to prove one under current assumptions should be +reported by its missing premise or countermodel. + +== Sensible staged programme + +. **Vocabulary and discovery (now).** Publish an extensible, + source-anchored, theorem-aware index of type disciplines and + identity/particularity judgements; incorporate Mathesis and + `nextgen-typing` rather than copying large cross-estate inventories. + Record `PROVEN`, `TESTED`, `MODEL-ONLY`, `SPECIFIED`, `OPEN` + separately. The old L0–L10 safety matrix remains intact. +. **Small proof bridge.** Propose a single carefully scoped + identity–particularity use case: two schema-compatible records, + distinct particulars, and an attempted MERGE. Test that static + compatibility alone cannot license an identity conflation and that + an explicit, appropriately warranted fusion can be represented. + Do not assume all types/tropes have a common equivalence. +. **Source and runtime obligations.** Give the new checks explicit + source forms only when their operational semantics, authority and + evidence contracts are specified. Keep transition admission and + commit permission separate; make the consumer fail closed. +. **Type-family graduation.** Add independent plugin/discipline + boundaries and proof receipts for the families that genuinely add + guarantees. When formal modelling requires a different prover, + establish and review the bridge instead of labelling a heuristic + detector a theorem. +. **Only then broader ontology.** Evaluate partial maps and + context-relative identity across additional semantic, spatial, + temporal, social, normative and evidential spaces. A claim + crossing spaces must preserve exactly the invariants stated in its + certificate, never a universal identity promised by default. + +VCL-UT owns its language/admissibility design and proof obligations; +Mathesis inventories theorem evidence; Kategoria/TypeLL research and +implement type mechanisms; Haec/Vocarium/Hermeneia and trope-checker +own situated particularity, use and loss. Shared work requires reviewed, +versioned interfaces without changing ownership or collapsing +these independently meaningful objects. From 39f9ace77fd803ced2fbc493daa7f0c34ee0890f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 29 Oct 2026 22:47:02 +0000 Subject: [PATCH 3/4] docs(recon): link independent type-trope identity-spaces programme --- docs/status/RECON-OBLIGATIONS-2026-10-29.adoc | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/docs/status/RECON-OBLIGATIONS-2026-10-29.adoc b/docs/status/RECON-OBLIGATIONS-2026-10-29.adoc index ae078d9..89562b1 100644 --- a/docs/status/RECON-OBLIGATIONS-2026-10-29.adoc +++ b/docs/status/RECON-OBLIGATIONS-2026-10-29.adoc @@ -120,6 +120,13 @@ L11+ wire tags are defined here. |Sized / total and gradual typing |Terminating proof sublanguages; guarded typed/untyped consumer interoperability |Decidable elaboration or runtime blame/error safety with explicit unchecked regions |=== +For the separate ontological and language-design implications of type +families, tropes, sortal identity, occupancy, and identity across +context/time/modality spaces, see +link:../research/TYPE-TROPE-IDENTITY-SPACES.adoc[Types, tropes and +identity across spaces]. That research direction does *not* assume a +proved equivalence, triangulation, or universal coercion between them. + Research progression is therefore an *open, multi-axis assurance programme*, not simply 'pass L10, then increment the level number'. Each proposal needs a typed source construct, semantics, decidable or From 245e7f8504828d4c27cf72f69aaeccf923bd67f8 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 29 Oct 2026 22:48:54 +0000 Subject: [PATCH 4/4] docs(research): add synchronic/diachronic identity probes without prescribing a single architecture --- docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc | 77 +++++++++++++++++-- 1 file changed, 71 insertions(+), 6 deletions(-) diff --git a/docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc b/docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc index b840033..88cf992 100644 --- a/docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc +++ b/docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc @@ -3,12 +3,15 @@ :toc: :sectnums: -Status: PROPOSAL / reconnaissance, 2026-10-29. This document does not -modify the normative L0–L10 safety levels, the source grammar, or the -VCLW/VCLS/VCLT wire contracts. It proposes a separate programme for -VCL-UT as an independent language and admission system, not as a +Status: EXPLORATORY RESEARCH CONTEXT / reconnaissance, 2026-10-29. +This document does not modify the normative L0–L10 safety levels, +the source grammar, or VCLW/VCLS/VCLT wire contracts. It explains +questions motivating several independent language/database experiments, +not a selected architecture or ordered implementation mandate. +VCL-UT remains its own language/admission research system, not a Hypatia-specific frontend. No type–trope equivalence or general -triangulation theorem is claimed. +triangulation theorem is claimed. Its proposed judgements and work items +are candidates, not architectural decisions. == Core question @@ -38,6 +41,60 @@ distinctions; tropes *can* have rigorous operations and checkers. The distinction is about what a judgement asserts and its evidence, not that one side is mathematics and the other is metaphor. +== The motivating problem, not a predetermined solution + +The owner is exploring **identity and equivalence**, including *synchronic* +questions (what agrees or counts as the same at a given observational +cut?) and *diachronic* questions (what survives change of +representation, algorithm, record, history and authority over time?). +Different systems are intentionally different probes of this question. +Nothing requires one global identity type, common coercion language, +a total hierarchy of kinds of space or a grand unified calculus. + +Crucially, *equivalence under a chosen relation* is not automatically +*identity through a history*. A static equivalence relation can +identify two presentations at one boundary, while a transition +requires a directed, evidence-bearing account of what persisted, +what was intentionally changed, which commitments survived and who +had authority at each point. Conversely, a continuing service may +change its future decisions without breaking a narrower contract +of identity. Proof of either judgement must name its criteria. + +[cols="2,2,3,3",options="header"] +|=== +|Independent project |Identity or equivalence lens |Source-grounded example |Known limit +|https://github.com/hyperpolymath/firmboot[Firmboot] |Diachronic continuity through live implementation change |Its `PURPOSE.md` explicitly separates synchronic state/history/authority coherence from diachronic observation order, commitments and migration. `SPEC.md` fixes episode IDs and activation ownership |Proved model contracts for known detector versions, not universal equivalence or actual hardware uptime; model-to-live refinement remains open +|https://github.com/hyperpolymath/lithoglyph[Lithoglyph] |Persistent, reversible and audited database history |Journals, migration artefacts, provenance and schema/version changes remain first-class narrative records |Durability, reversal and versioning alone do not establish numerical identity across arbitrary transformations +|https://github.com/hyperpolymath/gnpl[GNPL] |Identity of an evidence-grounded account as its evidence and focalisation evolve |Its `docs/THEORY.adoc` distinguishes a projection at time t from the history of changing projections; withdrawal may retract claims and a checked account is indexed by an evidence snapshot |Current kernel handles versioned evidence and withdrawals but lacks a general event-identity/partial-order temporal semantics (`docs/STATE-OF-PLAY.adoc`) +|https://github.com/hyperpolymath/tangle[Tangle] |Structural equivalence by admissible transformations |General braid/knot language where program equivalence is interpreted through isotopy and loss-bearing closure has an Echo-like account |A domain-specific equivalence model; it does not automatically specify identity for people, records or institutions +|https://github.com/hyperpolymath/quandledb[QuandleDB] + https://github.com/hyperpolymath/krl[KRL] |Distinguish possible matches, invariants and certified equivalence |Stored knot presentations and invariants yield candidates; intended resolution questions include witnessed isotopy and equivalence |The current `find_equivalent` gives heuristic candidates; `find_path` does not give a checked Reidemeister path; KRL's full resolution proof obligations remain open +|https://github.com/hyperpolymath/invariant-path[Invariant Path] |Sortal identity across presentations |Separate well-formedness, use-relative warrant and identity/counting; its double-counting attack shows why two apparently independent presentations may be one argument |The three-layer design is accepted, but proof-carrying equivalence/obstruction machinery is not yet implemented +|=== + +The distinctions offer **tests of any eventual theory**, not inputs that +must all be incorporated into VCL-UT. Some useful questions are: + +* Can two different presentations be equivalent under a named + observer/sortal yet retain separate provenance or numerical identities? +* Can a single subject persist over time even when its representation, + behaviour, effective authority or attached claims change? Which parts + of its history are non-negotiable? +* If account A was warranted at t1 and later retracted at t2, what is + the identity of the *account*, the *claim* and the *evidence*? How + are event time, admission time and knowledge-revision time separated? +* When a path is missing, do we mean not-equivalent, no proof found, + insufficient evidence, forbidden transformation or the relation is + not even defined? These are materially different outcomes. +* Under what circumstances can multiple views count as independent + corroboration, rather than duplicated presentations of one witness? + +These questions also connect back to the independent type disciplines: +linear/affine/immutable/phantom types can maintain tokens or versions; +epistemic and residual-evidence types can expose what a view warrants; +trope grades can report alteration of situated particularity; and +session/choreographic/dyadic types can constrain transitions. None +of those mechanisms, individually, settles the general identity question. + == Separate objects, not assumed equivalences [cols="2,3,3",options="header"] @@ -145,7 +202,15 @@ These are *open obligations*, not statements of proved results. An inability to prove one under current assumptions should be reported by its missing premise or countermodel. -== Sensible staged programme +== Possible experiments (not an agreed sequence) + +The following order reflects low-risk experiments *if* VCL-UT adopts +this line of research. It should not be interpreted as committing +Firmboot, GNPL, Tangle, QuandleDB, KRL, Haec, Vocarium or Hermeneia +to VCL-UT's architecture, or as requiring an all-purpose identity +calculus before doing local correctness work. + +=== Earlier draft: a staged programme . **Vocabulary and discovery (now).** Publish an extensible, source-anchored, theorem-aware index of type disciplines and