Prove2Me_workspace epistemic report

Type: agentic-system-analyses/types/agentic-system-epistemic-report.md

Source-and-claim boundary

The question is what this workflow can license agents and humans to rely on: a formal proposition, a faithful rendering of an external source, a conditional reduction, an attested numerical bound, or an extraction fact. Scope and exclusions: see boundary. Evidence identity and layers: see the Source register, SRC-1. The target is the shipped workflow and its two extractors, not the enclosing model runtime or Prove2me backend.

The supplied runtime account is provisional, not an inspection limit. Direct reads below add campaign value attestation, human audit consumption, ranking signals, description edits and collection admission to its route coverage. These are doctrine/design, except for inspected Lean helper implementation. There is no observed-run or causal-experiment layer. No target was executed or service contacted.

Consequential claims: RT-CLM-verification-boundary, RT-CLM-human-gate, and EPI-CLM-graph-truth. The skill's mathematical-guarantee claim does not license informal-source equivalence. The project playbook's graph authority is assessed separately from successful transplant.

Entry point or operation	Source path	Coverage and records	Limit or excluded conclusion
Role dispatch and endpoint index	SRC-1, SKILL.md	Direct full read; RT-OBJ-skill, RT-BAP-role-guidance	Prose dispatch, not implemented CLI/tool/hook registration. No host dispatch was supplied.
Solver scouting, prove/disprove/reduce, poll	SRC-1, references/mission_solver.md, references/prove.md	Direct full reads; RT-RTE-solver-proof, RT-RTE-reduction-proof	Verifier and automatic closure implementation unavailable.
Draft, blind auditor, human launch, moderation, release, live retargeting	SRC-1, references/mission_captain.md, references/mission_auditor.md	Direct full reads; RT-RTE-proposal-audit, RT-RTE-content-publish	Host isolation and actual evidence-consuming decisions unobserved.
Publish problems/definitions, description/source edits, deprecation	SRC-1, references/contribute.md	Direct full read; RT-RTE-content-publish, EPI-OBJ-description	A published sorry-stub is a target, not a proved proposition.
Read human audits, failed proofs, saved items; rate/vote	SRC-1, references/discover.md, references/curate.md	Direct full reads; EPI-OBJ-review, EPI-RTE-quality-signals	Popularity/reputation cannot certify source or formal truth.
Campaign template, value attestation, timeline and completed-result selection	SRC-1, references/campaigns.md	Direct full read; EPI-RTE-campaign-review, EPI-RTE-campaign-admission, EPI-RTE-campaign-selection	Attested Open bounds remain proposed; service selector uninspected.
Collection membership/suggestion review	SRC-1, references/collections.md	Direct full read; EPI-RTE-collection-admission	Membership explicitly changes neither imports nor verification.
Discussion, backlinks, dead-end feedback	SRC-1, references/communicate.md	Direct full read; EPI-OBJ-review, RT-RTE-solver-proof	No automatic validation of discussion claims found in this contract.
Mission introductory prose	SRC-1, references/mission_description.md	Direct full read; EPI-OBJ-description	Citation and status-honesty policies, not a prose verifier.
Milestone/frontier read side	SRC-1, references/missions.md	Supplied runtime findings only; RT-BAP-milestone-guidance	Detailed read-side implementation not inspected. Captain and solver consumers were read directly.
Extraction and exact-payload/type-diff checks	SRC-1, scripts/extract_decl_graph.lean, scripts/extract_sketch_info.lean, references/upload_full_project.md	Direct full reads; EPI-RTE-extraction-facts, RT-RTE-project-upload	Planner, generator and uploader are agent-written, not shipped implementations.
Authentication/version refresh and local environment setup	SRC-1, references/setup.md, references/lean-setup.md	Supplied runtime findings only; RT-RTE-workspace-refresh, RT-RTE-solver-proof	No installed environment, executed update or update-to-version equivalence evidence.
Workspace/example candidate artifacts and smoke test	SRC-1, Definitions/.gitkeep, Theorems/.gitkeep, Solutions/SmokeTest.lean, examples/upload_full_project/README.md	Supplied boundary inventory; individual example bodies uninspected	Prevents provenance/acceptance findings for particular example candidates and a system-complete negative.

Missing evidence is local to its conclusion. Backend source prevents an implemented verification/closure/permission guarantee; host source prevents implemented auditor isolation and model-fixity conclusions; execution traces prevent exercised acceptance, later reliance and learning claims; interventions prevent causal effectiveness claims. Accessible but unread example bodies are not an access gap. Imported sources and mathematical toolchains are not separately frozen here, so their truth and trust assumptions are not independently warranted by this run.

Epistemic-object inventory

Each object's identity, form and substrate are owned by the cited record. Rows separate formal target, proof payload, descriptions and testimony because their checks differ.

Object ID	Candidate truth-apt content or none	Claimed role	Evidence source ID and local anchor	Gap/limit
EPI-OBJ-source	External theorem, hypotheses, definitions and argument	Reference for translation	SRC-1, references/mission_captain.md	Acquisition requested; external source warrant unknown.
EPI-OBJ-formal-statement	Lean proposition with explicit binders; Open stub asserts a target to prove	Verification target and reusable child assumption	SRC-1, references/contribute.md	Compilation is not proof of a sorry-stub or source equivalence.
EPI-OBJ-definition	Definitions themselves stipulate meanings; included lemmas assert truth-apt propositions	Shared interface fixing what theorem symbols mean	SRC-1, references/contribute.md	A compiling definition can encode the wrong source concept.
RT-OBJ-solution	Candidate proof/disproof of exact target, possibly under imported children	Formal verification payload; identity/form/substrate: see record	SRC-1, references/prove.md	Conditional assumptions must not be promoted to closed results.
RT-OBJ-readback	Testimony about what a declaration literally asserts	Blind translation for human comparison; identity/form/substrate: see record	SRC-1, references/mission_auditor.md	Model testimony has no automatic equivalence certificate.
EPI-OBJ-description	Informal theorem description, proof explanation, source-facing mission claims	Human/agent comprehension, discovery and provenance	SRC-1, references/contribute.md	Editable prose/source metadata is distinct from immutable formal payload.
EPI-OBJ-review	Faithfulness criticism, audit comments, dead-end explanations, milestone rejection reasons	Revise or redirect later work	SRC-1, references/mission_solver.md	Retention/requested reading is not observed changed reliance.
EPI-OBJ-extraction-facts	Facts about elaborated dependencies and original source positions	Input to conversion planning/edits	SRC-1, scripts/extract_sketch_info.lean	Partial reference surface; not a certificate that generated files preserve meaning.
EPI-OBJ-campaign-value	Template-instantiation assertion and numerical bound, plus Open/Proved distinction	Comparable entries, timeline and result selection	SRC-1, references/campaigns.md	Attestation certifies match, not an Open bound's truth.
EPI-OBJ-quality-signal	None required for score/vote; optional reasoning may assert scoped claims	Quality guidance and reputation	SRC-1, references/discover.md, references/curate.md	Preference is not a truth evaluator.
RT-OBJ-skill	Workflow doctrines and API-contract claims; many imperatives are not truth-apt	Behavior guidance; identity/form/substrate: see record	SRC-1, SKILL.md	Opaque model processing: see RT-CMP-agent-model.

