diff --git a/.claude/board/EPIPHANIES.md b/.claude/board/EPIPHANIES.md index 39e0177df..96669bb01 100644 --- a/.claude/board/EPIPHANIES.md +++ b/.claude/board/EPIPHANIES.md @@ -1,3 +1,96 @@ +## 2026-09-03 — E-THE-FREE-MITIGATION-WAS-FREE-FOR-TWO-HOURS-1 — the entry's own thesis, applied to the entry + +**Status:** FINDING (observed on #1160; supersedes the mitigation half of +`E-THE-FIX-FOR-A-REVIEW-FINDING-SHIPS-UNREVIEWED-BY-DEFAULT-1`, whose Status +line is regraded in place). +**Confidence:** High for the fact (the reviewer said it in its own words); +the cause is not established. + +**What happened.** That entry, merged roughly two hours ago, offered a remedy +and graded it: *"The cheap mitigation, available today and unrelated to spend +… It costs one comment, is not rate-limited."* On #1160 the same reviewer +answered a review request with **"You have reached your Codex usage limits for +code reviews."** The other reviewer is simultaneously at its org spending cap. +**Both reviewers are now capped, and the free workaround is not free.** + +**Why this is worth its own id rather than a quiet edit.** The superseded +sentence is the exact failure mode of the entry it lives in — *a property +measured once, later read as a standing fact* — and it decayed inside the +document written to name that decay, in about two hours. The first entry's +own rule ("carry the commit it was measured at and the command that measures +it, so a reader re-runs rather than trusts") was applied there to claims about +the TREE and not to a claim about an EXTERNAL SERVICE, which is the gap: +external quotas are strictly less stable than a repo, and a remedy's +availability is not a property of the mechanism it remedies. + +**What is NOT superseded.** The trigger semantics — a push is not a review +trigger, so the commit fixing a finding is reviewed only if someone asks — is +a statement about the reviewer's contract, quoted from its own notice, and is +untouched. What changed is that asking now costs quota that is exhausted, which +makes the operator's spend decision the only remaining lever rather than one of +two. + +**Operational consequence, recorded because it is live.** As of now no +external reviewer can see any PR in this repo. Local gates (`cargo test`, +`clippy -D warnings`, `fmt`, disable-runs) are the whole verification surface +until the caps lift or are raised — which is a statement about coverage, not a +licence to merge faster. + +## 2026-09-03 — E-A-CITATION-IS-NOT-A-DEPENDENCY-AND-A-FORCED-COPY-NEEDS-A-GATE-1 — the Σ-transport kernel, verified by a crate it cannot call + +**Status:** FINDING (both implementations read; the gate is written, passing, +and disable-verified). +**Confidence:** High — the two bodies are byte-identical on inspection, and the +new test fails when either is perturbed. + +**What was found.** `lance_graph_contract::sigma_propagation::ewa_sandwich` +carried a module header claiming the math was *"verified empirically by +`crates/jc::ewa_sandwich`"*, quoting that pillar's numbers (PSD-preservation +1.000000, 10000/10000 hops). The kernel is a **byte-identical copy** of +`jc::ewa_sandwich`'s private `sandwich` — same arithmetic, same variable names, +same `0.5 * (r01 + r10)` symmetrization. + +**The duplication is FORCED, and that is the interesting part.** +`lance-graph-contract` is zero-dependency by design; its manifest forbids even +optional path deps, after one killed the whole PR pipeline on 2026-07-07. So it +structurally cannot call `jc` or share its `Spd2`. This is not a dedup target: +the copy has to exist. + +**What could not exist by citation is the certification.** A crate cannot +inherit a proof from a crate it is forbidden to depend on; naming the pillar in +a doc comment transfers no evidence. And the failure mode is quiet by +construction — **two identical copies agree until the moment one is edited**, +which is exactly when nobody is comparing them. Nothing in the tree executed +both; `grep` for a test naming them together returned nothing. + +**The fix is directional, and the direction is the whole design.** The gate +cannot live in the contract (it may never depend on `jc`). It lives in `jc`, +which already dev-depends on the contract, so it needed **zero new dependency +edges** — `jc::ewa_sandwich::tests::the_contract_copy_matches_the_certified_kernel_bit_for_bit` +runs both kernels over 1000 sampled SPD pairs and asserts **bit** equality +(`to_bits()`, not a tolerance: the two are the same arithmetic in the same order +on the same f64s, so any tolerance would hide precisely the drift the test +exists to catch). It carries an anti-vacuity guard requiring that most sampled +pairs have a non-zero off-diagonal, because diagonal inputs make the +symmetrization vanish and would agree under a wrong implementation too. +Disable-verified: dropping the symmetrization from the ABI copy fails it. + +**A structural check that nearly went unmade.** `jc` is workspace-EXCLUDED, so +`cargo test -p jc` does not work and a test there could plausibly never run. +It does: `.github/workflows/jc-proof.yml` runs +`cargo test --manifest-path crates/jc/Cargo.toml` on `crates/jc/**`. Worth +checking rather than assuming — an excluded crate's test that CI never runs is +a gate in name only. (I initially misread `"crates/jc"` in the root manifest as +membership; it is in the `exclude` list. Reading a grep hit without checking +which list it landed in is the same error shape this session hit four times +already.) + +**The generalisation.** *A citation is not a dependency.* Where an +architectural rule forces a copy, the certification does not travel with it, +and the copy needs its own executed gate — placed on the side of the boundary +that is ALLOWED to see both. The header now points at the test rather than at +the crate, which is the difference between a claim and a check. + ## 2026-09-03 — E-A-HAND-SWEEP-UNDERCOUNTS-TOWARD-DONE-AND-THE-CRITERION-IS-THE-WHOLE-DESIGN-1 — I reported 1 of 208; five defensible definitions give 32 to 125 **Status:** FINDING (measured, five variants, each reproducible from the @@ -137,7 +230,14 @@ because a clean audit result is evidence too, and because the next session should not have to re-run it blind. ## 2026-09-03 — E-THE-FIX-FOR-A-REVIEW-FINDING-SHIPS-UNREVIEWED-BY-DEFAULT-1 — the cap was the visible half -**Status:** FINDING (measured on this PR's own review metadata). +**Status:** FINDING (measured on this PR's own review metadata). **⊘ ITS +MITIGATION IS SUPERSEDED 2026-09-03, ~2h after this entry merged** — the +paragraph below calls `@codex review` "unrelated to spend" and "not +rate-limited"; that was measured and is now FALSE. Codex returned "You have +reached your Codex usage limits for code reviews" on #1160. Both reviewers are +now capped. See `E-THE-FREE-MITIGATION-WAS-FREE-FOR-TWO-HOURS-1` (above). The +trigger-semantics MECHANISM is untouched; only the remedy's availability +changed. **Confidence:** High for the MECHANISM (the trigger list is quoted verbatim from the reviewer's own notice). **Medium for the coverage table**, which is an inference from an ABSENCE: the same reviewer's stated rule is "comment when I diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index 1a880d9a9..49f738b76 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,3 +1,23 @@ +## 2026-09-03 — branch (#1160): both external reviewers are now capped — INVENTORY DELTA + +- OBSERVED on #1160: Codex answered a review request with "You have reached your Codex usage limits for code reviews"; CodeRabbit is simultaneously at its org spending cap (85 attempts/7d → 1/hour). **No external reviewer can currently see any PR in this repo.** +- CONSEQUENCE for the board: `E-THE-FIX-FOR-A-REVIEW-FINDING-SHIPS-UNREVIEWED-BY-DEFAULT-1` merged ~2h ago calling `@codex review` "unrelated to spend" and "not rate-limited". That was measured and is now false. Status line regraded in place (the one edit F1 permits); the mechanism half — a push is not a review trigger — is untouched and still quoted from the reviewer's own notice. New entry: `E-THE-FREE-MITIGATION-WAS-FREE-FOR-TWO-HOURS-1`. +- The lesson is narrower than "claims decay": that entry applied its own rule (carry the commit and the command) to claims about the TREE and not to a claim about an EXTERNAL SERVICE. A quota is strictly less stable than a repo, and a remedy's availability is not a property of the mechanism it remedies. +- OPEN, operational: `e7a0a032` still has ONE check attached (Cursor Bugbot, neutral, itself spend-capped). No repo workflow has run on that head. Cause established: the commit was pushed while the branch had no open PR, so no `pull_request` event fired for it; and marking the PR ready does not help, because `ready_for_review` is not in the default `pull_request` types (`opened`/`synchronize`/`reopened`). `opened` did fire at PR creation and produced no runs, which is NOT yet explained — an org-level Actions quota is a plausible common cause with the two bot caps, but it is unverified and is recorded as a hypothesis, not a finding. +- Therefore #1160's body claim that the new gate "is covered by CI (`jc-proof.yml`)" is currently a statement about the workflow's CONFIGURATION (trigger read: `pull_request`, `paths: crates/jc/**`) and not about an executed run on this head. Flagged rather than left standing, since the PR's own subject is the difference between a citation and a check. +- This commit carries real board work; that it also emits a `synchronize` event and may dispatch the workflows is a side effect, not its purpose. An empty commit to kick CI would not have been acceptable. + +## 2026-09-03 — branch (D-DCR-4 Σ-transport: the forced copy gets its gate) — INVENTORY DELTA + +- ADDED `crates/jc/src/ewa_sandwich.rs::tests::the_contract_copy_matches_the_certified_kernel_bit_for_bit` — runs the certified private `sandwich` and `lance_graph_contract::sigma_propagation::ewa_sandwich` over 1000 sampled SPD pairs and asserts BIT equality (`to_bits()`, no tolerance — the two are the same arithmetic in the same order, so a tolerance would hide the drift the test exists to catch). Anti-vacuity guard: most sampled pairs must carry a non-zero off-diagonal, since diagonal inputs make the shared symmetrization vanish. **Disable-verified**: dropping `0.5 * (r01 + r10)` from the ABI copy fails it; restored, green. +- ZERO new dependency edges: `jc` already dev-depends on `lance-graph-contract`. +- CHANGED `crates/lance-graph-contract/src/sigma_propagation.rs` module header — it claimed the kernel was "verified empirically by `crates/jc::ewa_sandwich`" and quoted that pillar's numbers, while nothing executed both. It now states that the copy is FORCED (this crate is zero-dep and may never call `jc`), that a citation transfers no evidence across a boundary the citing crate cannot cross, and it names the test instead of the crate. +- MEASURED: the two kernels are byte-identical on inspection (`jc/src/ewa_sandwich.rs:185` vs `contract/src/sigma_propagation.rs:194`) — same arithmetic, same variable names. So this was never a dedup target and never a divergence risk; it was a DRIFT risk, and drift between identical copies is silent by construction. +- VERIFIED before relying on it: `jc` is workspace-EXCLUDED (`cargo test -p jc` fails), but CI does run it — `.github/workflows/jc-proof.yml` runs `cargo test --manifest-path crates/jc/Cargo.toml` on `crates/jc/**`. An excluded crate's test that CI never runs would have been a gate in name only. +- CORRECTION to my own reading: I first took `"crates/jc"` in the root manifest as membership; it is in the `exclude` list. Same error shape as four earlier today — reading a grep hit without checking which list it landed in. +- Gates: `jc` 137/0 (was 136), contract 1309/0, fmt clean on both. +- Epiphany: `E-A-CITATION-IS-NOT-A-DEPENDENCY-AND-A-FORCED-COPY-NEEDS-A-GATE-1`. + ## 2026-09-03 — the retracted mint's DANGLING REFERENCES: three board/knowledge lines still advertise a deleted module **D-MRL-2a's own mandatory co-change, owed since 2026-09-02 and unpaid.** It diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 59961edf5..90680145e 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -112,7 +112,7 @@ earns a row because it has a merged artifact of its own. | D-DCR-2 | Mengenlehre candidate evaluation via `contract::revision::EvidenceMask` (support ∩ / refute ∖ over `dismech_evidence::Supports`) | **In PR** — `lance-graph-planner/src/dismech_candidates.rs` (`EvidenceItem` / `apply` / `evaluate` / `Evaluation` / `is_informative`). Only `Support` and `Refute` are set operations; `Partial` and `NoEvidence` are INERT by design (full-strength elimination must not be bought with partial evidence, and an asserted absence is not a licence to cut) — reported via `decisive`, never silently dropped. `narrowing` separates "decisive by stance" from "actually taught something", the primitive W5's frontier needs. 6 gates, 4 disable-verified. Spec corrected in preflight: the refute class is the evidence STANCE (`Supports`, shipped + measured), NOT the graph-construction skip filter the plan first named. The skip filter decides whether an item becomes an edge at all, so a candidate set built from the graph has already excluded it — `∖` would subtract twice. Plan §W2 carries the full correction | | D-DCR-2b | **the field map** — propagate precision about a knowledge stage over the WHOLE field; agreement / disagreement / support chains / MISSING LINKS into the HHTL nodes; the boring `is_a`/`part_of` rails lifted into a causality graph with propagated node edges | **In progress** (operator ruling 2026-09-01: three kinds of Mengenlehre; W2 shipped only kind 3, the question mask). Kind 2 (threshold elimination — Shannon / EWA / Hambly / Lyons) is a READING of this map and belongs with W4. **Carrier named 2026-09-01** (`E-AN-HHTL-POSITION-IS-A-NODE-AND-A-NODE-HAS-A-VALUE-1`): an HHTL position is an SoA node whose VALUE lane carries the 12-byte payload read as **24 signed i4** lanes — `+` agreement / `−` disagreement / `0` silence. Still unruled: which lane, versioned vs live, sweep granularity, and a node-level hydrate step for rail-implicit positions. **Census + one-node falsifier shipped 2026-09-01** (`E-G24N4-ALREADY-SHIPS-AND-THAT-IS-WHY-W2B-CANNOT-USE-IT-1`): `G24N4` already ships on `ValueTenant::CausalWitness`, so the carrier is not greenfield — and its operator-locked loci-never-magnitude value law plus its reserved slots `16..24` rule that lane OUT for W2b; 260 of 480 slab bytes free, so space is not the constraint. `tests/w2b_one_node_field.rs` pins the carrier at one-node scale (5 falsifiers, each disable-verified) incl. the whale case; it mints no lane and reserves no byte, and gap 3 (sweep convergence) is untouched. **Slices 1+2 shipped 2026-09-01 (this branch)**: DN dissolution + mechanical/epistemic split + one-hop law; `basin_lanes::BasinLanes` (magnitude register, G24N4 shape) + `accumulate_children` (one-hop, exact-sum-then-clamp) + `hhtl::{missing_ancestors, direct_children}`. Open: multi-register contested-mass semantics, provenance marker, tenant mint for the magnitude register (census: NOT CausalWitness; append margin at slab 220). **⊘ Superseded 2026-09-01 (co-architect ruling, `E-THE-SIGNED-NET-WAS-FALSIFIED-NOT-LIMITED-AND-THE-LOCI-LAW-WAS-SCOPED-TOO-WIDE-1`):** signed net falsified → `epistemic_bassin::EpistemicBassin24` pair (contested ≠ silence, survives accumulation); loci law re-scoped to the A9 READING so the bassin is a classid-selected reading of tenant 14 — NO new tenant until one real row needs both readings; Shannon/EWA adapters shipped against `dismech_candidates` counts + `sigma_propagation` certificates; Hambly-Lyons laneless while jc Pillar 11 is red. The named 24-axis catalogue SHIPPED as v3 2026-09-01 (`ogar-epistemic` 0x0334 + `epistemic_bassin::axes` mirror; supersedable by a v4 mint). Still open: the child-mask index, the provenance marker (PROVENANCE is now axis 20 — the marker's ROW placement is still unruled), armed catalogue parity after the OGAR merge **⊘ RETRACTED 2026-09-02 (operator semantic-family ruling; see `E-SIX-SEMANTIC-FAMILIES-MUST-NOT-IMPERSONATE-EACH-OTHER-1`):** `basin_lanes`, `epistemic_bassin` (the 24-byte pair), the fixed 24-axis basis (`ogar-epistemic` 0x0334) and the pair-specific loco band 0x87..0x8B are REMOVED — they aliased the episodic-loci, qualia-magnitude and population-basin families into one register. Population-basin geometry is an accepted VACANCY (no tenant, no ClassView, no axis set); tenants 14/15, Qualia, Cam96/PairPalette and the #1128 HHTL helpers stand. Kind-1 field map returns to **Open — falsifier-first design step next**. | | D-DCR-3 | counterfactual replay (edge cut through `contract::counterfactual`, Pearl rung 3), two-sided load-bearing/redundant gates | **In PR** — `lance-graph-planner/src/dismech_counterfactual.rs`. Both arms go through W1's `replay_chain` (no second replay path); the cut arm reserves the range AFTER the factual one and is tagged `InferenceType::Counterfactual` (−6) so the road not taken can never read as observed truth. **Measured correction:** the verdict reads FREQUENCY, not confidence — confidence saturates at 170 across every fixture, so a confidence bar would have been a vacuous threshold. `EdgeRole` carries the cut edge's own `CausalTopology` (59-60) + `ReasoningBand` (61-63) so "explains" stays distinguishable from "relates to". Also lands `impl EpisodicEdge for CausalEdge64` (the bridge `contract::counterfactual` documents as BLOCKED — the planner is the first crate depending on both sides). 8 gates, 4 disable-verified | -| D-DCR-4 | Σ transport via `jc::ewa_sandwich` + candidate-entropy readout; entropy-surface CONSOLIDATION decision recorded first | **Gate DONE 2026-09-03** (`e5e2520`, PROBE-ENTROPY-SURFACE-CENSUS-1): 7 surfaces / 4 conventions measured. Target is `contract::thought_atoms` (operator 2026-08-31), NOT `jc` — and the module had ZERO PRODUCTION consumers at the time of the gate (the census probe's own use is not one; the row narrates chronologically and the consolidation below closes it). C1 PASS (base inert), C2 FALSIFIED as pre-registered (B ≡ A on non-degenerate input, OPPOSITE on zero mass — routing is not a drop-in), C3 PASS (F/G are not entropies of a distribution: 92.1 apart at 10× mass, negative above 1). See `E-THE-ENTROPY-HOME-WAS-RULED-AND-LEFT-EMPTY-1`. **Consolidation SHIPPED 2026-09-03**: `insight::confidence_entropy` routed to `thought_atoms::normalized_entropy` (consumer count 0 → 1), the empty-arena guard preserved and pinned two-sided — C1 made the substitution safe, C2 named the one hazard. Forms C/D/E (excluded crates) and F/G (not entropies of a distribution) deliberately untouched. See `E-A-RULED-HOME-NEEDS-A-FIRST-CONSUMER-OR-IT-IS-A-VACANCY-1`. Σ-transport half still Queued | +| D-DCR-4 | Σ transport via `jc::ewa_sandwich` + candidate-entropy readout; entropy-surface CONSOLIDATION decision recorded first | **Gate DONE 2026-09-03** (`e5e2520`, PROBE-ENTROPY-SURFACE-CENSUS-1): 7 surfaces / 4 conventions measured. Target is `contract::thought_atoms` (operator 2026-08-31), NOT `jc` — and the module had ZERO PRODUCTION consumers at the time of the gate (the census probe's own use is not one; the row narrates chronologically and the consolidation below closes it). C1 PASS (base inert), C2 FALSIFIED as pre-registered (B ≡ A on non-degenerate input, OPPOSITE on zero mass — routing is not a drop-in), C3 PASS (F/G are not entropies of a distribution: 92.1 apart at 10× mass, negative above 1). See `E-THE-ENTROPY-HOME-WAS-RULED-AND-LEFT-EMPTY-1`. **Consolidation SHIPPED 2026-09-03**: `insight::confidence_entropy` routed to `thought_atoms::normalized_entropy` (consumer count 0 → 1), the empty-arena guard preserved and pinned two-sided — C1 made the substitution safe, C2 named the one hazard. Forms C/D/E (excluded crates) and F/G (not entropies of a distribution) deliberately untouched. See `E-A-RULED-HOME-NEEDS-A-FIRST-CONSUMER-OR-IT-IS-A-VACANCY-1`. **Σ-transport half DONE 2026-09-03**: the `jc::ewa_sandwich` citation was prose — `contract::sigma_propagation::ewa_sandwich` is a byte-identical FORCED copy (contract is zero-dep and may never call `jc`), so the certification could not travel with it. Gate added in `jc` (the only side allowed to see both, zero new dep edges), bit-equality over 1000 SPD pairs, disable-verified, CI-covered via `jc-proof.yml`. See `E-A-CITATION-IS-NOT-A-DEPENDENCY-AND-A-FORCED-COPY-NEEDS-A-GATE-1` | | D-DCR-5 | frontier scheduling (info-gain / rung-cost via `EpistemicMode::for_rung`) | **HELD** — operator rung 5-9 table ruling + W0 KILL check | | D-DCR-6 | consumer-leg pointer honoured: corpus bake + live evidence stay consumer-side; only synthetic fixtures here | standing gate | diff --git a/crates/jc/src/ewa_sandwich.rs b/crates/jc/src/ewa_sandwich.rs index 39797c5d6..bb3dfbf5a 100644 --- a/crates/jc/src/ewa_sandwich.rs +++ b/crates/jc/src/ewa_sandwich.rs @@ -387,6 +387,86 @@ mod tests { assert!(approx(r.c, 1.0, 1e-12)); } + /// **The ABI copy must not drift from the certified kernel.** + /// + /// `lance_graph_contract::sigma_propagation::ewa_sandwich` is a + /// BYTE-IDENTICAL copy of this module's private `sandwich` — same + /// arithmetic, same variable names, same `0.5 * (r01 + r10)` + /// symmetrization. That is not an accident and not a defect: the contract + /// crate is zero-dependency BY DESIGN (its manifest forbids even optional + /// path deps, after one killed the whole PR pipeline on 2026-07-07), so it + /// structurally CANNOT call this function or share this type. The + /// duplication is forced by the architecture. + /// + /// What was missing is the consequence: the copy's own module doc claims + /// it is "verified empirically by `crates/jc::ewa_sandwich`" and quotes + /// this pillar's numbers, while nothing anywhere executed both. A + /// verification claim that cites a crate the citing crate cannot depend on + /// is prose, not a test — and two identical copies agree until the moment + /// one is edited, which is exactly when no one is looking. + /// + /// This test is the missing execution. It lives HERE rather than in the + /// contract crate for the same reason the duplication exists: `jc` may + /// depend on the contract (it already dev-depends on it), and the contract + /// may never depend on `jc`. Direction is the whole design. + #[test] + fn the_contract_copy_matches_the_certified_kernel_bit_for_bit() { + use lance_graph_contract::sigma_propagation::Spd2 as AbiSpd2; + + let to_abi = |x: &Spd2| AbiSpd2 { + a: x.a, + b: x.b, + c: x.c, + }; + + // Anti-vacuity: identity-shaped or diagonal inputs would agree under + // almost any implementation, including a wrong one, because the + // symmetrization term vanishes. Count how many sampled pairs actually + // exercise a non-zero off-diagonal AND a non-symmetric intermediate, + // and require that most of them do. + let mut state = 0xCAFEu64; + let mut exercised = 0usize; + let total = 1000usize; + + for _ in 0..total { + let m = sample_step_sigma(&mut state, 0.3); + let n = sample_step_sigma(&mut state, 0.3); + let m_sqrt = m.sqrt(); + + let certified = sandwich(&m_sqrt, &n); + let abi = lance_graph_contract::sigma_propagation::ewa_sandwich( + &to_abi(&m_sqrt), + &to_abi(&n), + ); + + // BIT equality, not approximate: the two are the same arithmetic in + // the same order on the same f64s. Any tolerance here would hide + // precisely the drift this test exists to catch. + assert_eq!( + certified.a.to_bits(), + abi.a.to_bits(), + "ABI copy drifted from the certified kernel (a): \ + certified={certified:?} abi=({}, {}, {})", + abi.a, + abi.b, + abi.c + ); + assert_eq!(certified.b.to_bits(), abi.b.to_bits(), "…(b)"); + assert_eq!(certified.c.to_bits(), abi.c.to_bits(), "…(c)"); + + if m_sqrt.b.abs() > 1e-9 && n.b.abs() > 1e-9 { + exercised += 1; + } + } + + assert!( + exercised * 2 > total, + "fixture is vacuous: only {exercised}/{total} sampled pairs had a \ + non-zero off-diagonal, so the comparison never exercised the \ + symmetrization the two copies share" + ); + } + #[test] fn sandwich_preserves_spd() { let mut state = 0xCAFEu64; diff --git a/crates/lance-graph-contract/src/sigma_propagation.rs b/crates/lance-graph-contract/src/sigma_propagation.rs index 6634c4d19..46494d15b 100644 --- a/crates/lance-graph-contract/src/sigma_propagation.rs +++ b/crates/lance-graph-contract/src/sigma_propagation.rs @@ -1,6 +1,22 @@ //! Σ-Propagation — EWA-Sandwich kernel for multi-hop edge propagation. //! -//! # The math (Pillar 6, verified empirically by `crates/jc::ewa_sandwich`) +//! # The math (Pillar 6, certified in `crates/jc::ewa_sandwich`) +//! +//! **This module's [`ewa_sandwich`] is a byte-identical COPY of that pillar's +//! private `sandwich` kernel, and the duplication is forced, not sloppy:** this +//! crate is zero-dependency by design (see its manifest), so it can neither +//! call `jc` nor share its `Spd2`. What the copy therefore cannot do is inherit +//! the certification by citing it — for a while this header said "verified +//! empirically by `crates/jc::ewa_sandwich`" and quoted that pillar's numbers, +//! while nothing anywhere ran both. Two identical copies agree right up until +//! one is edited, which is when nobody is looking. +//! +//! The agreement is now EXECUTED, in the only direction the dependency rule +//! permits: `jc` dev-depends on this crate and +//! `jc::ewa_sandwich::tests::the_contract_copy_matches_the_certified_kernel_bit_for_bit` +//! runs both kernels over 1000 sampled SPD pairs and asserts bit equality. It +//! is covered by CI (`.github/workflows/jc-proof.yml`). Edit either kernel and +//! that test fails — verified by doing it. //! //! Multi-hop signal propagation through a graph of SPD covariance matrices //! follows the **EWA-Sandwich** rule: