MOTO v1.1.03

.cursor/rules/latex-renderer.mdc

@@ -59,7 +59,7 @@ Both paths call `DOMPurify.sanitize(rawHtml, DOMPURIFY_CONFIG)` after `renderLat
 
 Dual rendering: **Rendered LaTeX View** (KaTeX math, dark theme on screen, white for PDFs) and **Raw Text View** (plain text, dark theme). All rendering flows through `LatexRenderer.jsx` (`frontend/src/components/LatexRenderer.jsx`). CSS in `LatexRenderer.css`. PDF generation via `downloadHelpers.js`.
 
-**Performance Architecture**: For large documents (>~10K words), content is split into chunks at section boundaries. Each chunk renders independently via `IntersectionObserver`-gated `RenderedChunk` components — only chunks visible in the viewport (plus 600px margin) are LaTeX-rendered. Documents >50K chars auto-default to raw mode with a banner to switch. Content updates in rendered mode are debounced (1.5s) to prevent rapid re-rendering.
+**Performance Architecture**: For large documents (>~10K words), content is split into chunks at section boundaries. Each chunk renders independently via `IntersectionObserver`-gated `RenderedChunk` components — only chunks visible in the viewport (plus 600px margin) are LaTeX-rendered. Paper views default to rendered mode, including documents >50K chars. Content updates in rendered mode are debounced (1.5s) to prevent rapid re-rendering.
 
 ### Props API
 
@@ -97,7 +97,7 @@ DOMPurify sanitization is intentionally outside `renderLatexToHtml()` and must r
 
 **Debouncing**: `useDebouncedValue` hook delays rendered-mode processing by 1.5s during rapid content updates (WebSocket + polling). Raw mode is unaffected (instant updates).
 
-**Auto-threshold**: Documents >50K chars (`LARGE_DOC_THRESHOLD`) auto-default to raw mode with a banner offering to switch to rendered view.
+**Large-document threshold**: Documents >50K chars (`LARGE_DOC_THRESHOLD`) use the same progressive chunk rendering while preserving the caller's selected/default view.
 
 **Invariant**: Each chunk independently runs `renderLatexToHtml()` and then `DOMPurify.sanitize()`. Chunked and single-document paths must share the same conversion helpers and ordering anchors.
 
@@ -123,9 +123,9 @@ DOMPurify sanitization is intentionally outside `renderLatexToHtml()` and must r
 
 | Component | Location | PDF | Toggle | Disclaimer | Notes |
 |-----------|----------|-----|--------|------------|-------|
-| LivePaper.jsx | compiler/ | ✅ | ✅ | paper | Real-time paper viewing; auto-switches to raw >50K chars |
+| LivePaper.jsx | compiler/ | ✅ | ✅ | paper | Real-time paper viewing; defaults to rendered |
 | PaperLibrary.jsx | autonomous/ | ✅ | ✅ | baked-in | Paper library cards (backend embeds disclaimer at save) |
-| FinalAnswerView.jsx | autonomous/ | ✅ | ✅ | baked-in | Tier 3 final answer (defaults to raw for performance) |
+| FinalAnswerView.jsx | autonomous/ | ✅ | ✅ | baked-in | Tier 3 final answer; defaults to rendered |
 | FinalAnswerLibrary.jsx | autonomous/ | ✅ | ✅ | paper | Final answer library (all sessions) |
 | LivePaperProgress.jsx | autonomous/ | ✅ | ✅ | paper | Live Tier 2 paper in progress |
 | LiveTier3Progress.jsx | autonomous/ | ✅ | ✅ | paper | Live Tier 3 paper in progress |

.cursor/rules/part-1-aggregator-tool-design-specifications.mdc

@@ -15,7 +15,7 @@ Configurable 1-10 submitters + exactly 1 validator (default 3 submitters). Each
 
 **Single Validator Constraint**: Only one validator allowed — multiple validators would cause divergent database evolution, breaking coherent Markov chain alignment.
 
-Validator accepts a submission if adding it makes the training database more useful toward finding solutions. Submissions must first prefer avenues that aggressively attack the user's WHOLE question as stated, no partial solutions. If the true answer is that the user's question is impossible or has no valid solution as stated, that counts as directly answering the whole question. If a whole-question attack is absolutely not possible in one superintelligence brainstorm, they may choose the next best necessary piece whose resolution would visibly advance the original question. Broader exploratory/background-heavy avenues are allowed only when clearly required for that whole-question route, and easy/practical/broad/interesting detours must lose to a more direct rigorous route to the full prompt. On a fresh cleared run the accepted-submissions database starts blank; on normal desktop runs it reloads persisted accepted submissions, stats, and top-level manual run activity from the active data root. Manual read-only results/events views hydrate persisted data without requiring Start; autonomous/mini-aggregators must not write the manual event log. Distributor updates all submitters after each acceptance.
+Validator accepts a submission if adding it makes the training database more useful toward finding solutions. Ordinary submissions aggressively pursue the strongest credible and genuinely novel solution to the user's exact objective, using the contribution form and claim-type rigor appropriate to the problem; mathematics, theorem discovery, proof, and formalization remain first-class whenever relevant, but non-mathematical work is not rejected merely for lacking mathematical form. Submissions must first prefer avenues that aggressively attack the user's WHOLE question as stated, no partial solutions. If the true answer is that the user's question is impossible or has no valid solution as stated, that counts as directly answering the whole question. If a whole-question attack is absolutely not possible in one superintelligence brainstorm, they may choose the next best necessary piece whose resolution would visibly advance the original question. Broader exploratory/background-heavy avenues are allowed only when clearly required for that whole-question route, and easy/practical/broad/interesting detours must lose to a more direct rigorous route to the full prompt. On a fresh cleared run the accepted-submissions database starts blank; on normal desktop runs it reloads persisted accepted submissions, stats, and top-level manual run activity from the active data root. Manual read-only results/events views hydrate persisted data without requiring Start; autonomous/mini-aggregators must not write the manual event log. Distributor updates all submitters after each acceptance.
 
 ## Queue Submissions and Overflow Behavior
 
@@ -49,7 +49,7 @@ Validator processes 1, 2, or 3 submissions simultaneously using batch-specific p
 
 **Submission context injection**: Submitter context direct-injects first and offloads existing context to RAG when needed. Validator submissions under review are mandatory direct context; if a single or batch validation prompt is still too large after normal allocation, reject that validation batch with diagnostic feedback rather than indexing the pending submission as RAG.
 
-**Upload/path enforcement**: Server-side validation of `.txt` only, 5 MB max, filename sanitization, path traversal rejection. Upload responses return logical filenames, not absolute host paths. Public Aggregator starts resolve `uploaded_files` only under `user_uploads`; internal autonomous reference-paper context may opt into trusted data-root file references via an explicit coordinator flag.
+**Upload/path enforcement**: Server-side validation allows `.txt` and `.lean` text uploads only, 5 MB max, UTF-8/non-empty content, filename sanitization, path traversal rejection, and delete-by-logical-filename cleanup. Upload responses return logical filenames, not absolute host paths. Public Aggregator starts resolve `uploaded_files` only under `user_uploads`; internal autonomous reference-paper context may opt into trusted data-root file references via an explicit coordinator flag.
 
 ## Context Allocation
 
@@ -65,7 +65,7 @@ All Aggregator offload order and source-exclusion rules are centralized in `rag-
 
 ## Role Selection
 