Authority-route ledger

The ledger splits functions even where a supplied route container owns several. See citations delegate generic endpoints, progression, ownership, state, return and read-back fields to that container; the architectural status and authority assessment here are independent. Doctrine-only means an instructed or documented route, not an inspected implementation of the external evaluator. Results listed below are possible documented results, never observed results.

Route ID	Route function	Architectural status	Object/candidate ID	Content/update relation	Transition or check target	Evaluator/condition and domain	Activation and timing	Possible or observed result	Implemented force	Epistemic authority and scope	Operational authority: behavior permitted, blocked, or changed	Behavioral-authority path: consumer, channel, force, horizon	Evidence source ID and local anchor	Claim IDs or none	Mismatch marker or none	Gap/limit
RT-RTE-solver-proof	content transformation	doctrine only	EPI-OBJ-source	truth-apt transformation: acquisition/import	External source and prior submissions enter scouting	Agent selects exact reference and attempts; source warrant unknown	Before proof; see route	Retrieved content	None in inspected host	Acquired, not produced; no new warrant	Guides proof choice	Agent; fetched source/history; advisory; current attempt	SRC-1, references/mission_solver.md	none	none	Fetching and faithful uptake unobserved.
RT-RTE-proposal-audit	content transformation	doctrine only	EPI-OBJ-formal-statement	truth-apt transformation: indeterminate	Source-to-Lean encoding	Captain maps hypotheses/definitions; domain is named source result	Drafting; see route	Candidate formalization	None	Intended non-ampliative translation; preservation not established for any candidate	Supplies editable target	Captain; draft Lean; permissive proposal; review rounds	SRC-1, references/mission_captain.md	none	none	Could preserve, weaken, strengthen or trivialize the source; actual source/code pair needed.
RT-RTE-solver-proof	content transformation	doctrine only	RT-OBJ-solution	truth-apt transformation: indeterminate	Candidate proof/disproof construction	Agent; symbolic mathematical target	Attempt before checking; see route	Candidate proof or errors	None	Generation alone licenses no proposition	Allows submission attempt	Agent; generated Lean; permissive; current attempt	SRC-1, references/prove.md	none	none	No particular proof episode establishes whether construction is source reshaping, derivation or conjecture.
RT-RTE-solver-proof	check/evidence production	doctrine only	RT-OBJ-solution	no content change	Formal solution type against target or whole quantified negation	External Lean/service; fixed target environment and import rules	Local compilation then server polling; see route	ACCEPTED, SKETCH_ACCEPTED, CE, WA, SORRY, FAILED, ERROR	No inspected verifier enforcement	Claimed exact formal-type evidence; not source equivalence	Reports whether to continue or repair	Agent; verdict/error; advisory until service disposition; attempt	SRC-1, references/prove.md	RT-CLM-verification-boundary	local/server distinction	Local build may accept forbidden self-import.
RT-RTE-solver-proof	disposition/acceptance	doctrine only	RT-OBJ-solution	no content change	Formal candidate admission	Claimed service criteria: exact type, own code sorry-free, permitted imports	Terminal verdict; see route	Reject, accepted leaf, conditional sketch	External contract only	Intended use: formal proof/disproof of target under admitted axioms/dependencies	Records successful or failed submission; errors lead to resubmission	Service/solver; status; enforcing as claimed; submission and later attempts	SRC-1, references/prove.md	RT-CLM-verification-boundary	none	Recorded evidence-consuming acceptance not observed; no accepted ampliative product identified.
RT-RTE-reduction-proof	check/evidence production	doctrine only	RT-OBJ-solution	truth-apt transformation: entailed derivation	Parent under imported child propositions	Claimed Lean check in target environment	Reduction submitted; see route	Checked conditional parent	External contract only	Parent follows from checked child assumptions, not from proved premises when children Open	Admits reduction candidate to disposition	Service; Lean payload/verdict; enforcing as claimed; submission	SRC-1, references/prove.md	RT-CLM-verification-boundary	conditional warrant	Formal premise truth remains open until closure.
RT-RTE-reduction-proof	lifecycle integration	doctrine only	EPI-OBJ-formal-statement	no content change	Accepted sketch edges, then closed parent	Claimed service: every imported child Proved	After sketch acceptance and later child closure; see route	Decomposition children; parent Proved on closure	External contract only	Conditional acceptance first; closed formal result later	Makes child targets discoverable and parent reusable	Service/future solver; dependency graph/status; permissive; across attempts	SRC-1, references/prove.md	RT-CLM-verification-boundary	none	Dependency record and closure operation unobserved.
RT-RTE-proposal-audit	content transformation	doctrine only	RT-OBJ-readback	truth-apt transformation: indeterminate	Literal Lean-to-mathematical-English rendering	Blind model; every binder, definition and edge case	Fresh delegated context before human comparison; see route	Read-back testimony	Requested input exclusion, not host enforcement	No faithfulness verdict from auditor; intended reshaping not established	Gives human a comparison artifact	Auditor/captain/human; readback field; advisory; draft and permanent publication	SRC-1, references/mission_auditor.md	none	none	Must rerun after statement edits; actual isolation and semantic accuracy unobserved.
RT-RTE-proposal-audit	check/evidence production	doctrine only	EPI-OBJ-formal-statement	no content change	Source/intent faithfulness and well-posedness	Human compares read-back/code with intent; moderator reviews public proposal	Before launch and public catalog admission; see route	Confirm, flag, review report	No inspected comparison implementation	Scoped encoding judgment, separate from formal provability	Supplies confirmation or requested revision	Human/moderator; audit page/reviews; advisory to acceptance; review round	SRC-1, references/mission_captain.md	RT-CLM-human-gate	none	Optional read-back and reference-item bypass prevent a universal blind-review claim.
RT-RTE-proposal-audit	disposition/acceptance	doctrine only	EPI-OBJ-formal-statement	no content change	Proposal item confirmation and mission admission	Human decides launch; compilation can fail; moderator approves or requests changes publicly	Human submit publishes; later moderation; see route	Published items, live private mission, public admission or send-back	External permission/transition contract only	Intended use: source-faithful mission targets, not proof of Open statements	Human can withhold launch; moderator can withhold catalog admission, not undo publication	Human/service/moderator; confirmation and proposal status; enforcing as claimed; launch/review rounds	SRC-1, references/mission_captain.md	RT-CLM-human-gate	not universal publication gate	Direct contributions/upload-first/release differ.
RT-RTE-content-publish	disposition/acceptance	doctrine only	EPI-OBJ-definition, EPI-OBJ-formal-statement	no content change	Compile/publication admission	Service checks compile/import/name rules; contributor source review is policy	After queued publish job; see route	PUBLISHED, FAILED, ERROR	External contract only	Well-formed target/interface; not truth of an Open target or faithful meaning	Publishes reusable identifiers after success, not on 202	Contributor/service; publish status/ID; enforcing as claimed; library lifetime	SRC-1, references/contribute.md	RT-CLM-human-gate	alternative gate	Per-content human approval not prescribed; backend unavailable.
RT-RTE-content-publish	disposition/acceptance	doctrine only	EPI-OBJ-formal-statement	no content change	Milestone link fidelity	Captain reviews against authoritative milestone prose	Before link write; see route	Attested link or withheld/replaced link	Requested captain judgment plus external write permission	Canonical formalization license for solvers, not proof license	Solvers instructed to use linked statement as-is	Captain → solver; milestone link/prose; permissive and instructed authority; later attempts	SRC-1, references/mission_captain.md	none	none	Link records attestation, not independently verified correctness.
RT-RTE-content-publish	retention	doctrine only	EPI-OBJ-formal-statement, EPI-OBJ-description, EPI-OBJ-review	no content change	Library, explanations and criticism retained	Service contracts; authors can edit prose but not formal statements	Publication/submission/edit; see route	Immutable formal bytes, editable prose, retained history	External contract only	Retention alone grants no acceptance or extra warrant	Enables later import, search and scouting	Future solver/human; library/history/source fetch; advisory or import-permissive; later attempts	SRC-1, references/contribute.md, references/prove.md	none	none	Description/source may change without re-verifying formal bytes.
RT-RTE-content-publish	lineage/freshness/recovery	doctrine only	EPI-OBJ-review, EPI-OBJ-formal-statement	no content change	Deprecation, unlinking, replacement and history deletion	Authorized author/captain/admin; criterion supplied by criticism	After defect detected; see route	Hidden/restored node; new-name replacement; removed link/history	External contract only	Deprecation does not retract formal status or existing imports	Discovery changes; rejected links guide future avoidance; deleting milestone removes history	Future solver; browse/link/history; advisory/selection; until later edits/deletion	SRC-1, references/contribute.md, references/mission_captain.md	none	withdrawal not revocation	No guaranteed downstream invalidation of prior reliance.
EPI-RTE-extraction-facts	check/evidence production	implemented	EPI-OBJ-extraction-facts	truth-apt transformation: entailed derivation	Elaborated environment/syntax → dependency/span facts	Lean helper rules over loaded project environment and original syntax	Helper invocation after built project; see record	JSONL facts; Stage 2 aborts on errors	Stage 2 guard prevents normal successful emission on elaboration error	Bounded metaprogram-derived facts; not mathematical source truth	Supplies conversion input; does not publish or approve generated content	Agent-written planner/generator; JSONL; advisory facts; exact source revision	SRC-1, scripts/extract_decl_graph.lean, scripts/extract_sketch_info.lean	EPI-CLM-graph-truth	partial reference surface	No executed helper or converter supplied.
RT-RTE-project-upload	content transformation	doctrine only	EPI-OBJ-formal-statement, RT-OBJ-solution	truth-apt transformation: indeterminate	Skeleton subtraction, renaming and namespace conversion	Agent-written generator following extracted spans	Before upload; see route	Generated payloads	No shipped generator enforcement	Intended formal preservation; unestablished until exact-payload checks	Prepares files for verification	Agent/generator; staged Lean; permissive; upload episode	SRC-1, references/upload_full_project.md	EPI-CLM-graph-truth	graph is insufficient	Macro/local refs and environment changes can defeat naive conversion.
RT-RTE-project-upload	check/evidence production	doctrine only	RT-OBJ-solution	no content change	Original target axiom set	Agent using Lean; allowed axioms propext, Classical.choice, Quot.sound	Before decomposition; see route	Allowed or additional axioms	Requested gate, no shipped gate controller	Dependency-on-axioms evidence in formal environment; not source truth	Requires clean axiom set before proceeding	Agent; axiom report; enforcing policy only; preparation	SRC-1, references/upload_full_project.md	EPI-CLM-graph-truth	none	No actual axiom report supplied.
RT-RTE-project-upload	check/evidence production	doctrine only	EPI-OBJ-formal-statement, RT-OBJ-solution	no content change	Exact upload payload elaboration	Local Lean build in selected environment	Before upload; see route	Build succeeds or fails	Requested gate, no shipped gate controller	Formal well-formedness/proof compilation, not original-type preservation by itself	Blocks faulty payload and requests repair	Agent/generator; build errors; enforcing policy only; staging	SRC-1, references/upload_full_project.md	EPI-CLM-graph-truth	none	No exact-payload build trace.
RT-RTE-project-upload	check/evidence production	doctrine only	EPI-OBJ-formal-statement	no content change	Original versus staged elaborated type	Agent + Lean pretty-printer/diff; only universe display-name differences permitted	After payload generation, before upload; see route	Permitted diff or target mismatch	Requested gate, no shipped comparator	Formal target preservation if comparison performed correctly; no informal-source certificate	Requires correction before immutable publication	Agent/generator; type diff; enforcing policy only; conversion episode	SRC-1, references/upload_full_project.md	EPI-CLM-graph-truth	none	No performed comparison or comparator implementation.
RT-RTE-project-upload	check/evidence production	doctrine only	EPI-OBJ-formal-statement	no content change	Final uploaded theorem statuses	Agent reads service results; every selected theorem Proved, zero Open; original targets spot-checked by ID	After uploads; see route	Completed graph or unfinished targets	Requested completion gate	Claimed formal completion within uploaded graph; not converter correctness or source faithfulness	Allows completion report and proposal handoff only after checking	Agent/human; tag-paged library/status report; enforcing policy only; upload completion	SRC-1, references/upload_full_project.md	EPI-CLM-graph-truth	none	No terminal service state supplied.
EPI-RTE-campaign-review	check/evidence production	doctrine only	EPI-OBJ-campaign-value	no content change	Goal matches numerical template over shared foundation	Moderator; exact instantiated proposition and decimal value	Public proposal approval/release review; see record	Match or mismatch	External contract only	Attests comparability, not truth of Open bound	Supplies entry-admission decision	Moderator; reviewed goal/template; advisory to admission; review round	SRC-1, references/campaigns.md	none	none	Not automatic Lean-text parsing; no observed review.
EPI-RTE-campaign-admission	disposition/acceptance	doctrine only	EPI-OBJ-campaign-value	no content change	Campaign entry admission	Moderator decides from template check	At public approval; see record	Entry/value recorded or campaign flag removed	External contract only	Accepted as comparable proposed/settled bound, according to goal status	Adds entry; mismatch can still launch ordinary mission	Service/public readers; timeline; permissive; until moderator removal	SRC-1, references/campaigns.md	none	attestation is not proof	Open entry explicitly permitted.
EPI-RTE-campaign-selection	operational admission/selection/consumption	doctrine only	EPI-OBJ-campaign-value	no content change	latest_value and preferred order	Service predicates: Proved goals for latest_value; recorded_at recency; higher/lower preference separately	Campaign reads; see record	Latest completed bound or null; ordered mission list	External contract only	Claimed completed-result selection; newest does not mean best or earliest mathematical discovery	Influences which result is reported and mission browsed	Human/agent; API fields/list order; ranking; current and future campaign use	SRC-1, references/campaigns.md	none	none	Algorithm/backend uninspected.
EPI-RTE-quality-signals	operational admission/selection/consumption	doctrine only	EPI-OBJ-quality-signal	non-truth-apt policy/content update: preferences and reputation	Content priority and user reputation	Voter/rater preference; claimed service vote/trust aggregation	Rating/voting and subsequent sorted browse; see record	Scores, votes, trust, reordered hits	External contract only	No truth license; optional reasoning is unvalidated testimony	Surfaces content/users; not proof or faithfulness admission	Agent/human; votes/trust-sorted API and ratings; ranking/advisory; later browsing	SRC-1, references/discover.md, references/curate.md	none	none	Rating-to-sort implementation not stated; votes-to-sort is stated.
EPI-RTE-collection-admission	disposition/acceptance	doctrine only	EPI-OBJ-description	non-truth-apt policy/content update: collection membership	Suggested public mission inclusion	Collection manager; editorial selection, no mathematical criterion specified	Suggestion review or direct add/remove; see record	Accepted/declined suggestion, changed membership	External contract only	Editorial grouping only	Changes navigation, not Lean imports/verification or mission authority	Editor → readers; collection list; selection; until membership removal	SRC-1, references/collections.md	none	none	Not lifecycle integration of a newly accepted mathematical claim.
RT-RTE-workspace-refresh	behavior/policy adaptation	doctrine only	RT-OBJ-skill	non-truth-apt policy/content update: instruction replacement	Version mismatch → repository pull	Agent compares service version; Git supplies changed files	Each login/refresh; see route	Updated procedure text	Requested continuation policy	Freshness is not endorsement or measured improvement	Intended change in future API/procedure use	Agent; reloaded workspace text; advisory policy; current/later sessions	SRC-1, SKILL.md	none	none	No observed update or subsequent causally dependent operation.

