Tarski.lean provenance record: drafting and review process (who produced which claim)
type: Nanopublication
has assertion: assertion
has provenance: provenance
has publication info: pubinfo
created: 2026-08-10T12:57:30Z
creator: https://orcid.org/0000-0002-8042-4131
license: https://creativecommons.org/licenses/by/4.0/
verification bucket: ProcessProvenance

First attempt via a bare messages.create() API call (claude_convo_.py, no tools bound)
type: Activity
qualified attribution: attr-bare-api-validation
used: User specifies the five-step provenance protocol and, on request, the repo URL for Tarski.lean
was associated with: Claude Sonnet 5 (Anthropic Messages API, no tools)
outcome: No machine- or source-verified content was produced by this activity. Superseded by d:activity-claude-code-session below, which had actual tool access.
produced claim: Explicit refusal to fabricate hash/ISCC/compilation/concordance results, on the grounds that no tools were available in that call; produced only a negative-space accounting, itself truncated at max_tokens=16000 before completion.

Claude Code session: retrieval, compilation, axiom audit, grounding, and nanopublication drafting
type: Activity
generated: activity-ground
generated: activity-negative-space
generated: activity-retrieve-execute
generated: activity-separate
qualified attribution: attr-session-investigation
qualified attribution: attr-session-software
qualified attribution: attr-session-validation
qualified attribution: attr-session-writing
was associated with: Claude Sonnet 5 (Anthropic), running as Claude Code
was informed by: First attempt via a bare messages.create() API call (claude_convo_.py, no tools bound)

User specifies the five-step provenance protocol and, on request, the repo URL for Tarski.lean
type: Activity
qualified attribution: attr-request-conceptualization
qualified attribution: attr-request-supervision
was associated with: Myles Axton

User reviews NP-A through NP-E before any signing or publication
type: Activity
qualified attribution: attr-review-supervision
was associated with: Myles Axton
status: Pending at the time NP-E was drafted -- this activity node is declared in advance of its own completion, and its outcome (approved / revised / rejected) is not yet an assertable fact. See NP-D for the general rule that unsigned, unpublished status holds for this entire set.

Claude Sonnet 5 (Anthropic Messages API, no tools)
type: SoftwareAgent
has capability: text generation only -- no file access, no shell, no network fetch, no Lean toolchain

Claude Sonnet 5 (Anthropic), running as Claude Code
type: SoftwareAgent
has capability: Bash, file read/write, WebSearch, and an installed elan/Lean 4.32.0 toolchain

Myles Axton
type: Person
acted on behalf of: https://orcid.org/0000-0002-8042-4131

NP-A (machine-verified): hashing, ISCC, compilation, axiom audit
type: ClaimSet
qualified attribution: attr-session-investigation
qualified attribution: attr-session-software
was generated by: activity-retrieve-execute

NP-B (source-verified): license, authorship, historical citations, concordance spot-check
type: ClaimSet
qualified attribution: attr-session-investigation
was generated by: activity-ground

NP-C (asserted): self-reported claims quoted but not independently verified
type: ClaimSet
qualified attribution: attr-session-writing
was generated by: activity-separate

NP-D (negative space): explicit non-claims
type: ClaimSet
qualified attribution: attr-session-writing
was generated by: activity-negative-space

NP-E (this record): the drafting/review provenance graph itself
type: ClaimSet
qualified attribution: attr-session-writing
was generated by: Claude Code session: retrieval, compilation, axiom audit, grounding, and nanopublication drafting

assertion
description: This graph is a first-person account of the session's own activities and is therefore self-attested by the same agent (d:agent-claude-sonnet-5) that performed them, checked against no external source -- it is provenance about provenance, not a claim about Tarski.lean itself.
was generated by: Claude Code session: retrieval, compilation, axiom audit, grounding, and nanopublication drafting

sig
has algorithm: RSA
signed by: https://orcid.org/0000-0002-8042-4131