-User selects model per role. Multiple roles can share a model. Models load with user-set context sizes. Aggregator settings also expose one shared `aggregator_assistant` memory-search LLM role for optional verified proof-memory support; built-in/default profiles set Assistant equal to the primary Validator, and Session History Memory disabled greys Assistant out. Assistant may provide up to 7 prior verified proofs, reuses useful packs for two eligible receiver reads before refresh, skips true no-external-history targets because it only performs proof-memory retrieval for now, uses run-scoped cooldown for repeated zero-useful or stagnant retrieval, shuts down only for repeated zero-useful retrieval in the current run, hides skip/backoff/shutdown turns while showing Assistant model-output failures in live activity, and never injects into validator prompts.
+User selects model per role. Multiple roles can share a model. Models load with user-set context sizes. Aggregator settings also expose one shared `aggregator_assistant` memory-search LLM role for optional verified Lean proof-history support; it cannot redirect or mathematically reinterpret an unrelated parent goal, and returning no support is valid. Built-in/default profiles set Assistant equal to the primary Validator, and Session History Memory disabled greys Assistant out. Assistant may provide up to 7 prior verified proofs, reuses useful packs for two eligible receiver reads before refresh, skips true no-external-history targets because it only performs proof-memory retrieval for now, uses run-scoped cooldown for repeated zero-useful or stagnant retrieval, shuts down only for repeated zero-useful retrieval in the current run, hides skip/backoff/shutdown turns while showing Assistant model-output failures in live activity, and never injects into validator prompts.
 
 Per-role Supercharge is optional. When enabled for a submitter or validator, `api_client_manager.generate_completion()` runs 4 parallel full answer attempts for that role call, then a 5th same-model synthesis call and returns only the synthesis result. Supercharge candidate attempts intentionally use temperatures `[0.0, 0.2, 0.4, 0.8]` to diversify parallel outputs; synthesis remains `0.0`. Candidate attempts are sanitized to reusable visible answer text before synthesis; private thought/channel/control transcript text must never be fed back as feedback, brainstorm memory, or synthesis context. The synthesis prompt frames candidates as optional working material: the model may use one, combine several, ignore all, or write a stronger new answer, while preserving the original role output contract. If Boost applies to that role/task, all internal Supercharge calls use the Boost config first. Tool-call requests bypass Supercharge.
 
@@ -93,6 +93,12 @@ Embeddings for RAG: Default mode uses LM Studio first, falls back to OpenRouter
 
 Accepted submissions database: never truncated. Live preview shows exact non-truncated log. Validator reasoning/results NOT included in the database (accepted submissions only).
 
