Eigenius synthesis
Type: agentic-system-analyses/types/agentic-system-synthesis.md
Bounded synthesis
From prose to a delivered artifact
Eigenius is a typed knowledge platform with model-assisted prose formalization, retained executable resources and agent-facing tools. It is not the external agent's enclosing reasoning runtime. Its stated purpose is verifiable AI in science and engineering; the supported architectural contribution is more specific: it separates interpretation, artifact delivery, resource admission, domain checking and later reliance on checked evidence. This account covers repository https://github.com/eigenius/eigenius at commit 836498ebd99733067d45aa6f7b09d4ff5035dd99, with an analysis cutoff of 2026-10-15. SRC-1 supplies implementation and doctrine/design only. The complete repository is frozen, but operational coverage remains partial. No target execution, provider transcript, passing test, accepted discovery or causal comparison was supplied. See the boundary and evidence and source register.
The representative shipped workflow runs a notebook formalization cell and optionally loads its result. A persistent CLI-hosted server resolves the request's document identity, layer and lexicon scope, persists a task, and returns its UUID. A blocking formalizer then reloads previous document decisions, rebuilds glossary state, parses and resolves discourse, emits an artifact and commits newly recorded live decisions. Models receive seam-specific prompts rather than the operator's whole conversation. The notebook polls for terminal status, fetches the result, and returns the artifact with structure identity and encoded/cut counts. This is a source-traced workflow, not an observed successful delivery: RT-RTE-document-formalize and the workflow account.
Interpretation is bounded selection, not semantic certification. Code constructs candidates, limits the model's presentation to at most twelve structure groups, rejects indistinguishable presentations and checks answer membership. The full document and earlier selected glosses still enter the decision frame; the group count is not a token budget. A type-compatible candidate can misinterpret prose, and omitted alternatives cannot be chosen. Strict emission can fail on an unencodable unit; non-strict emission can return explicit cuts. Neither mode establishes faithful or complete scientific interpretation: RT-RTE-reading-selection, RT-RTE-document-formalize.
Delivery and admission are separate milestones. Without land, the artifact remains fetchable result data. With land, the notebook immediately calls auto-committing Load; mandatory human review does not intervene. The SDK propagates a refused Load as an error rather than successful landing. However, result serialization and terminal metadata writes discard errors, so completed computation need not become a retrievable terminal result. The thirty-minute client deadline stops waiting, not server work, and the inspected caller does not automatically repair and resubmit rejected content: RT-OBJ-formalization-artifact, RT-RTE-document-formalize, workflow rejection propagation.
What survives and changes later work
Recorded model decisions have an actual later consumer. Seam-specific structured exchanges become ProposalDraw resources; a later formalization loads them and matches question keys to supply choices, rankings, proposals, classifications or refusals. These are operative parser inputs, not merely audit logs. Selection and proposal keys include contextual identity; kind classification uses only sentence and gloss. Retained rationales do not establish a criticism cycle: selection replay returns its rationale, while kind rationale is explicitly for review. See MEM-OBJ-proposal-draw, MEM-OBJ-selection-record, MEM-OBJ-kind-record and MEM-BAP-recorded-decision.
The strongest supported learning-related contribution is automatic conversion of decision experience into durable, behavior-shaping replay inputs. That supports a local implemented trace-fed update, not improved future capacity. Its horizon is also limited: old draws are read before branch recreation, and replay arms contribute no replacement transcript. An all-replay round can therefore leave the new default document head without the original recordings; a third round is not guaranteed to replay them. Inline recordings provide another input route, but the shipped inline artifact-comparison test does not establish branch longevity. Original inputs also do not resolve into a controlled session-log, tool-trace, event-stream or trajectory category. These distinctions are preserved by MEM-RTE-draw-retention, MEM-BAP-recorded-decision and profile verification.
Later consumption is heterogeneous. Requested queries return retained resources and can use lexical, vector or hybrid ranking. Requested program-by-IRI execution interprets retained symbolic bodies; completion strings instead guide a provider model. Published notebooks reconstruct editable source and configuration, not a full checkpoint of prior outputs. Within computations, keyed replay automatically supplies saved answers, and post-commit rebuilding installs declaration-derived institution dispatch state. Thus requested returns coexist with internal automatic supply; there is no established unsolicited scientific-evidence feed into an enclosing chat agent. See MEM-RTE-query-resources, RT-BAP-retained-program, RT-BAP-completion-prompt, MEM-RTE-notebook-reopen and MEM-BAP-institution-refresh.
Maintenance preserves different things. Layer consolidation combines effective definitions and tombstones rather than producing a semantic summary. Tombstones suppress current resolution; eligible unreachable-layer GC forgets storage. Vector refresh derives access segments asynchronously and does not gate successful admission. Missing segments can reduce retrieval without making the underlying resources absent. None of these mechanisms alone establishes complete recall, erasure, scientific acceptance or improved reasoning: MEM-RTE-state-maintenance, MEM-RTE-index-refresh.
Admission and the scope of verification
There is no universal gate over retained content. Auto-committing Load uses structural, retroactive and applicable institution phases. Program outputs and query FIBER INTO use WithRetroactive without the same institution admission context; glossary persistence and trusted follow-up emissions take other paths. Newly loaded AutoOnLoad declarations govern later loads, not their own batch. Report verification additionally identifies a Reflect RPC trace-ingestion path using WithRetroactive without AutoOnLoad. These routes prevent equating persistence with uniform checking: RT-RTE-resource-admission, RT-RTE-program-execution, EPI-RTE-fiber-retention, report-verification limit.
Formal proof checking nevertheless has a substantive, narrower contribution. The Lean institution checks an offered export under an axiom allowlist and compares the target declaration's type with the claim's externalized proposition. Correspondence checking gates the export to Lean 4.29. A direct name-only query licenses no claim correspondence and emits no claim verification trace. For the claim-linked path, successful checking can produce a VerificationTrace; Load disposition can reject a failing subject and retain audit evidence. Later chain-attached type checking consumes accepted proof evidence as witness credit. Rebinding or tombstoning the target or proposition dependencies can withdraw ancestor credit. This is implemented acceptance and integration of a scoped formal result, not just storage of a “verified” label: EPI-RTE-lean-check, EPI-RTE-verdict-disposition, EPI-RTE-witness-consumption.
That credit depends on checker, externalization, encoding and trusted admission contracts. It does not establish empirical premises or the English interpretation. Checker identity is self-reported provenance, not independent attestation. Declared/Observed credit supplies attribution rather than truth; ProgramTrace grounds no witness. The frozen README's older three-part correspondence description differs from the implemented direct proposition comparison: EPI-OBJ-verification-trace, EPI-RTE-witness-consumption, EPI-CLM-lean-correspondence.
Statistical checking has another license. The inspected common path computes an effect decision from supplied observations and a plan using p below alpha plus a direction guard. A runnable plan can receive gate Holds while its effect does not reject; a canonical proposition attaches only conditionally. This is not automatic Verified credit or acceptance of a population mechanism. Hash verification checks byte identity; layout validation may sample, defer work or report success without a bound schema. These narrower results must not inherit formal-proof authority: EPI-RTE-statistical-decision, EPI-RTE-file-verification, EPI-RTE-layout-validation.
Scenario-relative assessment
For a request to encode prose and retain reproducible decisions, the architecture provides explicit cuts, separate artifacts and real replay consumers, subject to interpretation and replay-horizon limits. For a request to carry checked formal credit into later dependent checks, proof disposition and witness consumption provide a consequential route, conditional on their trusted machinery. For a request to establish a new empirical explanation, no supplied candidate and trace establishes accepted ampliative scientific knowledge. These are different scenarios, not a system-wide reliability grade.
The independent properties remain separate. Localized formal propositions and semantic witness consumers are implemented, but the records do not establish a full explanatory-theory route satisfying theory-builder conditions 1–4. Conditions 1 and 2 have localized-content and consumption support only for those formal propositions; they do not settle the broader theory characterization. Conditions 3 and 4—content-directed criticism and retention of its result into another round—are unestablished in the selected paths, not proven absent system-wide. No evidence establishes that criticism of a consumed theory improved future capacity. Reflection and autonomous theory building remain unassessed across the partial loop; automatic task progression and an RPC named Reflect do not establish either. See RT-RTE-document-formalize, EPI-RTE-witness-consumption and report verification.
Self-improvement is likewise unestablished at this revision and across later formalization requests. Replay offers a durable control change with a later consumer, but no independently specified improvement objective, objective-bearing evidence selecting an update, or subsequent observed operation causally dependent on that change closes an improvement-directed self-change account. No comparison demonstrates successful improvement. This does not negate the implemented trace-fed replay contribution: MEM-RTE-draw-retention, RT-RTE-document-formalize.
Concrete evidence could alter these assessments: a source-to-artifact fidelity evaluation with explicit cuts and candidate exclusions; a three-round default-branch replay trace or a change preserving replayed draws; a linked proof-check, admission, witness-use and dependency-withdrawal trace; and an objective-defined update comparison connecting retained criticism to later behavior and capacity. Broader inspection of import, Reflect, maintenance and recovery paths is needed before exhaustive coverage claims. No source reads were added during synthesis.
Limitations
| Limitation | Affected SRC IDs and record citations | Inspected boundary | Conclusion prevented | Evidence that would resolve it |
|---|---|---|---|---|
| Implementation is not observed operation or benefit. | SRC-1; RT-RTE-document-formalize, EPI-RTE-lean-check | Frozen repository code and doctrine; no registered run or experiment | Successful delivery, exercised checking, scientific discovery and causal improvement | Linked execution artifacts and appropriately scoped outcome/intervention comparisons |
| Trace-write inventory omits the separate Reflect ingestion route; carried report-verification limit. | SRC-1; MEM-OBJ-layer-resources, RT-RTE-resource-admission, EPI-RTE-witness-consumption, report-verification Limits | Verifier inspected kernel/src/server/reflect.rs: request resources enter WithRetroactive without AutoOnLoad; declaring inventories remain partial |
Exhaustive trace-acquisition and evidence-admission comparisons; inference that Load, program output and INTO exhaust mutations; handler name does not establish reflection | Accepted records tracing Reflect's acquisition, admission and actual later consumers alongside other mutation routes |
| Partial operational coverage leaves material alternatives unresolved. | SRC-1; MEM-OBJ-layer-resources, MEM-RTE-notebook-reopen, RT-RTE-runtime-registration | Bootstrap/import control, broader institutions/workers, local/offline mutations, reflection, autosave/merge and durable task recovery not collectively traced | Whole-system completeness, universal trust or deployment-grant/isolation claims, system-complete negatives about learning or autonomy | Producer-to-consumer records for these paths and explicit deployed capability contracts |
| Prose fidelity and full decision provenance remain unresolved. | SRC-1; RT-RTE-reading-selection, MEM-OBJ-rank-record, MEM-OBJ-proposal-record, MEM-OBJ-kind-record | Bounded candidate presentation, heterogeneous keys; full sense/proposal rationale use and original caller control unresolved | Faithful arbitrary-prose interpretation, uniform contextual invalidation, criticism from retained reasons or complete trace-origin classification | Paired semantic evaluations, remaining payload/consumer traces and original-input/control provenance |
| Default replay horizon is not indefinite. | SRC-1; MEM-RTE-draw-retention | Old-head read, branch reset and live-only recording; supplied evaluator uses inline draws | Guaranteed repeated branch replay, zero future provider calls or full reproduction | Three successive branch-based invocations with retained heads/draws, or revised retention plus corresponding evidence |
| Delivery, indexing and maintenance have incomplete durability/consistency guarantees. | SRC-1; RT-RTE-document-formalize, MEM-RTE-index-refresh, MEM-RTE-state-maintenance | Ignored terminal writes, non-gating vector work, current-session task roots; backend crash consistency, text-index lifecycle and metadata expiry unresolved | Guaranteed terminal retrieval, complete recall, cross-session recovery or erasure | Failure/restart traces and full backend, index and task-root lifecycle contracts |
| Formal warrant remains conditional and domain-specific. | SRC-1; EPI-RTE-lean-check, EPI-RTE-witness-consumption, EPI-OBJ-verification-trace | Selected checker/correspondence and witness paths; full externalizer, nanoda and arbitrary low-level admission not audited | Global soundness, independently attested checker identity, empirical truth or faithful English encoding | Audits of trusted components and admission boundaries, authenticated provenance, and independently warranted premises/encoding |
| Statistical and data checks do not establish general scientific acceptance. | SRC-1; EPI-RTE-statistical-decision, EPI-RTE-file-verification, EPI-RTE-layout-validation | Common decision path and diagnostic handlers; numerical/design-specific arms, data origins and deferred checks unassessed | Population-mechanism truth, full-file conformance or durable endorsement from success flags | Design/data validation, complete numerical and deferred-check evidence, and an acceptance decision for the intended scientific scope |
| Improved capacity, reflective theory building and self-improvement are not established. | SRC-1; MEM-RTE-draw-retention, RT-RTE-document-formalize, EPI-RTE-witness-consumption | Implemented replay and scoped formal reliance, without a linked content-criticism/update/comparison episode | Improvement from theory criticism, theory-builder conditions 3–4, autonomous theory building or exercised improvement-directed self-change | Explicit challenged theory, blame and changed reliance retained into another round; role-by-role autonomy evidence; objective-bearing update and later causal-use/outcome evidence |