diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 1a324e8..379317f 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -1,81 +1,85 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= AFFIRMATION — Hermeneia, as of += AFFIRMATION — Hermeneia, as of 2026-10-27T07:50Z :toc: macro :toclevels: 2 _the No-Bullshit file: what we affirm was true and checkable at this moment._ -[NOTE] -==== -*This file is a template.* Replace the `{{…}}` placeholders and the `<…>` anchor -fields, then re-run your project's own checks in the same session before signing. - -An *affirmation* is a solemn declaration of the truth of a statement, made by -someone who _declines to swear an oath_ — our truth-as-best-believed at a stamped -instant, binding on our honesty, not a claim of infallibility. It is the third of -the README / EXPLAINME / AFFIRMATION trio: - -[cols="1,3,2",options="header"] -|=== -| File | Answers | Tense -| `README.adoc` | _Where is this going, and why?_ — steering, intent, vision | future / aspirational -| `EXPLAINME.adoc` | _How is it built, and what's the evidence?_ — engineering | descriptive / mechanism -| *`AFFIRMATION.adoc`* (this file) | _What can we honestly affirm was *true and checkable* at a stamped moment?_ | a frozen instant, falsifiable -|=== -==== - toc::[] == What this is, and how it works -*What it is.* A short, dated, signed snapshot of what hyperpolymath can honestly and -verifiably claim about *Hermeneia* at one exact commit. Nothing here is -marketing and nothing is a promise about the future — those live in the README. -This file is the receipt. - -*How it stays trustworthy.* Three moving parts: - -. *Ground truth, not memory.* Every claim below must be produced by _running the - project's own checks_ in the session that writes this file (build, tests, - typecheck, `just audit`). Where a status doc, the `Justfile`, or memory says - otherwise, the live run wins and the contradiction is flagged here. -. *A frozen anchor.* The file names the exact commit SHA, branch, UTC timestamp, - and toolchain (see <>), so "true" always means "true _at - this point_". Move the SHA and this file is a draft until it is re-run. -. *A real signature.* It is landed by a *signed git commit*; that signature over - this content at the anchored SHA is what makes the affirmation tamper-evident - and attributable — not the prose alone. - -*We are fallible.* This is our best honest belief, not a proof of its own -correctness. Treat it as a falsifiable claim, not gospel. - -== The epistemic contract (read this before you trust _or_ attack) +A short, dated, signed snapshot of what hyperpolymath can honestly and verifiably +claim about *Hermeneia* at one exact commit. Nothing here is marketing or a +promise; those live in the README. This file is the receipt. Every claim below +was produced by running the project's own checks in the session that wrote this +file; the anchor (<>) names the commit, time and toolchain, so +"true" means "true at this point". It is to be landed by a signed commit — the +owner signs on landing. -This document records hyperpolymath's *best belief* at the timestamp below. It is -*not a guarantee of correctness.* The only guarantee is *no intentional -overclaim*: where something is proven we say "proven"; where it is a documented -trust boundary, an experiment, or an unwired module, we say so; where a claim is -the README's aspiration rather than a checked result, we say so. An honest claim -that later turns out false is an *error to be fixed* — not a lie. +== The epistemic contract -*Standing invitation to refute.* You are invited to bulldoze any claim in this -file. Bring a counter-example, a failing run, or a contradicting source. +This records hyperpolymath's best belief at the timestamp below, not a guarantee +of correctness. The only guarantee is no intentional overclaim: proved is called +proved, a trust boundary is called a trust boundary, an unimplemented verb is +called unimplemented. You are invited to refute any line with a counter-example, +a failing run, or a contradicting source. -== What we affirm (fill in — delete the examples) +== What we affirm [cols="2,1,3",options="header"] |=== -| Claim | Status | Evidence (command / `file:line`) -| _e.g. The library builds clean_ | affirmed | `just build` at the anchor SHA -| _e.g. The ABI seam typechecks_ | affirmed | `idris2 --typecheck abi.ipkg` -| _e.g. Feature X is complete_ | aspiration | README §… (not yet checked) +| Claim | Status | Evidence (command / file) + +| The workspace builds and its tests pass: 39 tests — hermeneia-cli's `gate` +integration target 4, hermeneia-store 8, hermeneia-ir 11, hermeneia-core 7, +hermeneia-syntax 9 (the fifth crate, hermeneia-cli, has no unit tests of its own). +| affirmed +| `cargo test --workspace` at the anchor → 39 passed, 0 failed, 4 s. + +| `invoke` works end to end against the trope-checker — its Rust fast core +`tropecheck-rs`, conformance-validated against the Idris2 reference, not the +reference binary itself: the README example's +query, reduced to `show verdict` (the README's `show verdict, loss, warrant` is +refused at `show loss`), yields `p-insufficient` with the expected witness edge; +the same particular is licensed (`p-sufficient`) under the permissive use-model; +the emitted IR carries the required top-level keys and is accepted as well-formed +by that checker (schema validation at the trust boundary). +| affirmed +| `HERMENEIA_TROPECHECK=/path/to/tropecheck-rs cargo test -p hermeneia-cli --features e2e --test slice` +→ 7 passed (`src/hermeneia-cli/tests/slice.rs`). + +| Refusals are honest, not fabricated: `show loss` is refused rather than +invented; the unimplemented vokes are reported as unimplemented, distinct from +syntax errors (`evoke` through the CLI in the slice; all six keywords at the +parser in `hermeneia-syntax::other_vokes_are_unimplemented_not_syntax_errors`, +part of the workspace run); a missing checker exits 3 with instructions. +| affirmed +| the same slice run (`show_loss_is_refused_rather_than_fabricated`, +`unimplemented_vokes_are_distinguished_from_syntax_errors`, +`missing_checker_exits_three_with_instructions`). + +| Verdicts come from the trope-checker, never from Hermeneia: the e2e slice +drives the Rust fast core, and the verdict semantics are the checker's. +| trust boundary +| `HERMENEIA_TROPECHECK`; `docs/SPEC.adoc` "Status — no overclaim". |=== == What we do NOT claim -* List the known gaps, trust boundaries, postulates, unwired modules, and stale - docs here. Silence is not affirmation — name what you have *not* verified. +* `evoke`, `convoke`, `transvoke`, `provoke`, `intervoke`, `revoke` — recognised by + keyword and refused as unimplemented (their bodies are not parsed); the refusal is + what is tested (`docs/SPEC.adoc`). +* `show loss` and `show warrant` — refused (`hermeneia-core::plan_invoke`); the first + needs the checker's loss vector, the second the warrant graph. `show failure_points` + is parsed but *not* refused by the planner — the request proceeds to the checker — + although `docs/SPEC.adoc` lists it as refused; that line is stale (finding, not fixed + here). +* Nothing is Integrated: the store is a stub (`hermeneia-store`), the Vocarium + `StoreProvider` adapter (M2) does not exist yet. +* No proofs of our own: the grade algebra is the checker's, machine-checked + there (`trope-checker/docs/status/PROOF-STATUS.adoc`), cited not restated. [#verifiable-anchor] == Verifiable anchor @@ -84,12 +88,13 @@ file. Bring a counter-example, a failing run, or a contradicting source. |=== | Project | Hermeneia | Repository | https://github.com/hyperpolymath/hermeneia -| Commit (SHA) | -| Branch | main -| Timestamp (UTC) | -| Toolchain | -| Affirmed by | Jonathan D.A. Jewell +| Commit (SHA) tested | 21b15931b3b93c6de9e5b536e20401336825f26b (`main` at the time; the tree the commands ran against) +| Landing commit | the signed commit that lands this snapshot on `main` (the file itself predates it as a template); after landing, `git log --first-parent --show-signature -1 main -- AFFIRMATION.adoc` selects it. A file cannot record its own commit's SHA +| Timestamp (UTC) | 2026-10-27T07:50Z +| Toolchain | rustc 1.97.0 (2d8144b78 2026-07-07), cargo 1.97.0; checker `tropecheck-rs` built with `cargo build --release` from trope-checker 44020f9 (= `main` 216f23b plus the two Phase 0 spec/CI patches, which do not touch `src/rust`); Ubuntu 24.04 cloud container +| Affirmed by | Jonathan D.A. Jewell (owner signs on landing; run by the Phase 0 agent) |=== -_Landed by a signed git commit. Verify with `git log --show-signature` that the -anchor SHA above matches the commit that introduced this affirmation._ +_To be landed by a signed git commit. The "Commit (SHA) tested" row is the base the +checks ran on; verify the landing commit and its signature with +`git log --first-parent --show-signature -1 main -- AFFIRMATION.adoc`._ diff --git a/README.adoc b/README.adoc index dce2046..a9fa280 100644 --- a/README.adoc +++ b/README.adoc @@ -51,6 +51,8 @@ To **voke** is to call a stored particular into a use-relation. | `intervoke` | call between trope paths or candidates | | `revoke` | call back or withdraw a previous licence | +Implemented end-to-end and tested: `invoke`. The other six are recognised by keyword and refused as unimplemented (their bodies are not parsed) — status table in `docs/SPEC.adoc`. + Hermeneia does not select rows. Hermeneia vokes tropes. @@ -134,6 +136,10 @@ because warrant "source_check_failed" This withdraws a previously licensed answer when its warrant, evidence, or use-model no longer holds. +## Where this repo sits + +Vocabulary track: trope-particularity-workbench → haec → trope-checker (verdict). Store/query track: haec → vocarium → hermeneia → trope-checker (verdict). trope-checker depends on nothing (HC-1); the workbench depends on nothing; vocarium and hermeneia meet at the M2 StoreProvider adapter (vocarium ADR-0002: wire, do not link). + ## Relationship to Vocarium Hermeneia queries **Vocarium**, the database of vokeable particulars. diff --git a/docs/THEORY.adoc b/docs/THEORY.adoc index caad33e..f92aa8d 100644 --- a/docs/THEORY.adoc +++ b/docs/THEORY.adoc @@ -8,7 +8,7 @@ [abstract] == Abstract -Every deployed query language answers one question — _which stored items match?_ — and leaves two others unasked: _can this item be meaningfully read in the present context?_ and _is the use licensed, given what has been lost between the original record and the item in hand?_ In practice the three collapse into one, and the collapse has a cost: in evidential reasoning and AI-assisted scholarship, "the system retrieved it" is routinely treated as "the system licensed it." This paper presents the theory of Hermeneia, an experimental query language in which the three questions are kept formally distinct. Its semantic core is a small, machine-checked algebra: every transformation of a stored particular carries a six-coordinate _grade_ recording what kind of loss it inflicted; grades compose associatively along transformation paths, the fidelity coordinate by tropical addition over stem:[\mathbb{N}\cup\{\infty,\top\}]; a declared _use-model_ is a partial demand vector — a _floor_ — over the same coordinates; and an answer is _licensed_ (p-sufficient) exactly when the floor lies below the accumulated grade in a componentwise retention order. Licensing thereby becomes a decidable order-theoretic question rather than a matter of judgement. Around this core sit seven _voking_ operations, of which one — `revoke`, licence withdrawal as contraction over a warrant graph — has no analogue in any existing query language known to us. The contribution claimed is the conjunction, not any single ingredient: the trichotomy of retrieved, interpretable, and licensed, made operational in one small algebra. +Every deployed query language answers one question — _which stored items match?_ — and leaves two others unasked: _can this item be meaningfully read in the present context?_ and _is the use licensed, given what has been lost between the original record and the item in hand?_ In practice the three collapse into one, and the collapse has a cost: in evidential reasoning and AI-assisted scholarship, "the system retrieved it" is routinely treated as "the system licensed it." This paper presents the theory of Hermeneia, an experimental query language in which the three questions are kept formally distinct. Its semantic core is a small, machine-checked algebra: every transformation of a stored particular carries a _grade_ — three coordinate kinds, fate (per field), bond, merge, over six slots — recording what kind of loss it inflicted; grades compose associatively along transformation paths, the fidelity coordinate by tropical addition over stem:[\mathbb{N}\cup\{\infty,\top\}]; a declared _use-model_ is a partial demand vector — a _floor_ — over the same coordinates; and an answer is _licensed_ (p-sufficient) exactly when the floor lies below the accumulated grade in a componentwise retention order. Licensing thereby becomes a decidable order-theoretic question rather than a matter of judgement. Around this core sit seven _voking_ operations, of which one — `revoke`, licence withdrawal as contraction over a warrant graph — has no analogue in any existing query language known to us. The contribution claimed is the conjunction, not any single ingredient: the trichotomy of retrieved, interpretable, and licensed, made operational in one small algebra. == Introduction @@ -72,7 +72,7 @@ The stored objects are _particulars_: property-instances in the trope-theoretic carrying respectively the situated quality itself, the entity it is a quality of, the situation individuating it, and an honest provenance of how the record came to be. -Particulars are transformed — paraphrased, projected, compressed, merged — and every transformation carries a _grade_: a record of what it did, in kind and not merely in amount. A grade has six coordinates: +Particulars are transformed — paraphrased, projected, compressed, merged — and every transformation carries a _grade_: a record of what it did, in kind and not merely in amount. A grade has three coordinate kinds — fate (per field), bond, merge — over six slots: [stem] ++++ @@ -134,7 +134,7 @@ The order is decidable: every coordinate is finite except fidelity, which is a d === Use-models, floors, and licensing -Here is the paper's spine. _A use-model is a partial demand vector over the grade coordinates._ Formally a use-model stem:[U] declares a _floor_: a record assigning to each of the six coordinates an _optional_ minimum, +Here is the paper's spine. _A use-model is a partial demand vector over the grade coordinates._ Formally a use-model stem:[U] declares a _floor_: a record assigning to each of the six slots — the four field fates, bond, merge — an _optional_ minimum, [stem] ++++ @@ -260,11 +260,11 @@ Honesty about scope is part of the design, and several limits are structural. *Use-models do not yet revise in time.* `revoke` handles withdrawal of warrants under a fixed population of use-models. It does not address temporal revision of the use-models themselves: what becomes of standing licences when a floor is tightened or a use-model deprecated. The warrant graph gives an obvious purchase — a use-model is a warrant element of every verdict issued under it, so tightening it is a mass degradation — but the semantics of versioned use-models, and of grandfathering versus wholesale re-examination, is open. -Beyond these: whether the six coordinates are complete for particularity-loss is an open question rather than a theorem, and the operational cost of warrant graphs at archive scale is unmeasured. +Beyond these: whether the three coordinate kinds — fate, bond, merge — are complete for particularity-loss is an open question rather than a theorem (calculus O1-coord), and the operational cost of warrant graphs at archive scale is unmeasured. == Conclusion -The argument of this paper is that "the system found it" and "the system licensed it" are different claims, that the difference is precisely the failure mode of AI-assisted evidential work, and that it can be made computable at small formal cost: a six-coordinate graded monoid with a tropical fidelity dimension, a componentwise retention order, and one comparison — stem:[\mathrm{floor}(U) \sqsubseteq \mathrm{acc}(v)] — with a witness on failure. Around that core, a query vocabulary in which retrieval (`evoke`, `convoke`, `transvoke`), licensing (`invoke`, `provoke`, `intervoke`), and withdrawal (`revoke`) are distinct verbs, so that no result carries an endorsement it was never given and no withdrawn licence disappears without trace. None of the ingredients is new. The instrument they assemble — a query language whose answers know what they are licensed to become — is, we believe, new; the experiment worth running is whether practices that adopt the trichotomy stop mistaking retrieval for warrant. +The argument of this paper is that "the system found it" and "the system licensed it" are different claims, that the difference is precisely the failure mode of AI-assisted evidential work, and that it can be made computable at small formal cost: a graded monoid of three coordinate kinds — fate (per field), bond, merge — over six slots, with a tropical fidelity dimension, a componentwise retention order, and one comparison — stem:[\mathrm{floor}(U) \sqsubseteq \mathrm{acc}(v)] — with a witness on failure. Around that core, a query vocabulary in which retrieval (`evoke`, `convoke`, `transvoke`), licensing (`invoke`, `provoke`, `intervoke`), and withdrawal (`revoke`) are distinct verbs, so that no result carries an endorsement it was never given and no withdrawn licence disappears without trace. None of the ingredients is new. The instrument they assemble — a query language whose answers know what they are licensed to become — is, we believe, new; the experiment worth running is whether practices that adopt the trichotomy stop mistaking retrieval for warrant. [bibliography] == References diff --git a/docs/status/STATE-OF-PLAY.adoc b/docs/status/STATE-OF-PLAY.adoc index e011b8b..76a107e 100644 --- a/docs/status/STATE-OF-PLAY.adoc +++ b/docs/status/STATE-OF-PLAY.adoc @@ -195,15 +195,15 @@ call job, which GitHub rejects before creating any job. ones someone had already filled by hand to get CI passing. See <> below. -| Unsigned AFFIRMATION, no CRG grade -| *Still owed, and deliberately not filled in.* `AFFIRMATION.adoc` is an unsigned - template that says so itself in a NOTE block; filling it honestly requires - RUNNING the project's checks in the session that signs it (`cargo test`, - `idris2 --typecheck abi.ipkg`, `zig build`), and none of those toolchains is - available in the environment this work was done in. Inventing an affirmation is - precisely the overclaim the file exists to prevent. `docs/status/READINESS.adoc` - is the same story: the CRG assessment is still blank, so this repo has no - published readiness grade. +| AFFIRMATION filled, unsigned until landing; no CRG grade +| *Update 2026-10-27 (Phase 0, PR #76).* `AFFIRMATION.adoc` is no longer a template: + it was filled from a real run (`cargo test --workspace` 39 passed; the e2e slice + 7 passed against `tropecheck-rs`) at commit 21b1593, with a verifiable anchor and + a do-not-claim list. It is unsigned until the owner signs the landing commit — + that is the owner's act, not this pass's. The earlier state (an unsigned template + that said so in a NOTE block, no toolchain to run the checks) is historical. + `docs/status/READINESS.adoc` is unchanged: the CRG assessment is still blank, so + this repo has no published readiness grade. | ABI/FFI seam is scaffolding | `src/interface/` was inherited from the template and never instantiated.