+## Progressive Solution Path
+
+Manual Aggregator owns one durable Progressive Solution Path for the whole manual Aggregator→Compiler run. It is absent from prompts and UI until the fifth accepted brainstorm event; acceptance counting is monotonic across Stop/Start, remains distinct from cleanup-reduced retained database size, and does not include validation, proof, or paper events. Normal Manual Aggregator owns this count; parent-controlled child Aggregators share the manager without count authority. After activation, the current Main Submitter 1-approved canonical revision proposed by the semantic validator is optional advisory direct context.
+
+Only the existing semantic validator may originate an optional update, as a separately parsed addition to its normal JSON, and only for material route/goal/evidence changes or meaningful step status—not routine nuance. Malformed or omitted path data cannot change the primary decision. Proposals are durably queued without blocking validation and are transactionally reviewed by a dedicated role copied exactly from Main Submitter 1. Only completely valid approved revisions become canonical; hard failures enter explicit user-repair state and resume only through the generation-fenced retry action. Stop/crash preserves the plan and pending work; explicit manual Clear removes it and is serialized against same-run reacquisition.
+
 ## Database Cleanup Review
 
 Every 7th tracked acceptance (`total_acceptances % 7 == 0`, minimum 7 before first review). Manual Part 1 normally reloads persisted stats, so its cleanup cadence is persisted across restarts; autonomous/mini-aggregator runs can use fresh run-local stats when initialized with stats loading skipped. Autonomous resume offsets used for hard caps/completion reviews do not shift this cleanup modulo.
@@ -115,12 +121,12 @@ New submission acceptance → synchronously persists to accepted memory and asyn
 
 ## Validation
 
-JSON formatting used for all submission/validation communication. Submissions must be rooted in sound mathematical reasoning with no unfounded claims or logical fallacies.
+JSON formatting is used for all submission/validation communication. Ordinary submissions must meet domain- and claim-appropriate standards of correctness and defensibility with no unfounded claims, fabricated support, or logical fallacies. Mathematical claims specifically require sound derivation, proof, or explicit assumptions.
 
 JSON validation failure: reject submission, send reason + content to submitter's local failure feedback memory.
 
 ## Optional Lean 4 Proof Submissions
 
 When `lean4_enabled`, submitters may use `submission_type="lean_proof"` only for high-impact prompt-directed proof candidates whose claimed novelty is public/citable and absent from standard references or Mathlib, not merely new to the program. The shared Lean proof gate rejects missing/invalid novelty tiers and missing prompt-relevance/novelty/anti-standard-result rationales before Lean cost. Supporting lemmas, routine helpers, local facts, trivial/easy proofs, and weakened substitutes are not valid targets. Once Lean accepts real proof code, preserve/register the actual artifact for novelty/triviality ranking, but normal brainstorm validation may still reject it from the accepted-submission database when the actual theorem is low-impact, trivial, routine, or redundant. Hard rejection always applies to non-Lean-verified attempts, malformed submissions, or fake proof devices such as new `axiom`/`constant`/`opaque` declarations.
 
-Manual Aggregator live results expose "Try to Prove This" over the current accepted-submissions database. It uses standard proof discovery, asking for candidates that directly solve the user prompt first and then candidates that substantially build toward solving it. When Session History Memory is enabled, the separate Assistant LLM role runs in parallel during brainstorming and proof checks, maintaining a freshness-tagged up-to-7 pack of fully Lean-verified local/SyntheticLib4 memory supports for eligible submitter/proof roles; proof discovery/formalization may use the latest pack but must not wait for it, and useful packs refresh only after two eligible receiver reads. Assistant cooldown state is run-scoped across transient task IDs/roles, survives ordinary stop/restart for that same run scope, is cleared only by explicit workflow/session reset, hides skip/backoff/shutdown turns from live activity, and shows Assistant model-output failures as errors; zero-useful retrieval can shut down for the run, while stagnant same-pack retrieval only backs off. Validators never receive Assistant context. Any non-duplicate Lean-verified proof from that user-triggered check is stored in the active manual proof database and appended to the active manual Aggregator database proof appendix for user-visible display/download, regardless of novelty rating. This known-proof preservation is intentional for RALPH looping: the user can see validated work, and later proof checks can avoid redoing exact verified proofs instead of losing them because they ranked `not_novel`. Progress is also persisted to the manual Aggregator event log so live activity can recover missed WebSocket events. Later proof-check prompts strip that generated-proof appendix and receive verified proofs through the manual proof database injection instead. Manual Aggregator clear archives the active manual proof database to history and resets active proof context to empty; clear is rejected while manual proof verification is active.
+Manual Aggregator live results expose "Try to Prove This" over the current accepted-submissions database. It prioritizes direct prompt solutions, then substantial progress. Assistant retrieval is parallel/non-blocking, capped at 7, refreshed after two receiver reads, and filters the requesting run/session on fresh and reused packs; validators never receive it. Every newly verified current occurrence is stored after independent novelty judgment, while source appendices avoid only same-source exact duplication. Known and cross-run `duplicate_novel` proofs remain visible/searchable for RALPH history but stay outside highest-priority prompt-novel injection. Clear archives the active manual proof run and resets active proof context; it is rejected during verification.