System-claim versus route comparison

Claim ID	Claimed operation or warrant	Claim source ID/anchor and evidence layer	Doctrine/design support	Implemented route IDs	Observed-run support	Causal support and design limits	Supported conclusion	Mismatch/unknown
RT-CLM-verification-boundary	Exact formal target check provides mathematical guarantee	SRC-1, SKILL.md; doctrine/design; see claim passage	Submission status/import rules and distinct source-faithfulness procedure	none inspected for service; see RT-RTE-solver-proof, RT-RTE-reduction-proof	None supplied	Backend/Lean trust external; Open children qualify guarantee	Claimed formal-domain checking, with conditional reduction authority	Not informal-source truth, unconditional sketch closure or independently verified service enforcement.
RT-CLM-human-gate	Human-only proposal confirmation/launch	SRC-1, references/mission_captain.md; doctrine/design; see claim passage	Human compares intent/readback, confirms items; public moderator follows	none inspected; see RT-RTE-proposal-audit, RT-RTE-content-publish	None supplied	Host/account controls unavailable; direct contribution and upload precede this gate	Proposal-specific decision protocol	No universal human approval gate on mathematical-library publication.
EPI-CLM-graph-truth	Graph is conversion ground truth; mechanical subtraction preserves statements	SRC-1, references/upload_full_project.md; doctrine/design; see record passages	Span rewriting plus axiom/build/type-diff/final-status checks requested	EPI-RTE-extraction-facts only; orchestration: see RT-RTE-project-upload	None supplied; worked-example bodies not assessed	Original-position/constant-only references; instance roots and compiler auxiliaries need special handling	Implemented bounded fact extraction supports prescribed conversion planning	Graph/positions alone cannot warrant every generated payload's semantic preservation.

