feat: verify document-shaped semantic reliability

crates/semath-core/src/engine.rs

@@ -1052,9 +1052,7 @@ impl SemathEngine {
             match change {
                 ProjectChange::Upsert { document } => {
                     let file_id = document.file_id.clone();
-                    let accept = self.index.documents.get(&file_id).is_none_or(|current| {
-                        document.document_version > current.document.document_version
-                    });
+                    let accept = self.accepts_upsert(&document);
                     if accept {
                         let previous_order = self.index.order_document(&file_id);
                         if self.can_reuse_analysis(&document) {
@@ -1346,6 +1344,21 @@ impl SemathEngine {
             && appended_comments_only(&current.document.content, &next.content)
     }
 
+    fn accepts_upsert(&self, next: &ProjectDocument) -> bool {
+        let Some(current) = self.index.documents.get(&next.file_id) else {
+            return true;
+        };
+        if next.document_version > current.document.document_version {
+            return true;
+        }
+        next.document_version == current.document.document_version
+            && next.content == current.document.content
+            && next.path == current.document.path
+            && next.language == current.document.language
+            && next.schema_version == current.document.schema_version
+            && analysis_fingerprint(next) != current.analysis_fingerprint
+    }
+
     fn visible_definitions(
         &self,
         file_id: &str,

crates/semath-core/src/engine_tests.rs

@@ -296,6 +296,66 @@ fn incremental_upsert_matches_the_new_document_version() {
     assert_eq!(view.symbol.unwrap().definitions[0].description, "the state");
 }
 
+#[test]
+fn same_revision_structural_relink_reanalyzes_without_accepting_stale_text() {
+    let content = "Let $A$ and $B$ be events. $\\joint{A}{B}$";
+    let start = content.find("\\joint").unwrap() as u32;
+    let source = ProjectSourceRef {
+        file_id: "main".into(),
+        path: "main.tex".into(),
+        range: range(start, start + "\\joint".len() as u32),
+    };
+    let mut expanded = document("main", "main.tex", content, 1);
+    expanded.macros.push(ProjectMacro {
+        kind: ProjectMacroKind::Call,
+        name: "joint".into(),
+        source: source.clone(),
+        definitions: Vec::new(),
+        expansion: ProjectMacroExpansion {
+            status: ProjectMacroExpansionStatus::Expanded,
+            depth: 1,
+            editable: false,
+            surface: Some("A \\cap B".into()),
+            input_range: Some(range(start, start + "\\joint{A}{B}".len() as u32)),
+            notation: None,
+        },
+    });
+    let mut unresolved = document("main", "main.tex", content, 1);
+    unresolved.macros.push(ProjectMacro {
+        kind: ProjectMacroKind::Call,
+        name: "joint".into(),
+        source,
+        definitions: Vec::new(),
+        expansion: ProjectMacroExpansion {
+            status: ProjectMacroExpansionStatus::Unresolved,
+            depth: 0,
+            editable: false,
+            surface: None,
+            input_range: None,
+            notation: None,
+        },
+    });
+
+    let mut project = snapshot(content);
+    project.documents = vec![expanded];
+    let mut engine = SemathEngine::default();
+    engine.reset(project).unwrap();
+    let update = engine
+        .apply(ChangeEnvelope {
+            protocol_version: PROTOCOL_VERSION,
+            epoch: "project:1".into(),
+            inventory_version: 2,
+            analysis_generation: 2,
+            changes: vec![ProjectChange::Upsert {
+                document: Box::new(unresolved),
+            }],
+        })
+        .unwrap();
+
+    assert_eq!(update.changed_file_ids, ["main"]);
+    assert_eq!(update.analyzed_file_ids, ["main"]);
+}
+
 #[test]
 fn append_only_comments_advance_the_version_without_semantic_reanalysis() {
     let original = "Let $x$ denote the input. $y=x$";

docs/architecture.md

@@ -67,6 +67,10 @@ Pure extractors derive document observations from immutable documents. Project m
 reverse-include invalidation, cancellation, and caching form the effectful
 shell. An edit reanalyzes only the changed document and its reverse include
 closure; clean and incremental rebuilds must produce the same semantic result.
+When an external declaration relinks a wasmtex snapshot, Semath accepts the
+same text revision only if the source identity is unchanged and the structural
+fingerprint differs. This retracts generated meaning without admitting stale or
+rewritten text under an old document version.
 
 English scientific prose follows the same functional-core boundary. Bounded
 stages segment visible spans, extract mentions and claim spans, determine each

docs/capability-test-matrix.md

@@ -6,12 +6,12 @@ reserved for real editor, Worker, and deployment wiring.
 | Capability | Authoritative test | Boundary evidence | E2E responsibility |
 | --- | --- | --- | --- |
 | Notation CST, UTF-16, cursor paths, malformed input | wasmtex contract plus `bun run notation:conformance` matrix/generative tests | adapter and clean/incremental parity | editor selection wiring |
-| Semantic selection and binders | Rust cursor/parser/binder tests | native/WASM parity | one semantic selection journey |
+| Semantic selection and binders | Rust cursor/parser/binder properties plus the neutral eight-family cursor plan | 102 native/WASM view/navigation queries | one semantic selection journey |
 | Definitions, references, rename | pure scope and include-order tests | LSP mapping and both cursor edges | one navigation journey |
 | Canonical meaning and typed laws | Rust canonical/unifier tests plus manifest-owned corpus | protocol and native/WASM equality | one meaning-first view |
 | Shapes, quantities, roles, diagnostics | pure extractors and contradiction tests | Worker/LSP result mapping | reveal one source-linked conflict |
 | Domain packs | Rust schema-7 compiler tests, conformance, pack-derived property planning, and evaluated or probe corpus | clean package and compiled catalog | none |
-| Incremental analysis | pure edit-trace planning, first-divergence comparison, shrinking, reverse-include closure, and clean-rebuild equivalence | full-path 61-document budget and 501-document scale budget | one rapid-edit wiring case |
+| Incremental analysis | pure six-family lifecycle planning, first-divergence comparison, shrinking, reverse-include closure, and clean-rebuild equivalence | fixed-sample and manual full-lifecycle parity plus 61/501-document budgets | one rapid-edit wiring case |
 | Worker lifecycle | pure queue and generation policy tests | real engine recreation | one project-switch or crash case |
 | CorTeX formula meaning | pure calm-presentation and bounded view-model tests | component integration tests | one meaning and one real-conflict journey |
 

docs/pack-maturity.md

@@ -1,6 +1,6 @@
 # Pack maturity report
 
-This is measured repository state on 2026-08-10, not live production telemetry
+This is measured repository state on 2026-08-11, not live production telemetry
 and not a future plan. The [quality manifest](../fixtures/corpus-manifest.json)
 holds approved support policy; GitHub issues hold planned work.
 
@@ -21,14 +21,12 @@ holds approved support policy; GitHub issues hold planned work.
   Electromagnetism, thermodynamics/heat transfer, fluid mechanics, calculus,
   discrete mathematics, and optimization remain deliberately narrow slices;
   evaluated capability evidence is not a field-completeness claim.
-- The independent frozen challenge v2 contains 48 cases across binding,
-  constraints, packs, presentation, resolution, and syntax. The Protocol 8
-  hard-cutover engine passes 48 of 48. Three reviewed oracle corrections preserve
-  a complete `\\sum` token during local malformed recovery and place the
-  higher-order derivative cursor on `\\partial^2`, the notation being tested;
-  the capacitor condition pair also declares its differentiation variable as
-  time on both sides of the boundary. Case IDs remain frozen, and each
-  correction removes an unintended variable rather than relaxing an outcome.
+- The independent frozen challenge v3 preserves 48 semantic boundaries across
+  binding, constraints, packs, presentation, resolution, and syntax, then
+  composes them into six realistic document shapes. The engine passes 48 of 48,
+  including all five decision states, source-grounded explanations, and the
+  neutral-versus-conflict Problems policy. Full execution remains a manual
+  release gate.
 
 These numbers describe the synthetic benchmark, not real-world prevalence or
 field completeness.

docs/performance.md

@@ -16,7 +16,8 @@ mkdir -p .artifacts && bun run budget:report
 
 The fixture set deterministically rotates through the reported ECE expression,
 nested modifiers and styles, dense matrices, Unicode and combining characters,
-malformed recovery, and binder/rename notation. A measured leaf edit must parse
+malformed recovery, binder/rename notation, sectioned multi-equation reports,
+and scoped malformed neighbors. A measured leaf edit must parse
 and transfer only its own syntax snapshot. Append-only comments must do no
 semantic analysis; a separate real notation mutation must analyze only its
 reverse-include closure and complete within 50ms. An empty delta must also do no
@@ -37,6 +38,11 @@ defaults, not live production telemetry. The dependency lock pins the
 wasmtex input used for a report; record the Semath and wasmtex commits when
 comparing reports.
 
+The report also names every lifecycle family, exposes semantic-view p95
+separately from other cursor queries, and records deterministic failure-shrinker
+input, output, and evaluation counts. Shrinking has a linear work budget; timing
+is not gated on a shared runner.
+
 The normal and scale gates cap law candidates at 20 visited rules per document.
 This is a structural dispatch budget, independent of installed pack count.
 Pure 100-pack and 500-pack fixtures additionally require a uniquely keyed form

docs/public-api.md

@@ -17,6 +17,9 @@ hard cutover to a small meaning-first API.
 Hosts send a complete `ProjectSnapshot`, then ordered `ChangeEnvelope` deltas.
 Every request carries protocol, inventory, document, and analysis versions so
 stale results can be rejected.
+An upsert may repeat a document version only for a wasmtex structural relink of
+identical source and path. Semath requires a changed structural fingerprint;
+same-version text changes remain stale and are ignored.
 
 The query surface is:
 

docs/semantic-quality-scorecards.md

@@ -40,13 +40,16 @@ assumption, evidence, refusal, and scope independently instead of blending them
 into one recognition number.
 
 The frozen recognition challenge is separate from those development and
-diversity fixtures. Version 2 has 48 manually authored cases, including twelve
-positive/refusal semantic boundary pairs, grouped by the layer that owns a
-failure: syntax, binding, constraint, pack, resolution, or presentation. Exact
-IDs and normalized document sources must not occur in development or foundation
-fixtures. Association, structure, constraint, recognition, evidence, refusal,
-scope, and navigation remain separate metrics. Default CI validates
-the challenge schema and coverage matrix through pure tests but does not execute
+diversity fixtures. Version 3 preserves the 48 independently authored v2
+semantic boundaries and places every case into one reviewed document shape:
+distant prose, neighboring macros, neighboring malformed input, multiple
+equations, a multi-file project, or section scope. Every case declares the
+expected final decision, meaning presence, and Problems policy. The scorecard
+reports decision classes, source grounding, reason integrity, and problem
+visibility separately from association, structure, constraints, recognition,
+evidence, refusal, scope, and navigation. Exact IDs and normalized document
+sources must not occur in development or foundation fixtures. Default CI
+validates the schema, pure composition, and coverage matrix but does not execute
 the engine over the holdout.
 Evaluated laws require
 100% role, evidence, and refusal preservation, at least 99% precision, and at
@@ -90,7 +93,10 @@ Pack validation also derives a deterministic bounded property plan from the
 reviewed law declarations. Its oracle is the declared transformation relation,
 not the production matcher. Broad generated execution and failure artifacts
 remain part of the manual quality workflow; only planner integrity and a small
-fixed sample run in default CI.
+fixed sample run in default CI. A separate cursor plan exercises 102
+native/WASM queries across eight neutral structural families and compares
+semantic view, definition, references, and rename preparation at every reviewed
+edge.
 
 Native/WASM parity, full-path incremental latency and memory, package integrity,
 and documentation are separate gates so failures remain actionable. The normal