Bounded conclusion

Formal proof authority and source authority are different routes. The proof/disproof contract checks an exact Lean target; a sketch establishes a parent only under imported child propositions, with later Proved-child closure required. No actual accepted candidate, successful checker execution or backend implementation was supplied. This does not negate the workflow's explicit formal criteria; it prevents attributing exercised acceptance or unconditional warrant to a concrete candidate. See RT-RTE-solver-proof, RT-RTE-reduction-proof, SRC-1, references/prove.md.

The source-facing criterion is faithfulness, not ease or formal truth. Captain checks, blind testimony, human comparison and moderator feedback are separately prescribed. The auditor is explicitly forbidden to decide faithfulness. Human confirmations are intended to accept source-faithful, well-posed mission items for that mission; public moderation admits the mission to the catalog after declarations are already published. Direct publication and upload-first are counterexamples to a universal human or moderator gate. See RT-RTE-proposal-audit, RT-CLM-human-gate, SRC-1, references/mission_captain.md, references/mission_auditor.md.

Retention and operational reliance can precede proof. Open child targets are published and imported as tracked assumptions; milestone links authorize solvers to use the attested formalization as-is. Failed attempts, human flags and captain reasons are prescribed inputs to later selection/revision. Descriptions, explanations and source fields may change independently of immutable formal declarations; they are not newly verified merely because their associated proof has a status. Deprecation hides discovery while preserving imports and proof status; unlinking preserves mission membership; deletion can destroy milestone history. These distinctions bound withdrawal and lineage claims. See RT-RTE-content-publish, RT-BAP-milestone-guidance, EPI-OBJ-description, EPI-OBJ-review, SRC-1, references/contribute.md, references/mission_captain.md.

Campaign attestation accepts comparability, not an unproved bound's truth. The moderator checks the shared-definition template and records a number; an Open goal is a legitimate proposed-value entry. The latest-value field excludes Open goals and uses recording recency, while preferred value sorting is a separate rule. Therefore neither entry inclusion nor newest timestamp independently establishes mathematical achievement or optimality. See EPI-RTE-campaign-review, EPI-RTE-campaign-admission, EPI-RTE-campaign-selection, SRC-1, references/campaigns.md.

Extraction has inspectable, narrower authority than conversion. The helpers derive facts from elaboration and syntax, with a concrete deduplication/filter trace in EPI-RTE-extraction-facts. Original-position restrictions and recursive-local exclusions bound the result reaching the consumer. Prescribed exact-payload builds and original/staged elaborated-type diffs are needed after generation; no shipped generator or executed comparison establishes semantic preservation here. Source mathematical warrant remains unknown, whereas helper-derived structural facts have implementation support in their stated domain. See EPI-CLM-graph-truth, SRC-1, scripts/extract_sketch_info.lean, scripts/extract_decl_graph.lean, references/upload_full_project.md.

No concrete newly accepted ampliative mathematical claim is individuated. Source import is acquisition; intended translations remain indeterminate without input/output pairs; checked formal derivation is a distinct, conditional doctrine route. Quality signals and collection membership have ranking/editorial authority rather than truth authority. Version mismatch can request replacement of behavior-guiding instructions without a truth-apt product or demonstrated improvement. See EPI-RTE-quality-signals, EPI-RTE-collection-admission, RT-RTE-workspace-refresh, SRC-1, references/curate.md, references/collections.md, SKILL.md.

Model parameters, version resolution and internal truth-apt representations remain uninspected: see RT-CMP-agent-model. That uncertainty does not erase inspectable workflow affordances. Product-review iteration, later-use instructions and instruction refresh do not independently establish improved future capacity, reflection about the workflow, autonomous performance of every internal operation, or exercised self-improvement. The human-dependent proposal route and the separately host-dependent solver route keep their independent property limits in the supplied records. No system-wide epistemic score or complete-negative verdict follows.

Shared records

Components

none declared in this member

Operative objects

EPI-OBJ-source

Label: External mathematical source

Source-native identity: exact source reference, chapter assumptions, theorem/equation index and source argument consulted by captain/solver. Representational form: natural-language mathematics and source symbolic formulas. Storage substrate: external references plus fetched agent context and citation metadata; no actual fetched source is supplied. Distinct from RT-OBJ-skill, which directs acquisition, and RT-OBJ-solution, which is a generated proof payload. No supplied object declares the mathematical source itself. SRC-1, references/mission_captain.md, doctrine/design.

Read the whole section, not just the theorem. Sources state many assumptions once, at the top of a chapter or section ("Throughout this section we assume…", "Assumption (A)", the definitions of the objects). --- references/mission_captain.md

EPI-OBJ-formal-statement

Label: Formal statement target

Source-native identity: theorem formal_statement and its preamble, mirrored into Theorems/ and published under theorem ID/environment. Representational form: symbolic Lean proposition and sorry-stub. Storage substrate: local file, mutable draft and documented immutable published declaration. Distinct from RT-OBJ-solution: the target is the oracle against which the separately submitted solution is checked. It is not contained in that proof-payload record. SRC-1, references/contribute.md, references/prove.md, doctrine/design.

The theorem name must match theorem_name. Must end with := by sorry. --- references/contribute.md

EPI-OBJ-definition

Label: Definition interface

Source-native identity: /submit-definition payload and Definitions.Def_<definition_name> module. Representational form: symbolic Lean definitions, types, instances and any included proved lemmas. Storage substrate: local module, draft and documented published interface. Distinct from RT-OBJ-solution and EPI-OBJ-formal-statement; definitions fix target interpretation rather than furnishing an independently verifiable problem ID. SRC-1, references/contribute.md, doctrine/design.

A definition file must be sorry-free — it is not a holding pen for unproved lemmas. --- references/contribute.md

Note: you cannot submit proofs against a definition. Attempting to call /verify with a definition's ID returns a 400 error. --- references/contribute.md

EPI-OBJ-description

Label: Editable mathematical prose

Source-native identity: natural_language_statement, submission explanation, mission description and attached source metadata. Representational form: natural-language mathematical claims and citations interpreted by readers/models, distinct from symbolic Lean. Storage substrate: documented editable platform fields and description snapshots. This groups the human-readable parts with no inspected automatic mathematical checker; their edit permissions differ as described below. Closest supplied records are RT-OBJ-solution, which expressly excludes explanation prose, and RT-OBJ-readback, whose blind literal testimony has a separate producer and check consumer. No supplied prose object is coextensive.

The author may patch an explanation, while submitters/moderators may edit theorem descriptions; source metadata can be cleared by the submitter. Mission prose is captain-maintained. These changes do not edit the formal target or prove the revised prose. SRC-1, references/prove.md, references/contribute.md, references/mission_description.md, doctrine/design.

Use PATCH /api/v1/theorems/:theorem_id to update the natural language statement, source, or tags on a theorem you submitted. Moderators may additionally edit the natural_language_statement of any theorem. --- references/contribute.md

Every change to natural_language_statement — yours or a moderator's — is snapshotted into the theorem's description edit history, viewable via the Description edit history endpoint below. --- references/contribute.md

Every nontrivial claim in the body also gets its link inline where the claim is made. --- references/mission_description.md

EPI-OBJ-review

Label: Review and attempt testimony

Source-native identity: theorem audits, proposal reviews and item flags, milestone-history reason, and discussion attempt comments with artifact references. Representational form: natural-language criticisms and explanations plus symbolic artifact/status identifiers. Storage substrate: documented platform histories/discussions, with author edits, comment soft deletion and milestone-history deletion limits. These are inputs already mentioned by RT-RTE-solver-proof, RT-RTE-proposal-audit and RT-BAP-milestone-guidance, not duplicate route identities. They differ from RT-OBJ-readback, whose producer must not judge faithfulness.

Human audits judge correctness/well-posedness; moderators produce requested changes; the captain supplies rejected-link reasons. Solver consumption is explicit, not observed. Discussion authors are not automatic truth evaluators, and token-based is_agent attribution does not identify the actual reasoning producer. SRC-1, references/discover.md, references/mission_solver.md, references/communicate.md, doctrine/design.

Check the theorem's audits — the human review history returned by GET /theorems/:id. A "flag" decision is a warning sign that the statement may be wrong or ill-posed: read the reviewer's comment before investing effort (discover.md). --- references/mission_solver.md

Log dead-ends. When an approach fails, post an attempt comment referencing the failed solution. It saves the next agent the same wall. --- references/communicate.md

EPI-OBJ-extraction-facts

Label: Extraction JSONL facts

Source-native identity: Stage 1 decl_graph.jsonl and Stage 2 decl/ref JSONL. Representational form: symbolic names, flags, dependency arrays and source byte positions. Storage substrate: generated file/stdout captured by prescribed orchestration, not a supplied executed output. Distinct from RT-CMP-extract-decl-graph and RT-CMP-extract-sketch-info: those are producing programs, this is their output consumed by conversion. SRC-1, scripts/extract_decl_graph.lean, scripts/extract_sketch_info.lean, implementation.

IO.FS.writeFile "decl_graph.jsonl" (String.intercalate "\n" lines.toList) --- scripts/extract_decl_graph.lean

Only occurrences whose syntax carries an original position are emitted; --- scripts/extract_sketch_info.lean

EPI-OBJ-campaign-value

Label: Attested campaign value

Source-native identity: campaign template/foundation, entry attested_value, goal status and recorded_at, and campaign latest_value. Representational form: symbolic decimal strings, IDs/statuses and Lean template proposition; human interpretation binds the value to the shared quantity. Storage substrate: documented campaign/mission records. Distinct from EPI-OBJ-formal-statement: this is the cross-mission comparability/result record, not just the Lean goal. No supplied runtime record individuates campaign attestation. SRC-1, references/campaigns.md, doctrine/design.

An entry whose goal theorem is still Open is a proposed value: someone stated it, the community has yet to prove it. --- references/campaigns.md

EPI-OBJ-quality-signal

Label: Quality and reputation signals

Source-native identity: /rate score/reasoning, content votes and profile trust. Representational form: symbolic numeric preferences and optional natural-language justification. Storage substrate: documented platform records. Distinct from verdicts consumed by RT-RTE-solver-proof: these preferences do not assess exact proof type. No supplied counterpart after comparison. SRC-1, references/discover.md, references/curate.md, doctrine/design.

Voting helps surface the best content and affects the creator's trust score. --- references/curate.md

Routes

EPI-RTE-extraction-facts

Label: Bounded extraction facts Part of: RT-RTE-project-upload

Endpoints/progression: loaded built-project environment → Stage 1 filtered declaration/dependency JSONL; individual source file → re-elaboration and error guard → Stage 2 declaration spans and deduplicated original-position constant-reference JSONL. Owner: helper code; invocation/configuration belongs to external agent. Inputs: environment, project prefix, exact source bytes; effect: file/stdout facts, not generated proof approval. This is the executable fact-production part of the larger prescribed project route. SRC-1, scripts/extract_decl_graph.lean, scripts/extract_sketch_info.lean, implementation.

• implementation conclusion status: wired
• operation conclusion status: uninspected
• Immediate return: Stage 1 writes a graph file; Stage 2 prints facts or exits 1 on missing argument/elaboration error.
• Later read-back: uninspected — generated fact files are intended for the converter, but no later invocation or reusable generated artifact was supplied.
• Delegated visibility: inapplicable — these programs do not launch a delegated model context.
• Selection predicate: Stage 1 keeps project-module declarations, retaining private user names and traversing filtered internal dependencies; Stage 2 keeps original constant syntax, optional prefix matches, deduplicates by constant/start/end and sorts by start.
• Invalidation or expiry: byte positions belong to the exact source version; the playbook requires re-extraction after edits.
• Activation or effect: facts are prescribed planner/generator inputs; actual conversion or downstream behavior is unobserved.
• Evidence limits: imported Lean semantics/toolchain and built source environment are external; original-position and constant-expression restrictions omit some references; no helper execution was performed.

Concrete deterministic trace, deduced from inspected implementation rather than execution: give the Stage 2 refs fold two identical tuples (SumSquares.foo, start=10, end=13) and one (Other.foo, start=20, end=23), with prefix SumSquares. The first tuple's key is new and its name passes isPrefixOf, so it is inserted; the repeated tuple has the same key and is discarded; the Other tuple fails keep and is discarded. Sorting a one-element result leaves that single ref. This establishes deduplication/filtering of supplied resolved tuples, not that arbitrary source text elaborates to those tuples or that every semantic reference enters refs. No target fixture was created.

let key := s!"{c}:{s'.byteIdx}:{e.byteIdx}" if seen.contains key || !keep c then (seen, out) else (seen.insert key, out.push r) --- scripts/extract_sketch_info.lean

| some p => p.isPrefixOf c || p.isPrefixOf ((privateToUserName? c).getD c) | none => true --- scripts/extract_sketch_info.lean

if s.commandState.messages.hasErrors then for msg in s.commandState.messages.toList do IO.eprintln (← msg.toString) return 1 --- scripts/extract_sketch_info.lean

The completeness counterexample is source-supported: a recursive self-reference elaborating as a local variable never passes the .const branch. Thus a complete rename cannot be licensed from emitted ref rows alone. The playbook compensates with re-elaboration and type diff, not a claim that omissions cannot occur.

A recursive def's self-references inside its own body elaborate as local variables, not constants, so they produce no ref fact. --- scripts/extract_sketch_info.lean

EPI-RTE-campaign-review

Label: Campaign template review

Distinct from RT-RTE-proposal-audit: ordinary proposal faithfulness review is the enclosing review setting, while this record owns the additional quantity-template comparison and numeric attestation target. It spans proposal review and campaign comparability, rather than being coextensive with the supplied generic route. Endpoints/progression: public campaign-flagged proposal or private release → moderator reads goal against template/foundation → match/mismatch result. Owner: moderator. State/input: exact bound in goal and shared definition imports; effect: evidence for separate campaign entry decision. SRC-1, references/campaigns.md, doctrine/design.

• contract conclusion status: claimed
• implementation conclusion status: uninspected
• operation conclusion status: uninspected
• Immediate return: a review finding that the goal does or does not instantiate the template, with numeric value on a match.
• Later read-back: inapplicable — this check's result is passed to entry disposition; persistent timeline/read-back is owned by the separate admission/selection routes.
• Delegated visibility: inapplicable — no blind sub-agent frame is prescribed for moderator value attestation.
• Selection predicate: submitted campaign flag selects the template/foundation and exact goal for moderator comparison.
• Invalidation or expiry: wrong-template finding prevents campaign inclusion; no implemented re-attestation algorithm is supplied.
• Activation or effect: result is documented input to campaign entry admission, not proof of the goal.
• Evidence limits: no moderator episode or backend comparison implementation; Open goals can pass this check.

Contributor proposes exact numerical substitution; moderator decides and can withhold campaign match. Answer reference is the campaign template and shared foundation, not a model-invented expected answer. Mode: open campaign entry proposal/review, triggered by public approval or release. Product under assessment is comparability of a formal numerical proposition, not an improvement to the workflow's own machinery.

Theory assessment boundary: formulated campaign goal and its shared-definition interpretation. theory-builder conditions 1–4: condition 1 conclusion status: afforded — a whole Lean proposition is localized; condition 2 conclusion status: claimed — template comparison depends on its content; condition 3 conclusion status: uninspected — mismatch withdrawal is prescribed, but no particular challenged claim/result/blame episode is supplied; condition 4 conclusion status: uninspected — no retained campaign criticism shaping a new round is identified. Addressability: draft goal/value/imports are inspectable and editable before launch; published types require replacement. Persistence: entry and goal have a documented cross-attempt horizon. Learning: uninspected — no improved future capacity evidence. Reflection: uninspected — campaign records concern mathematical products, not an established two-way representation of this workflow. Reflective theory builder: uninspected — no method criticism against operation records. Autonomous theory builder: inapplicable — this prescribed comparison explicitly requires a moderator decision.

Approval of a campaign-flagged proposal is also the value attestation: the moderator checks that the goal theorem instantiates the template over the foundation definitions, and records the numeric value. --- references/campaigns.md

EPI-RTE-campaign-admission

Label: Campaign entry admission

Distinct from RT-RTE-proposal-audit: mission launch does not itself imply this extra cross-mission timeline admission. Endpoints/progression: template-review finding → moderator approval with entry/value record, or campaign flag removal → ordinary mission remains. Owner: moderator/service. State/action effects: adds comparable public entry and recording date; private launch adds no entry. SRC-1, references/campaigns.md, doctrine/design.

• contract conclusion status: claimed
• implementation conclusion status: uninspected
• operation conclusion status: uninspected
• Immediate return: campaign entry created with recorded value/date, or flag removed while ordinary mission launches.
• Later read-back: public timeline and campaign lists expose the accepted entry/value to later readers; proposed versus settled distinction uses goal status.
• Delegated visibility: inapplicable — no delegated model context is prescribed by entry admission.
• Selection predicate: moderator accepts template instantiation for a public mission; private launch is excluded until public release review.
• Invalidation or expiry: moderator can remove an entry outright; no entry-status lifecycle is exposed.
• Activation or effect: accepted entry joins timeline, even when goal Open; actual writes and subsequent reliance unobserved.
• Evidence limits: inclusion is comparability acceptance for campaign use, not evidence the numerical claim was proved; service uninspected.

Trigger/change: public review proposes adding a mission's bound to the shared quantity record. Proposer is captain/human; moderator decides and can veto campaign inclusion, not necessarily ordinary mission launch. Guidance: exact value substitution and unchanged foundation definitions. Accepted value persists until removal; wrong-template recovery is ordinary-mission launch without campaign flag. Criterion/intended use/scope: same template over same definitions for comparable campaign entries. No new mathematical truth follows from this decision alone.

It instantiates the template. The mission launches and its campaign entry is created, with recorded_at set to the approval time. The entry does not wait for the goal to be proved: an open bound is a valid entry. --- references/campaigns.md

It does not. The moderator removes the campaign flag and the mission simply launches as an ordinary mission. --- references/campaigns.md

Every listed entry is attested: an entry exists only because a moderator accepted it, and a moderator can remove one outright, so there is no entry status to check. --- references/campaigns.md

EPI-RTE-campaign-selection

Label: Campaign result selection

Distinct from RT-RTE-solver-proof: this selects an already attested campaign result, rather than an attempted target or proof verdict. Endpoints/progression: retained entries and goal statuses → latest completed value or preferred mission order → API/website readers. Owner: external service contract. State/effects: filters Open entries out of latest_value; uses recency for that field and independent higher/lower preference for mission order. SRC-1, references/campaigns.md, doctrine/design.

• contract conclusion status: claimed
• implementation conclusion status: uninspected
• operation conclusion status: uninspected
• Immediate return: latest_value decimal string or null; mission order follows configured value_direction.
• Later read-back: later campaign reads consume retained entry/value/status/recording-date data.
• Delegated visibility: inapplicable — no delegated context appears in campaign selection.
• Selection predicate: only Proved goals qualify for latest_value, then newest recorded_at; higher/lower value preference controls mission sorting separately.
• Invalidation or expiry: entry removal or changed goal/completion state can affect eligibility; exact backend update timing uninspected.
• Activation or effect: documented reported-result and browsing order; no downstream target choice observed.
• Evidence limits: recency measures record entry, not mathematical discovery, and does not establish best bound; backend selector unavailable.

Selector is software as claimed, with moderator-provided attestation and proof-status input from a separate verifier. Reference outcome is not an answer oracle for a new mathematical problem: it is the existing entry/status record. Mode is campaign browsing; no theory revision or product acceptance occurs in this selection route.

entry_count counts the campaign's entries; latest_value is the most recent completed mission's attested value (by recorded_at, the date it entered the campaign's record). Only missions whose goal theorem is Proved qualify; it is null when none are completed. Open mission values do not replace completed results. --- references/campaigns.md

value_direction is higher or lower: which value is better. It controls default mission sorting independently of bound_type. --- references/campaigns.md

EPI-RTE-quality-signals

Label: Quality signal consumption

Distinct from RT-RTE-solver-proof, which mentions post-verdict rating but not the quality/reputation selector mechanism. Endpoints/progression: rater/voter supplies score or toggleable vote → service records/aggregates signals → content votes and user trust sorting expose preference. Owner: users/agents for judgments, external service for stored counts/sort. Context: theorem/submission IDs and optional reasons. Effects: discovery priority and reputation, not theorem proof status. SRC-1, references/discover.md, references/curate.md, doctrine/design.

• contract conclusion status: claimed
• implementation conclusion status: uninspected
• operation conclusion status: uninspected
• Immediate return: vote created/changed/toggled-off; rating accepts score with optional reasoning under the documented API.
• Later read-back: later browsing can use vote_count and trust ordering; rating is described as a shared quality signal but its exact read/aggregation path is unspecified.
• Delegated visibility: inapplicable — no delegated context is prescribed for voting/rating.
• Selection predicate: agent/human chooses content by perceived interest/difficulty/elegance; server supports theorem sort=votes and user sort=trust.
• Invalidation or expiry: identical repeat vote removes it, opposite vote flips it; rating replacement/expiry policy uninspected.
• Activation or effect: claimed ranking/reputation change, not observed improved selection or truth acceptance.
• Evidence limits: no service implementation or consumer episode; rating-to-ranking linkage is not specified and is not inferred.

Rater/voter proposes and decides the preference; score-domain validation is not truth evaluation. There is no mathematical answer oracle. Mode: ongoing open content curation. User/voter can withdraw a vote; service computes trust from first-proof and vote signals as documented. The quantity does not license claims about a user's general mathematical reliability.

Whenever you evaluate theorems, rate them based on difficulty, interest, or elegance (an integer from 0-10). Ratings are a quality signal that helps everyone judge which problems are worth attempting. --- references/discover.md

First vote: creates the vote --- references/curate.md

Same vote again: toggles off (removes the vote) --- references/curate.md

Additionally, upvotes on your theorems and proofs give +1 trust, and downvotes give -1 trust. --- references/curate.md

EPI-RTE-collection-admission

Label: Collection mission admission

No supplied counterpart after comparison with RT-RTE-content-publish: this is editorial membership of already public missions, not publishing Lean nodes or milestone attestation. Endpoints/progression: authenticated suggestion/reason → manager accepts or declines; editors may directly add/remove mission → retained collection mission list. Owner: collection owner/editors; service supplies permissions and recorded membership. State/effects: changed navigation grouping. SRC-1, references/collections.md, doctrine/design.

• contract conclusion status: claimed
• implementation conclusion status: uninspected
• operation conclusion status: uninspected
• Immediate return: suggestion ID/status; review/direct membership writes return 204 or a documented error.
• Later read-back: collection mission list and reviewed suggestion status are available to later readers/managers.
• Delegated visibility: inapplicable — no delegated model context is prescribed.
• Selection predicate: proposer chooses public mission, manager chooses editorial inclusion; no fixed mathematical acceptance criterion stated.
• Invalidation or expiry: editor can remove membership; reviewed suggestions cannot be reopened by resubmission; conflicting decisions return 409.
• Activation or effect: acceptance adds mission and accepts pending suggestions for it, decline changes no membership; operation unobserved.
• Evidence limits: editorial admission changes neither imports nor verification and grants no mission-editing permission.

Proposer supplies mission and optional reason; manager decides and can veto. Mode: open editorial curation, without mathematical answer oracle. Trigger/proposed change: request to include an existing public mission. Guidance is topic/textbook/research grouping; persisted result is membership/review status. Recovery is manager membership removal or new editorial action, not formal proof rollback.

Collection membership does not add Lean imports or change verification. Use each mission's own Lean environment. --- references/collections.md

Accepting adds the mission and accepts every pending suggestion for it at once. Declining changes no membership. --- references/collections.md

Claims

EPI-CLM-graph-truth

Label: Graph ground truth

Claimed operation: project conversion must use the supplied elaboration extractors for positions/dependencies, treating the graph as ground truth; skeleton subtraction is said to preserve source context and statements. Distinct from RT-CLM-verification-boundary: this is upstream conversion authority, not the server's proof-verification guarantee. The implementation supports bounded extraction, while the playbook itself requires consumer compensation and independent exact-payload checks. SRC-1, references/upload_full_project.md, doctrine/design; scripts/extract_decl_graph.lean, scripts/extract_sketch_info.lean, implementation.

This graph is the ground truth everything else consumes. --- references/upload_full_project.md

Hand-splitting loses variable scopes, local notations, and instance context; subtraction preserves them byte-for-byte, which is why statements survive unchanged. --- references/upload_full_project.md

Instances vanish from proof terms (a CoeFun unfolds away at elaboration), so reachability never marks them, yet consumers fail without them. --- references/upload_full_project.md

Pretty-print the elaborated type of every node in the original tree and in the staged tree (a 20-line run_meta with ppExpr) and diff; the only acceptable differences are universe display names (u_1 vs u_2). --- references/upload_full_project.md

Evidenced absences

none declared in this member

Behavioral-authority paths

none declared in this member