From 97db650d9fec1ce7ae27e83a7eeb6e52e6592711 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 19:52:09 +0000 Subject: [PATCH 1/5] =?UTF-8?q?knowledge:=20post-#1132=20literature=20harv?= =?UTF-8?q?est=20=E2=80=94=20two=20pillar=20corrections,=20MINT=20NOW=20em?= =?UTF-8?q?pty?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five-area literature audit (NARS/term logic, bilattice/FDE, EIG/active inference, Hambly-Lyons signatures, SPD/EWA concentration) adjudicated against the ratified post-#1126..#1132 / OGAR #295..#297 architecture and against shipped code rather than prose. Outcome: no new atom, axis, or core opcode. Nine certificate-grade results, of which two correct existing claims: - Pillar 5+ (jc/koestenberger.rs) is a lawful use of K-S Thm 1, but sigma_propagation::pillar_5plus_bound is the jc generator's empirical CV curve applied to a congruence orbit, and sigma_tension_u4 divides a squared distance by it. Deterministic isometry bound proposed as the expressible replacement (probed). - Pillar 11's cited Hambly-Lyons Thm 1 is correct and insufficient; Thm 2/3 of the same paper give the finite-depth certificate for lattice walks (length-parameterized). Depth-2 forward leg is necessary-only: the paper's own figure-eight has S1=S2=0, S112=1 (probed). Also: ACCUMULATE on L16 is associative (0/4096 violations) — the module caveat is too weak; the real defect is ratio distortion under per-side clamp. Greedy INFO_GAIN admission has a published Omega(n/log n) lower bound; EC^2 is the adaptive-submodular repair as a rung-local script. Board hygiene: one EPIPHANIES entry; SUPERSESSION-INDEX regenerated last. Zero code changed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QHVUi6Q9XtmKgxh6pDRayP --- .claude/board/EPIPHANIES.md | 39 +++ ...literature-harvest-2026-09-01-post-1132.md | 231 ++++++++++++++++++ 2 files changed, 270 insertions(+) create mode 100644 .claude/knowledge/literature-harvest-2026-09-01-post-1132.md diff --git a/.claude/board/EPIPHANIES.md b/.claude/board/EPIPHANIES.md index 2db871dd7..80f7bd028 100644 --- a/.claude/board/EPIPHANIES.md +++ b/.claude/board/EPIPHANIES.md @@ -1,3 +1,42 @@ +## 2026-09-01 — E-LITERATURE-HARVEST-POST-1132-TWO-PILLAR-CORRECTIONS-1 + +**Status:** HARVEST (5-auditor literature sweep, adjudicated against shipped +code; zero code changed). **Confidence:** the two corrections below are +[G] by code read + local probe; the Pillar 11 green path is [G] as read by +the auditor and awaits a main-thread re-read of the constant before the +pillar flips. + +Full ledger: `.claude/knowledge/literature-harvest-2026-09-01-post-1132.md` +(census of 45 results, nine detailed rows, MINT NOW = **empty**). + +1. **Pillar 5+ is correct; `pillar_5plus_bound` is not Pillar 5+.** + `jc/koestenberger.rs` builds a genuine inductive mean and is a lawful use + of Köstenberger-Stark Thm 1. `sigma_propagation::pillar_5plus_bound` + (`√(2/n)·√(1+2σ²n)`, σ=0.2, → 0.4) is the jc generator's empirical CV + curve — its own comment says "K-S-*style*" — applied to a congruence + orbit `MΣMᵀ`, which is an isometry, not a mean. `sigma_tension_u4` then + divides a squared affine-invariant distance by that dimensionless CV. + Eigen-aligned `M = diag(e^0.2, e^-0.2)` gives growth `0.32n²` and + saturates the u4 on every regular walk. Replacement, expressible today: + `|‖log Σ_n‖_F − ‖log Σ_0‖_F| ≤ 2·Σ‖log M_k‖_F` (probed, max ratio 0.567 + on 2000 random paths; tight on the aligned arm). +2. **Pillar 11's cited theorem is right and insufficient; the green path + is two sections later in the same paper.** Hambly-Lyons Thm 2/3 (§2.4) + give an explicit finite depth `⌈2.3959·L⌉` (d=2 lattice; `c(d)·L` in + general) at which the truncated signature separates non-tree-equivalent + unit-step walks. The Index regime therefore becomes *length- + parameterized*; the depth-2 forward leg is a necessary condition only — + the paper's own §1.6 figure-eight has `S¹=S²=0` and `S¹¹²=1` (probed). + Preconditions: `d ≥ 2` (a `u8:u8` rail read as one axis is d=1 and + collapses to the endpoint) and unit basis-aligned steps. + +Also strengthened in the safe direction: ACCUMULATE on L₁₆ is an MV-monoid +(associative; 0/4096 violations; the caveat in `epistemic_bassin.rs` is too +weak — the real defect is non-cancellative ratio distortion, which needs a +saturation flag on Contested reads). Greedy INFO_GAIN admission carries a +published Ω(n/log n) lower bound (Golovin-Krause-Ray Thm 9); EC² is the +adaptive-submodular repair as a rung-local script. + ## 2026-09-01 — E-THE-24-AXIS-BASIS-V3-EVERY-AXIS-IS-A-GROUNDED-PRESSURE-1 **Status:** BUILT on the operator's "mach weiter" — the catalogue derived diff --git a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md new file mode 100644 index 000000000..c141587d9 --- /dev/null +++ b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md @@ -0,0 +1,231 @@ +# Literature harvest — post-#1132 reasoning substrate audit (2026-09-01) + +**READ BY:** truth-architect, integration-lead, theorem-checker, contradiction-cartographer; anyone proposing a new atom, axis, loco opcode, or pillar certificate. +**Status:** HARVEST (5 Opus auditors, areas A–E with F folded into A; every cited theorem read in the source, not the abstract). Adjudicated on the main thread against **shipped code**, not prose: `epistemic_bassin.rs`, `sigma_propagation.rs`, `jc/{koestenberger,ewa_sandwich,hambly_lyons}.rs`, `planner/nars/{truth,tactics}.rs`, `ogar-loco/vocabulary.rs`, `ogar-epistemic/lib.rs`. Three claims were re-verified by local probes before entering this file (marked ✔ PROBED). +**Scope:** ratified facts of lance-graph #1126..#1132 and OGAR #295..#297 are treated as constitutional — the 256-entry palette is FULL, the six loco-core calls (TERNLOG · BELNAP_JOIN · INFO_GAIN · SIGMA_TENSION · ACCUMULATE · STANCE_ENTROPY) are universal, the 24-axis basis v3 is `0x0334`, one classid per rung, BasinCodebook for value families, red-pillar + mechanism≠rhyme rules. MC #610 is a consumer shadow and was not used as evidence. +**Question answered:** *what genuinely executable or certifying reasoning capability is still absent AFTER the core ops, v3 basis, NARS recipes, canonical atoms and loco/R2IL composition are taken into account?* + +**Headline:** MINT NOW is **empty**. The harvest's value is almost entirely **certificates** — three of them correct or strengthen claims the substrate already carries (`pillar_5plus_bound` is miscited and mis-unitized; ACCUMULATE is provably associative; greedy INFO_GAIN admission has a published Ω(n/log n) lower bound against it) — plus four rung-local macros that are compositions of what exists. One v4 pressure survives its witness test (a conative pair) and is blocked on a scope ruling, not on evidence. + +> **Area D (Hambly-Lyons / jc Pillar 11)** returned last (its first auditor died on an API error and was relaunched). It carries the single highest-value certificate of the harvest: Hambly-Lyons' *own* Theorems 2/3 give an explicit finite truncation depth for lattice walks, and the paper's own §1.6 figure-eight falsifies the depth-2 forward leg. Both entered the census below (rows D1–D4, placed by value). + +--- + +## 0. Ground truth the audit was adjudicated against + +| carrier | what the code actually does (read, not recalled) | +|---|---| +| `EpistemicBassin24` | 24 × `(agree_u4, disagree_u4)`; `net`, `contest = min(a,d)`, `axis_state ∈ {Silent, Agree, Disagree, Contested}`, `entropy_bits` = Shannon over the 4-state census, `stance_entropy_bits(children, axis)`, `accumulate_children` = exact u32 sum per side then clamp 15, `support/refute/contested/silent_mask` u64 | +| `info_gain_u4(before, after)` | `floor(log2(before/after))` clamped 0..15; `after == 0 && before > 0` → 15 | +| `sigma_tension_u4(growth, bound)` | `ceil(4·|growth|/bound)` clamped 15; `growth` = `‖log Σ_n‖²_F − ‖log Σ_0‖²_F` (a squared affine-invariant distance), `bound` = `pillar_5plus_bound(n)` | +| `pillar_5plus_bound(n)` | `√(2/n)·√(1+2·0.04·n)` — a **coefficient of variation** curve, `σ_step = 0.2` hard-coded; → 0.4 as n→∞ | +| `jc::koestenberger::prove` | a genuine Sturm inductive mean `S_{n+1} = S_n ⊕_{1/(n+1)} X_{n+1}` on 2×2 SPD, `E[d²(S_n, I)]` vs K-S Thm 1 RHS — **correct use of K-S** | +| `jc::ewa_sandwich::prove` | 10000 random paths of `MΣMᵀ` with i.i.d. rotated log-normal steps; PSD rate ≥ 0.999 and *population* CV of `‖log Σ_n‖²_F` ≤ 1.75 × the curve above; the comment itself says "Köstenberger-Stark-**style**" | +| `planner/nars/truth.rs` | deduction `⟨f₁f₂, f₁f₂c₁c₂⟩`, induction/abduction `w/(w+1)` products, analogy product — NAL-exact | +| `planner/nars/tactics.rs` | RCR #4, TR #6, ASC #7, CAS #8, CR #11 shipped; S5 throttle = confidence floor + budget k + hub exclusion; `GapKind` reach-out | +| `ogar-loco` | six core calls at `0x86..0x8B`; TERNLOG pops 3, ACCUMULATE pops 1, others pop 2 | +| `ogar-epistemic` | axes 0..23 = IS_A PART_OF TYPICALITY MISSING_LINK · SUPPORT REFUTE PARTIAL REPLICATION · PREMISE DEDUCTION FALSIFIER COUNTERFACTUAL · INFO_GAIN TENSION COHERENCE AMBIGUITY · TEMPORAL KAUSAL MODAL LOKAL · PROVENANCE REVISION QUORUM CONTRADICTION | + +--- + +## 1. Census (sorted by expected architecture value) + +| # | area | result | destination | ΔH | status | +|---|---|---|---|---|---| +| D1 | D | Hambly-Lyons **Theorem 2/3** (math/0507536v2 §2.4): a lattice path of length L whose first ⌊e·log(1+√2)·L⌋ = ⌊2.3959·L⌋ iterated integrals vanish is tree-like (d=2); general d: ⌊(2⌈log₃(d/2)⌉+3)·2.3959·L⌋. Truncated signature is a homomorphism into G^N, so `S^(N)(X)=S^(N)(Y) ⟺ X∼Y` at `N ≥ ⌈c(d)·(|X|+|Y|)⌉` for unit-step lattice walks | **CERTIFICATE_ONLY — the green path for Pillar 11**, length-parameterized | highest | auditor read §2.4; constant to be re-read before greening | +| D2 | D | The depth-2 forward leg tests membership in `ker(G^∞→G²)`, not tree-likeness: the §1.6 figure-eight has S¹=S²=0 like the out-and-back but S³≠0 | **REJECT** depth-2 as Index regime (necessary condition only) | high | ✔ PROBED (S¹¹²: fig-8 = 1.0, out-and-back = 0.0) | +| 1 | E | `pillar_5plus_bound` cites a theorem about the inductive mean of independent samples (K-S Thm 1) to certify a congruence orbit; `sigma_tension_u4` divides a squared distance by a dimensionless CV | **CERTIFICATE_ONLY (falsifies)** | high | ✔ PROBED (code read; aligned-M arm) | +| 2 | E | Replacement: deterministic isometry bound `|‖log Σ_n‖_F − ‖log Σ_0‖_F| ≤ 2·Σ‖log M_k‖_F` for any invertible symmetric M | **MACRO_CANDIDATE** (composition of `logm` + Frobenius) | high | ✔ PROBED (max ratio 0.567 on 2000 random 20-hop paths) | +| 3 | C | Greedy posterior-based admission (INFO_GAIN, VoI) is Ω(n/log n)-suboptimal (Golovin-Krause-Ray Thm 9); EC² edge-cut objective is adaptive-submodular with a `(2 ln(1/p_min)+1)` bound | CERTIFICATE_ONLY + **MACRO_CANDIDATE** `admit_ec2` | high | literature [G] | +| 4 | B | ACCUMULATE (sum-then-clamp on L₁₆) is an MV-monoid: associative, commutative, non-cancellative, top-absorbing — the module's "not claimed associative" is too weak | CERTIFICATE_ONLY (strengthen) | high | ✔ PROBED (0/4096 violations, 1360 non-cancel pairs) | +| 5 | A | Independent per-side clamp is not ratio-preserving: (30,2)→(15,2) moves f 0.938→0.882; heavy agreement drifts toward a=d=15 = false Contested | CERTIFICATE_ONLY (saturation flag) | high | arithmetic [G] | +| 6 | B | Knowledge-order MEET (⊗_k, per-component min) is not expressible by TERNLOG (boolean) or BELNAP_JOIN (max) | **MACRO_CANDIDATE** `MEET_K` | high | non-expressibility [G] | +| 7 | B | Scalar STANCE_ENTROPY is permutation-invariant over {T,F,B,N}: cannot separate Both-heavy from Neither-heavy | EXISTING_COMPOSITION (+ `contest`/`silent_mask`) + certificate | med | theorem [G] | +| 8 | C | AMBIGUITY (E[H(o|s)]) is level-set-inequivalent to INFO_GAIN (log-det vs log-det-ratio); witness in Corva 2026 Remark 4 | GROUNDING_ONLY (axis stands) | med | [G] | +| 9 | A | NAL revision ≡ ACCUMULATE; ⟨f,c⟩ ↔ (w⁺,w⁻) is a bijection for c<1 | EXISTING_PRIMITIVE | high | [G] | +| 10 | A | NAL choice/expectation `(c(f−½)+½) = (w⁺+k/2)/(w+k)` = Krichevsky-Trofimov posterior mean; antisymmetric in a↔d, so STANCE_ENTROPY cannot order beliefs | **MACRO_CANDIDATE** `EXPECT` (integer cross-multiply) | med-high | [G] | +| 11 | A | Syllogistic chaining is multiplicative and absent from the six pooling ops — but it lives in the exact NARS carrier and the shipped tactics use the exact NAL products | EXISTING_PRIMITIVE (exact carrier) | med | ✔ PROBED (`truth.rs` read) | +| 12 | C | Wald-Wolfowitz SPRT is a TERNLOG over an ACCUMULATE'd log-odds with two thresholds; the free-energy pins 0.2/0.05/0.8 have no derivation and mix a bounded and an unbounded term | MACRO_CANDIDATE `sprt_stop`; REJECT the three pins as primitives | med-high | [G]/[S] | +| 13 | C | NOVELTY (parameter info gain) = `½(1/a − 1/a₀)` over Dirichlet counts = a script over REVISION/ACCUMULATE registers | EXISTING_COMPOSITION (v4 axis rejected) | med | [G] | +| 14 | C | Pragmatic value is `−E[log p̃(o)]`, a consumer preference prior | CODEBOOK_VALUE | med | [G] | +| 15 | B | Subjective-logic cumulative fusion ≡ ACCUMULATE in evidence space; base rate `a` enters only at projection | GROUNDING_ONLY + CODEBOOK_VALUE (`prior_u4` per axis) | med | [G] | +| 16 | B | Mares 2002 paraconsistent revision: coherent ⇔ accept∩reject = ∅ ⇔ `contest = 0` | GROUNDING_ONLY | med | [G] | +| 17 | B | MIS-based inconsistency measures are not functions of per-axis (a,d); `contest` satisfies Consistency + Monotony only | REJECT as v4 axis (relational, lives in premise ancestry) | med (fence) | [G] | +| 18 | B | Every interlaced bilattice ≅ L⊙L (Avron 1996); the pair IS the canonical form; signed-net = non-injective truth projection | GROUNDING_ONLY | med | [G] | +| 19 | A | ONA anticipation = eager `FALSIFIER.disagree += δ⁻`, then `agree += δ⁺ > δ⁻`; loop is control-plane | EXISTING_COMPOSITION + certificate (`δ⁺>δ⁻` post-clamp) | med | [G] | +| 20 | A | NARS temporal projection = uniform scaling of both sides = right-shift on the pair; Allen's 13 relations are a value family | MACRO_CANDIDATE `PROJECT` + CODEBOOK_VALUE (Allen) | med | [G]/[H] | +| 21 | A | Typicality/defaults: Nixon diamond → Contested; specificity = IS_A depth → `EXPECT` → choice; Reiter extension *sets* are the one thing not expressible | EXISTING_COMPOSITION | med | [G]/[H] | +| 22 | A | Recipe 12 TCA "Granger" is a rhyme: NARS temporal induction is co-occurrence + decay, Granger is a residual-variance test | REJECT the label (relabel "temporal precedence induction", re-check rung delta) | low-med | [S] | +| 23 | A | Stamp disjointness prevents double-counting, does not certify independence (no theorem exists) | CERTIFICATE_ONLY (narrow the wording) | med | [H] | +| 24 | E | If a probabilistic bound is wanted it is the random-matrix-product CLT (Cuny-Dedecker-Merlevède-Peligrad Thm 2.1/3.1), centred at `2nλ_μ` with `√n` spread — requires i.i.d. M | CERTIFICATE_ONLY | med | [G] | +| 25 | E | No Berry-Esseen for *dependent* matrix products found; edges on a path share endpoints, so this is the live case | CERTIFICATE_ONLY, OPEN | 0 | [H] | +| 26 | E | `SIGMA_TENSION` quarters are linear in k; tail probability is ~1/k² (Cantelli/Chebyshev) — 12 of 16 codes spent on p∈[0.05,1] | CODEBOOK_VALUE (tail-class ladder), after #1 is fixed | med | [G] | +| 27 | E | "EWA" names three different operations (convex EMA, congruence, geodesic); the PSD 10000/10000 proof is a one-line identity | GROUNDING_ONLY + rename; promote `det(M)>eps` to the real gate | low | [G] | +| 28 | E | Le Gouic-Paris-Rigollet-Stromme Cor. 11: `E d² ≤ σ²/n` dimension-free on CAT(0) — sharper than K-S for any actual barycenter | GROUNDING_ONLY | 0 | [G] | +| 29 | B | Shramko-Wansing SIXTEEN₃: t-order and f-order are already the two components; permits asymmetric per-side ops | GROUNDING_ONLY | low | [G] | +| 30 | C | INFO_GAIN = Lindley EIG = I(θ;y) for uniform posteriors; u4 cap = ratio 2¹⁵ with silent one-sided saturation; Miller-Madow applies only to sampled counts | GROUNDING_ONLY (contract text) | low-med | [G] | +| 31 | C | Under additive control + fixed noise, EIG is constant across policies (Koudahl 2021) → a flat-frontier detector | CERTIFICATE_ONLY | med | [G] | +| 32 | A/F | WANT (NSM prime) ≡ Xu 2026 anti-goal `G¡ ≡ ¬(G ⇒ D̃)`: a conative (desire, aversion) pair, not an evidence lobe | **V4_AXIS_CANDIDATE — blocked on scope ruling** | med-high | [G] paradox / [H] relevance | +| 33 | F | CAN (ability/affordance) — one source, no NARS counterpart | DO NOT MINT | 0 | [S] | +| D3 | D | d=1 collapse: `S(X) = (1, Δ, Δ²/2!, …)`; a single `u8:u8` rail read as ONE scalar axis is d=1 and carries only the endpoint (Diehl-Ebrahimi-Fard-Tapia Rem. 1.4) | REJECT 1-rail carrier; `d ≥ 2` static precondition | high (fence) | [G] | +| D4 | D | Goursat scheme is O(h²) (Salvi et al. Thm 15) — the 2e-7 floor is the scheme, not signal; but Thm 8 needs C¹ and the probe paths are piecewise-linear (segment-wise Chen lemma must be written) | CERTIFICATE_ONLY | med | [G]/[H] | +| D5 | D | The depth-∞ leg against a constant path reads `dev ≈ ½‖S²‖²` to leading order — the same Lévy area the depth-2 leg reads; a figure-eight scaled by ε has `dev ∝ ε⁶` and sinks under the O(h²) floor | GROUNDING_ONLY / not independent evidence; mint a min-loop-scale precondition | med | [H] | +| D6 | D | Chevyrev-Oberhauser tensor normalization Λ (Thm 21): without it truncated signature features are not characteristic; the 1e6 "discrimination ratio" is a scale artifact | CERTIFICATE_ONLY + MACRO_CANDIDATE `Λ` | med | [G] | +| D7 | D | Factorial tail decay bounds magnitude, not discriminating power — never cite it for losslessness | GROUNDING_ONLY | low | [G] | +| D8 | D | Iterated-sums signature (ISS) quotients by time-warping, deliberately RETAINS tree-like excursions, has no group structure and no injectivity theorem | REJECT for the Index regime (separate discovery for stutter walks) | med (fence) | [G] | + +--- + +## 2. Detailed rows (the strongest nine) + +### R1 · `pillar_5plus_bound` is miscited and `sigma_tension_u4` is mis-unitized — CERTIFICATE_ONLY (falsifies) +- **CLAIM** [G] The K-S citation on `pillar_5plus_bound` is a category error; the readout that consumes it divides a squared distance by a coefficient of variation. +- **PRIMARY SOURCE** Köstenberger & Stark, arXiv:2307.06057v2 (22 Jul 2024), Theorem 1, pp. 6–8, read verbatim. +- **SPECIFIC RESULT** Thm 1 bounds `E[d²(S_n, μ)]` for the **inductive mean** `S_{n+1} = S_n ⊕_{1/(n+1)} X_{n+1}` of **independent** `L²`-valued samples. Its RHS is `O(1/n)`. `pillar_5plus_bound(n) = √(2/n)·√(1+0.08n)` is dimensionless, has no `μ`, `μ_k`, `D_n` or `Var`, and tends to `2σ_step = 0.4` (probed: 1.470, 0.812, 0.534, 0.424, 0.400 at n = 1, 4, 16, 100, 10⁴). jc's own `ewa_sandwich.rs:317` calls it "Köstenberger-Stark-*style*" and derives it from a log-normal/χ² heuristic over a population of random paths. +- **CURRENT MAP** `sigma_propagation::pillar_5plus_bound` doc ("per Pillar 5+ proof-in-code"); `sigma_tension_u4(growth, bound)` (#1129); v3 axis TENSION's grounding line in `E-THE-24-AXIS-BASIS-V3…-1`. **Pillar 5+ itself (`jc/koestenberger.rs`) is NOT affected** — it builds a real inductive mean and is a correct use of Thm 1. +- **DESTINATION** CERTIFICATE_ONLY (falsification of a citation + a units defect; no new concept). +- **ΔH** Removes "the sandwich walk is concentration-certified by K-S" and the free parameter `σ_step = 0.2`. +- **MECHANISM CHECK** `Σ' = MΣMᵀ` is a congruence, an isometry of `d_AI` for invertible M, not a geodesic convex combination; there is no `S_n` in the code (`grep barycenter|frechet|inductive_mean sigma_propagation.rs` → 0 hits). Units: `growth` is `d_AI(Σ_n, I)² − d_AI(Σ_0, I)²`; `bound` is a CV. The 10000/10000 PASS is a property of the i.i.d. rotated-step generator in `ewa_sandwich::prove`, not of the bound. +- **CERTIFICATE** Replace with R2. Until then, label `pillar_5plus_bound` "empirical CV reference curve for the jc i.i.d. generator, not a bound". +- **FALSIFIER** `Σ_0 = I`, `M_k = diag(e^0.2, e^-0.2)` for all k (eigen-aligned; `‖log M_k‖_F = 0.2√2`). Then `log Σ_n = diag(0.4n, −0.4n)`, growth `= 0.32n²`; at n=100 that is 3200 against a "bound" of 0.424 → `sigma_tension_u4` saturates at 15 on a perfectly regular walk. The i.i.d. arm passes. If the substrate's edge transforms ever correlate along a path (they do — consecutive edges share an endpoint) this arm is the live one. +- **MINT CONSEQUENCE** None. Doc + readout change; see R2. + +### R2 · Deterministic isometry bound for the sandwich — MACRO_CANDIDATE (composition), ✔ PROBED +- **CLAIM** [G] For symmetric invertible `M_k`: `|‖log Σ_n‖_F − ‖log Σ_0‖_F| ≤ 2·Σ_{k≤n} ‖log M_k‖_F`. +- **PRIMARY SOURCE** Affine-invariant metric on SPD, `d(A,B) = ‖log(B^{-1/2}AB^{-1/2})‖_F`, GL-congruence invariance (stated at arXiv:2307.06057v2 p.6); triangle inequality. +- **SPECIFIC RESULT** `d(MΣM, I) ≤ d(MΣM, M·I·M) + d(M², I) = d(Σ, I) + 2‖log M‖_F`; iterate. +- **CURRENT MAP** replaces `pillar_5plus_bound` inside `sigma_tension_u4`; `ewa_sandwich::log_norm_growth` keeps its measured quantity (R3 in census: `‖log Σ‖²_F = d_AI(Σ,I)²` exactly, closed form `(ln λ₁)² + (ln λ₂)²` for 2×2). +- **DESTINATION** MACRO_CANDIDATE — `logm` + Frobenius already exist in `Spd2`; the RHS is a running sum the propagator has in hand. Not a primitive: expressible. +- **ΔH** Deletes `σ_step`, deletes the i.i.d./isotropy assumption, adds an inequality valid for adversarial `M` sequences. +- **MECHANISM CHECK** All growth is base-point drift; drift is the accumulated step size. No distributional assumption. +- **CERTIFICATE** ✔ PROBED locally: 2000 random 20-hop paths (random rotations, log-eigenvalues uniform ±0.3), max `lhs/rhs = 0.567`. Aligned arm from R1: `lhs/rhs → 1` (tight). +- **FALSIFIER** Any invertible symmetric `M` sequence with `lhs/rhs > 1 + 1e-12`. Singular `M` voids it — which is the same failure PSD-preservation cannot see (census #27); promote `det(M) > eps` to the gate. +- **MINT CONSEQUENCE** `SIGMA_TENSION`'s `bound` argument becomes `2·Σ‖log M_k‖_F`; the u4 then measures *how much of the deterministic budget a path spent* — a lawful, unit-consistent readout. If a probabilistic statement is later wanted, census #24 (Cuny-Dedecker-Merlevède-Peligrad Thm 2.1/3.1, `2nλ_μ ± 2s√n`) is the correct pillar, and it requires i.i.d. M (census #25 is the open dependent case). + +### R3 · Greedy INFO_GAIN admission has a published Ω(n/log n) lower bound; EC² is the adaptive-submodular repair — CERTIFICATE_ONLY + MACRO_CANDIDATE +- **CLAIM** [G] Every posterior-based greedy admission policy (info gain, VoI) is Ω(n/log n)-suboptimal on a family with uniform priors; the `(1−1/e)` guarantee needs adaptive submodularity, which information gain lacks. +- **PRIMARY SOURCE** Golovin, Krause, Ray, arXiv:1010.3091v2 (NeurIPS 2010; rev. 2013-12-16), Theorems 8–9 + Appendix B; Golovin & Krause, arXiv:1003.3967v5 (JAIR 42, 2011), Theorem 5 and Prop. 2. +- **SPECIFIC RESULT** Construction: `m = 2^q` classes × 2 hypotheses, one test `t₀` reveals `v`, tests `t_k` reveal `1[φ_k(a)=v]` — individually zero information gain until `t₀` has run — plus slow sequential tests and unbounded dummies. Optimal cost `log₂n`; any posterior-based greedy pays `≥ m/2`. Mechanism: **complementarity** — a set of hops is far better than the sum of its parts. EC² (`f_EC = w(⋃ E_t)` over cross-class pairs, `w = P(h)P(h')`) is adaptive submodular, bound `(2 ln(1/p_min) + 1)·c(π*)`. +- **CURRENT MAP** S5 throttle (`c_min`, budget `k`, hub exclusion) + `admit_derived`; `info_gain_u4` ranking; the FIELD axis INFO_GAIN. +- **DESTINATION** CERTIFICATE_ONLY (the throttle inherits no approximation guarantee) + MACRO_CANDIDATE `admit_ec2` (a weighted pair-cut count over the Belnap-partitioned candidate set — registers that already exist; the budget-`k` throttle is exactly Theorem 5's cardinality constraint). +- **ΔH** Moves the frontier's admit rule from "unproven" to "in the proved-bad region" until the EC² certificate runs. +- **MECHANISM CHECK** Multi-hop abductive derivation is exactly the `t_k`-shaped case: individually worthless, jointly decisive. +- **CERTIFICATE** Adaptive-submodularity check over 10⁴ sampled `(ψ ⊆ ψ', t)` triples: 0 violations for `f_EC`, ≥1 exhibited for INFO_GAIN. +- **FALSIFIER** Instantiate the construction at `q=8` (256 classes, 512 hypotheses): optimal 9 hops, posterior-greedy ≥128 expected. Run the shipped frontier; ≤20 hops means it is not posterior-based greedy and the exposure does not apply. +- **MINT CONSEQUENCE** None. Rung-local admit script. + +### R4 · ACCUMULATE is an MV-monoid — CERTIFICATE_ONLY (strengthen), ✔ PROBED +- **CLAIM** [G] `a ⊕ b = min(15, a+b)` on `L₁₆` is associative and commutative (Chang 1958 MV-algebra axioms; Mundici tutorial); it is non-cancellative with absorbing top. +- **CURRENT MAP** `accumulate_children` and the module doc's "recursively composing already-clamped child registers is NOT associative". +- **SPECIFIC RESULT** ✔ PROBED: 0 violations of `(a⊕b)⊕c = a⊕(b⊕c)` over all 4096 triples per side; 1360 `(a,b≠c)` pairs with `a⊕b = a⊕c`. Any DAG fold order gives a bit-identical register; what is lost is *mass* (a clamped 15 means "≥15"), never *order*. +- **DESTINATION** CERTIFICATE_ONLY. Rewrite the caveat as "associative, commutative, monotone, non-cancellative, top-absorbing; saturation understates mass, never converts conflict to silence". +- **ΔH** Licenses schedulers to reassociate hop trees without proof obligation. Area A's assertion that the clamp *causes* non-associativity is refuted by the same probe; what the clamp causes is R5. +- **FALSIFIER** already run; re-runnable as a `#[test]` over `0..16³`. +- **MINT CONSEQUENCE** Doc/contract only. + +### R5 · Per-side clamp is not ratio-preserving: saturation manufactures Contested — CERTIFICATE_ONLY (saturation flag) +- **CLAIM** [G] arithmetic, [H] practical bite. NAL `f = w⁺/w`, `c = w/(w+k)`; independent clamping of `w⁺` and `w⁻` at 15 is not ratio-preserving. +- **PRIMARY SOURCE** Wang NAL (`c = w/(w+k)`), restated Xu arXiv:2607.20902v1 §2.2 and Hammer & Lofthouse ONA (AGI-2020). +- **SPECIFIC RESULT** true `(30,2)` → `f = 0.938`; stored `(15,2)` → `0.882`; as both sides saturate every heavily-evidenced axis drifts to `(15,15)` = Contested. The confidence ceiling `c ≤ 15/16` is AIKR-legal (NAL requires `c < 1`); the frequency drift is not. Interaction with ONA's Assumption-of-Failure (census #19): once `disagree` saturates, no `δ⁺` can outweigh it — an eagerly-pessimistic axis becomes permanently pessimistic. +- **CURRENT MAP** `axis_state` → `Contested` on `(a>0, d>0)`; `contested_mask`; ASKED_CONTESTED ternlog. +- **DESTINATION** CERTIFICATE_ONLY: a Contested read must carry `saturated = (a==15 || d==15)` or is uncertified. Do **not** widen u4→u8 (moves the ceiling, keeps the distortion). +- **FALSIFIER** 30 agree + 2 disagree via repeated `accumulate_children` on one axis → assert the classification is not reported as genuine conflict without the flag. Second arm: 40 predict/confirm cycles with `δ⁻=1, δ⁺=2`; `EXPECT` (R7) must be non-decreasing; under the current clamp it plateaus and, on one failure, drops and never recovers. +- **MINT CONSEQUENCE** None (one derived flag bit; no storage). + +### R6 · Knowledge-order MEET is the one bilattice law the core set cannot express — MACRO_CANDIDATE `MEET_K` +- **CLAIM** [G] (Arieli-Avron 1996; Fitting): an interlaced bilattice needs both `⊕_k` (join, componentwise max = BELNAP_JOIN) and `⊗_k` (consensus, componentwise min). Every interlaced bilattice is `L⊙L` (Avron 1996), so the `(a,d)` pair is the canonical form and the signed net was the non-injective truth-projection (census #18). +- **CURRENT MAP** BELNAP_JOIN only; TERNLOG is boolean over 3 mask columns, so u4 `min` is not a TERNLOG; no saturating subtract to recover `a+b−max`. +- **SPECIFIC RESULT / FALSIFIER** A=(3,0), B=(0,3): BELNAP_JOIN → (3,3) Contested; ACCUMULATE → (3,3); `⊗_k` → (0,0) Silent ("what both sources agree on"). Exhaustive search over length-≤3 compositions of the six calls on the 256×256 pair table for one yielding (0,0) here and (3,3) on ((3,0),(3,0)): expected none. +- **DESTINATION** MACRO_CANDIDATE — rung-local compare-select over nibbles. Not a global opcode. Interlacing certificate (B1 falsifier: `¬, ∧_t, ∨_t` preserve `≤_k` over all 256 pairs) travels with it. Also grounds Mares 2002 (census #16): coherent ⇔ `contest = 0`. +- **MINT CONSEQUENCE** One script; zero axes; zero opcodes. + +### R7 · NAL choice/expectation is a Krichevsky-Trofimov mean the entropy readouts cannot reproduce — MACRO_CANDIDATE `EXPECT` +- **CLAIM** [G] `exp(f,c) = c(f−½)+½ = (w⁺ + k/2)/(w + k)`; with k=1 the Jeffreys/KT posterior mean `(a+½)/(a+d+1)`. +- **PRIMARY SOURCE** Hammer & Lofthouse, ONA (AGI-2020), verbatim definition of `exp`. +- **CURRENT MAP** belief-arena CHOICE path (CR #11, ASC #7 overlap fallback) — ordering key not pinned to a formula. STANCE_ENTROPY is symmetric in `a↔d`: `(12,3)` and `(3,12)` have equal stance entropy, equal info gain, `exp` 0.78 vs 0.22. +- **DESTINATION** MACRO_CANDIDATE. Integer-safe: order by `(2a+k)(w'+k)` vs `(2a'+k)(w+k)` — a u8 cross-multiply, no division. `k` is an operand (coupled to the ceiling in R5), not a global constant. +- **FALSIFIER** (i) `exp(a,d) == (a+0.5)/(a+d+1)` over the u4 grid; (ii) anti-vacuity: find a pair with equal STANCE_ENTROPY and equal INFO_GAIN and different `exp`, assert no choice rule over those two ops separates it. +- **MINT CONSEQUENCE** No classid. Also the required ingredient for census #21 (specificity preemption) and #23 (choice-on-overlap fallback). + +### R8 · AMBIGUITY ≠ INFO_GAIN, with a witness pair — GROUNDING_ONLY (axis stands) +- **CLAIM** [G] Corva, arXiv:2607.20306v1 (2026-07-22) Remark 4 / Example 1: in linear-Gaussian active inference with state-dependent observation noise, `ε_k(π) = ε_k(π')` for every policy pair (equal information gain, a log-det **ratio**) while ambiguity `½ ln det(2πe R)` differs (a log-**det**). Plus Koudahl-Kouw-de Vries 2021: under additive control and fixed noise EIG is *constant* across policies (census #31 → a flat-frontier assertion). +- **CURRENT MAP** FIELD::AMBIGUITY vs FIELD::INFO_GAIN. +- **DESTINATION** GROUNDING_ONLY; retires "AMBIGUITY duplicates INFO_GAIN". Two-sided certificate: a pair with equal INFO_GAIN/unequal AMBIGUITY (Remark 4) and a pair with equal AMBIGUITY/unequal INFO_GAIN (halve a clean candidate set: 1 bit gain, ambiguity unchanged). +- **FALSIFIER** Scalar model `A=B=C=Q=1, Σ₀=1, R(x)=1+x²`: `u=0` → gain 0.549 nats, ambiguity 1.419; `u=2` → gain 0.168, ambiguity 2.224; then the Remark-4 level-set arm. +- **MINT CONSEQUENCE** None. (Companion collapses: NOVELTY = `½(1/a − 1/a₀)` over Dirichlet counts = a script over REVISION/ACCUMULATE registers, census #13; pragmatic value = consumer prior `C`, census #14.) + +### R9 · Hambly-Lyons Theorems 2/3 green Pillar 11 for lattice walks and kill the fixed-depth Index regime — CERTIFICATE_ONLY +- **CLAIM** [G] (theorem as read by the auditor in math/0507536v2 §2.4; the constant must be re-read on the main thread before the pillar flips). For a length-`L` path on the 2-d integer lattice, vanishing of the first `⌊e·log(1+√2)·L⌋ = ⌊2.3959·L⌋` iterated integrals implies tree-likeness (Thm 2); in `R^d`, `⌊(2⌈log₃(d/2)⌉+3)·2.3959·L⌋` (Thm 3). The GL(2,C)-projected integrals carry less than the full tensor algebra, so the full truncated signature satisfies it a fortiori. +- **SPECIFIC RESULT** `S^{(N)}` is a homomorphism into the free nilpotent group `G^N`, so `S^{(N)}(X) = S^{(N)}(Y) ⟺ S^{(N)}(X ⋆ Y^{-1}) = 1`; apply Thm 2/3 to the concatenation: **`N ≥ ⌈c(d)·(|X|+|Y|)⌉`** is a complete two-sided certificate for unit-step lattice walks. +- **CURRENT MAP** `jc::hambly_lyons` (cites Thm 1/Cor 1.5 only — correct, depth-∞, insufficient); `sigker` `CodecRoute::Sigker` Index regime; the `E-V3-FACET-4-PLUS-12` rails as carrier. +- **DESTINATION** CERTIFICATE_ONLY. The auditor proposed CORE_PRIMITIVE_CANDIDATE; **overruled on the main thread**: this greens a *held* primitive (the operator's stated highest-value outcome), it mints nothing new, and the Index regime it certifies is length-parameterized, so `sigker` must carry a walk-length budget and escalate beyond it. Preconditions before flipping: (a) `d ≥ 2` — a `u8:u8` rail read as one scalar axis is d=1 and collapses to the endpoint (census D3); the canon "u8:u8 is two bytes, never widened" is load-bearing here; (b) steps must be unit basis-aligned lattice steps — Thm 2's hypothesis is literally `‖x_k − x_{k+1}‖ = 1` on `Z^{|A|}`; arbitrary quantized vectors are outside it. +- **ΔH** Eliminates "no finite-depth Hambly-Lyons exists" and "depth 2 suffices" simultaneously. The depth-2 forward leg (census D2, ✔ PROBED) is a necessary condition only; the 1e6 discrimination ratio is a scale artifact until Λ-normalized (D6). +- **FALSIFIER** Enumerate reduced/unreduced word pairs on 2 generators up to L=6; assert `S^{(⌈2.3959·2L⌉)}` (exact rational arithmetic on basis exponentials) separates every non-tree-equivalent pair and merges every tree-equivalent pair; re-run at depth 2 and count false merges (expect many; the figure-eight is one). +- **MINT CONSEQUENCE** No new concept. Pillar 11 may flip green *for the lattice-walk class* once the constant is re-read and the two preconditions are asserted in `sigker`; the fixed-depth wording is retired in place. + +--- + +## 3. MINT NOW +**EMPTY.** No result survived both the composition test and the mechanism test with a new executable address attached. + +## 4. MACROS WORTH PROBING (rung-local loco/R2IL scripts; no global opcode) +| macro | what | composition | probe first | +|---|---|---|---| +| `SANDWICH_BUDGET` | R2 replacement for `pillar_5plus_bound` | running `2·Σ‖log M_k‖_F` (2×2 closed form `√((ln λ₁)²+(ln λ₂)²)`) | aligned-M arm + `det(M)>eps` gate | +| `MEET_K` | knowledge-order consensus | per-nibble min over the pair | interlacing check over 256 pairs; non-expressibility search | +| `EXPECT` | NAL choice key | `(2a+k)(w'+k)` cross-multiply | R7 falsifiers (i),(ii) | +| `admit_ec2` | adaptive-submodular frontier admission | weighted pair-cut count over Belnap-partitioned candidates, under budget `k` | R3 construction at q=8; submodularity triples | +| `sprt_stop` | theorem-backed stopping (Wald-Wolfowitz 1948) | TERNLOG over (`cum_llr < ln B`, `> ln A`, budget) on an ACCUMULATE'd log-odds | `(α,β)=(0.05,0.05)` → `E[N] ≈ 5.9` at ±0.5 nats/hop vs fixed k=20 | +| `PROJECT` | NARS temporal projection | right-shift both nibbles by `n` (`λ = 2^-n`) before ACCUMULATE | `f` preserved within 1 LSB, `c` strictly decreasing | +| `NOVELTY` | parameter info gain | `½(1/agree − 1/total)` over REVISION/ACCUMULATE | hop α (1/10) → 0.450, hop β (9/10) → 0.0056 at equal INFO_GAIN | +| `Λ` (tensor normalization) | Chevyrev-Oberhauser Def. 12 | dilation `δ_c` with `ψ` injective | triangle scaled ×{0.1,1,10}: ratio stable only when normalized | +| `flat_frontier_assert` | Koudahl degenerate regime detector | `stddev(info_gain_u4)` over admitted frontier `> 0` | 32 candidates each 4096→2048 | + +## 5. CERTIFICATES TO HARVEST (green or falsify an existing pillar/claim) +1. **Pillar 11 green path** — Hambly-Lyons Thm 2/3 (math/0507536v2 §2.4) + homomorphism into `G^N`; re-read the constant `e·log(1+√2)`; assert `d ≥ 2` and unit-lattice steps in `sigker`; retire fixed depth 2 (necessary-condition only). Companion: Salvi et al. Thm 15 (O(h²)) certifies the 2e-7 floor but Thm 8 needs C¹ — write the segment-wise Chen lemma; add a minimum-loop-scale precondition (figure-eight `dev ∝ ε⁶` sinks under the floor). +2. **Pillar 5+ scope** — keep `jc/koestenberger.rs` green for inductive means; strike "per Pillar 5+ / K-S" from `sigma_propagation::pillar_5plus_bound`; relabel it as the jc generator's empirical CV curve; fix `sigma_tension_u4` units via R2. If a stochastic pillar is wanted later: Cuny-Dedecker-Merlevède-Peligrad arXiv:2110.10937v2 Thm 2.1/3.1 (i.i.d. M only; the dependent case is OPEN and is the live one). +3. **ACCUMULATE contract** — associative/commutative/non-cancellative/top-absorbing (R4, probed); saturation flag on Contested reads (R5); `δ⁺ > δ⁻` post-clamp for Assumption-of-Failure (census #19). +4. **Frontier admission** — Golovin-Krause-Ray Thm 9 lower bound; EC² adaptive-submodularity as the repair (R3); Koudahl flat-EIG detector (#31). +5. **STANCE_ENTROPY never gates alone** — permutation invariance over {T,F,B,N} (census #7): pair it with mean `contest` or `silent_mask`. +6. **Stamp wording** — disjointness certifies "no evidence item counted twice", not independence (census #23); confirm the arena's choice-on-overlap fallback exists and uses `EXPECT`. +7. **Recipe 12 TCA** — drop "Granger" (rhyme); relabel "temporal precedence induction"; re-check its rung delta (#22). +8. **INFO_GAIN contract text** — `= Lindley EIG` for uniform posteriors; u4 cap = ratio 2¹⁵ with one-sided silent saturation (expose a flag); Miller-Madow only where counts are sampled (#30). +9. **SIGMA_TENSION ladder** — after (2): re-index the u4 as a Cantelli/Chebyshev tail class (`q=7 ↦ k=1.75 ↦ p ≤ 0.327` today; proposed `q=15 ↦ k=4.472 ↦ p ≤ 0.05`) — CODEBOOK_VALUE (#26). + +## 6. V3 SURVIVES (proposed novelties that collapse into the 24 axes or the six calls) +- **NAL revision** → ACCUMULATE (bijection `⟨f,c⟩ ↔ (w⁺,w⁻)` for c<1; census #9). +- **Subjective-logic cumulative fusion** → ACCUMULATE; base rate → per-axis `prior_u4` in the BasinCodebook (#15). +- **Mares paraconsistent coherence** → `contest = 0` (#16). +- **Shramko-Wansing truth/falsity orders** → the two components; permits asymmetric per-side ops (#29). +- **Novelty / parameter info gain** → script over REVISION + ACCUMULATE (#13). +- **Pragmatic value** → consumer codebook prior, not an axis (#14). +- **Anticipation / negative evidence on failed prediction** → `FALSIFIER.disagree += δ⁻` then `agree += δ⁺` (#19); the loop is control-plane. +- **Typicality / defaults / specificity preemption** → IS_A depth → `EXPECT` → choice; Nixon diamond → Contested (#21). Reiter extension *sets* are the one thing not expressible, deliberately. +- **Allen interval relations** → ValueCodebook operand on TEKAMOLO, never an opcode (#20). +- **Syllogistic chaining** → exact NARS carrier (`truth.rs` products, ✔ read); the six calls are a pooling algebra and are meant to be (#11). +- **SPRT** → TERNLOG over an ACCUMULATE'd log-odds (#12). +- **AMBIGUITY** stands as its own axis (R8) — a survival in the other direction. + +## 7. V4 PRESSURE (irreducible dimensions, with witness pair) +- **Conative pair (desire, aversion) — blocked on a scope ruling, not on evidence.** Two independent sources converge: NSM's prime WANT (Area F) and Xu 2026 (arXiv:2607.20902v1, Thm 4: `G¡ ≡ G ⇒ ¬D̃ ≡ ¬(G ⇒ D̃)`; "avoid G" ≠ "pursue ¬G"). **Witness pair:** the light-press case — P1/P2/G1 with identical evidence on every one of the 24 axes (all are evidence-about-propositions), where "avoid hurt" and "pursue not-hurt" are indistinguishable in v3 yet the lawful downstream action differs (press vs not press). **Mechanism fence:** modelling aversion as `disagree` on an evidence axis is exactly the paradox's assumption A3 — if ever minted it is a *separate* pair, never an evidence lobe. **Ruling needed:** is the basis epistemic-only? If yes → REJECT permanently and record why; goal handling then lives in `ActionDef`/kanban, outside the basis. +- Nothing else survived the witness test: MIS-inconsistency (relational, in premise ancestry; #17), novelty (#13), pragmatic value (#14), a third bilattice order (#29) all collapsed. + +## 8. DO NOT MINT +- **"Granger"** on recipe 12 — a residual-variance test NARS does not compute (#22). +- **A Hambly-Lyons axis or fixed-depth signature primitive** — the certificate is length-parameterized; a depth-2 Index regime is falsified by the paper's own figure-eight (D2, probed). +- **Iterated-sums signature** as the discrete signature — quotients by time-warping, retains tree-like excursions, no group, no injectivity (D8). Separate discovery for stutter walks only. +- **An inconsistency-measure axis** — `I_MI` is not a function of per-axis `(a,d)` (#17). +- **A "novelty" or "epistemic value" scalar** — reducible (#13, #14). +- **u4→u8 widening** to fix saturation — moves the ceiling, keeps the ratio distortion (R5). +- **A seventh core opcode for MEET/EXPECT/SYLLOG/SPRT** — all rung-local scripts. +- **CAN (ability/affordance)** — one source, no mechanism (#33). +- **Factorial tail decay as a losslessness argument** — bounds magnitude, not discrimination (D7). +- **"EWA" as a name for the congruence** — three operations share the word (#27). + +--- + +### Method notes +- Five Opus auditors (A+F, B, C, D, E), alphaXiv + WebFetch, theorems read in source. Area D's first run died on an API error and was relaunched with the same brief. +- Main-thread adjudication overrode two auditor destinations: D's CORE_PRIMITIVE_CANDIDATE → CERTIFICATE_ONLY (greening a held primitive is the higher-value, lower-entropy outcome); A's "the clamp causes non-associativity" → refuted by the exhaustive probe, retained as ratio distortion (R5). +- Local probes (scratchpad, not committed): L₁₆ associativity (4096 triples), sandwich isometry bound (2000 paths), aligned-M growth, figure-eight depth-2/depth-3 signature. Each is small enough to become a `#[test]` in the crate it certifies. +- Zero code changed by this harvest. Board hygiene: one EPIPHANIES entry for the two corrections (Pillar 5+ scope, Pillar 11 green path); SUPERSESSION-INDEX regenerated last. From 7751581f71edc4c298d209a59edcabbfbaffe271 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 20:39:48 +0000 Subject: [PATCH 2/5] jc: Pillar 11 green for lattice walks (Theorem 2 leg) + pre-#1129 register audit pins MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Hambly-Lyons math/0507536v2 §2.4 Theorem 2/3 re-read from the primary source: a lattice word of length L is separated from the identity at depth floor(e·ln(1+√2)·L) = floor(2.3958·L). New W6 leg in jc::hambly_lyons (gated, default build stays zero-dep): 484/484 reduced words of length <= 5 separated at the theorem depth; 64 tree-like words at the identity (2e-15); 64 reduced length-8 words share S^(2) = 1 with the constant path and all separate by depth 3 <= floor(c·8) = 19; d = 1 collapses to exactly 7 classes. Disable arm (cap the separation search at depth 2) fails the test. sigker's Index regime re-worded as length-parameterized; depth 2 is a necessary condition only. epistemic_bassin: source audit of the superseded signed lane — true i4 over [-8, 7], "-3..+3" was prose only, the #1129 failure is dimensional (every magnitude 1..7 nets to SILENT). Adds const width pins (size_of == 24 == 2·CASCADE_UNITS), the universal-magnitude balanced-conflict test, and the exhaustive associativity / non-cancellativity census; corrects the module caveat (sum-then-clamp is an MV-monoid, associative across hops; the clamp costs cancellativity). Board: one EPIPHANIES entry; LATEST_STATE line; SUPERSESSION-INDEX regenerated last. Verified in a scratch standalone workspace (the in-tree workspace cannot load here: the ndarray sibling is absent). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QHVUi6Q9XtmKgxh6pDRayP --- .claude/board/EPIPHANIES.md | 48 +++ .claude/board/LATEST_STATE.md | 1 + ...literature-harvest-2026-09-01-post-1132.md | 2 +- crates/jc/src/hambly_lyons.rs | 286 +++++++++++++++++- .../src/epistemic_bassin.rs | 94 +++++- crates/sigker/src/codec.rs | 19 +- crates/sigker/src/lib.rs | 4 +- 7 files changed, 438 insertions(+), 16 deletions(-) diff --git a/.claude/board/EPIPHANIES.md b/.claude/board/EPIPHANIES.md index 80f7bd028..222330752 100644 --- a/.claude/board/EPIPHANIES.md +++ b/.claude/board/EPIPHANIES.md @@ -1,3 +1,51 @@ +## 2026-09-01 — E-PILLAR-11-GREEN-FOR-LATTICE-WALKS-LENGTH-PARAMETERIZED-1 + +**Status:** SHIPPED (jc W6 leg, `hambly_lyons.rs`; sigker Index regime +re-worded; harvest ledger D1–D8). **Confidence:** [G] — the constant was +re-read from the primary source (math/0507536v2 p.11/p.14) on the main +thread, the leg is exhaustive over its word classes, and its disable arm +fails. + +Pillar 11 was red because Theorem 1 is depth-∞. The finite-depth statement +is Theorem 2/3 of the SAME paper: a lattice word of length L is separated +from the identity by depth ⌊e·ln(1+√2)·L⌋ = ⌊2.3958·L⌋ (d = 2; × +(2⌈log₃(d/2)⌉+3) in general). Homomorphism into the free nilpotent group +gives the pair form `S^(N)(X) = S^(N)(Y) ⟺ X ∼ Y` at `N ≥ ⌊c·(|X|+|Y|)⌋`. +Measured (W6, release, 2.0 s): 484/484 reduced words of length ≤ 5 +separated at ⌊c·L⌋ (min ‖S−1‖ = 1.118); 64 tree-like words at the +identity (max 2e-15); **64 reduced length-8 words share `S^(2) = 1` with +the constant path** (the paper's own §1.6 figure-of-8 class) and every one +separates by depth 3 ≤ ⌊c·8⌋ = 19; d = 1 collapses the 64 length-6 words +to exactly 7 signature classes (net increment only — the `d ≥ 2` +precondition). Consequences: the sigker Index regime is **length- +parameterized** (a walk-length budget, escalate or refuse beyond it), +depth 2 is a necessary condition only, a single `u8:u8` rail read as one +axis is out of regime, and arbitrary quantized step vectors stay outside +Theorem 2 (Theorem 9 gives non-triviality without an explicit depth). +Default jc build stays zero-dep/DEFERRED. + +**Companion source audit (pre-#1129 signed register), same session:** the +old `BasinLanes` lane was true two's-complement i4 over the FULL `[−8, 7]` +(`atoms::I4x32::sext4`; 16 states, no quantizer); "−3..+3" is prose only — +one illustrative pair, absent from every implementation, test and commit +(`git log -S` negative). The #1129 failure is DIMENSIONAL, not range: the +transcribed old encoder maps `+x + (−x)` to bytes identical to `SILENT` for +every `x ∈ 1..=7`; only `x = 8` escapes, by the `+8 → +7` clamp artifact. +Bit accounting: old 24×4 = 96 bit = 12 B (one facet payload, pinned +against `CASCADE_UNITS`); new 24×(4+4) = 192 bit = 24 B — now pinned by +`const` asserts and a universal-magnitude test in `epistemic_bassin.rs`. +No jc pillar certifies a compact projection it did not test: the A→B +adapters (`sigma_tension_u4`, D-SK casts, causal-witness loci) are all +labelled unproven and gated. Two wording risks for the operator: +`epistemic_bassin.rs` line 18 ("one extra 12-byte register") vs line 61 +("a reading of the SAME physical lane") cannot both size one row; and +`PR_ARC_INVENTORY.md` ~1688 summarises `probe_tarski_signed_witness` as a +"24×i4 signed derivational field" although its polarities live in two +separate slots (`ConstructiveDepth`/`FalsifyingDepth`) and never net. +Also corrected: the ACCUMULATE caveat ("NOT associative") — sum-then-clamp +on L₁₆ is an MV-monoid, associative across hops; the clamp costs +cancellativity only (0/4096 violations, 1360 non-cancel pairs, pinned). + ## 2026-09-01 — E-LITERATURE-HARVEST-POST-1132-TWO-PILLAR-CORRECTIONS-1 **Status:** HARVEST (5-auditor literature sweep, adjudicated against shipped diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index 332e4e2fa..c1493ebd9 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,4 +1,5 @@ ## 2026-09-01 — branch (PR pending): D-DCR-2b EpistemicBassin24 — CONTRACT INVENTORY DELTA +- `jc::hambly_lyons` **Pillar 11 GREEN for lattice walks — length-parameterized (W6, 2026-09-01)**: Theorem 2 lattice leg added (Hambly-Lyons math/0507536v2 §2.4, `c = e·ln(1+√2) = 2.3958`, re-read from the primary source): all 484 reduced words of length ≤ 5 separated at depth ⌊c·L⌋, 64 tree-like words at the identity (2e-15), 64 depth-2 false merges among length-8 reduced words all separated by depth 3 ≤ ⌊c·8⌋ = 19, d = 1 collapses to exactly 7 signature classes (the `d ≥ 2` precondition). `sigker` Index regime re-worded: lossless on the tree-quotient ONLY under a walk-length budget `N ≥ ⌊c(d)·(|X|+|Y|)⌋`; depth 2 is necessary-only. Default build stays zero-dep/DEFERRED. Still red for non-lattice quantized step vectors (Thm 9 gives non-triviality without an explicit depth). - `lance_graph_contract::epistemic_bassin::{EpistemicBassin24, AxisState, BASIS_AXES(24), BASIS_PAIR_BYTES(24), AXIS_COUNT_MAX(15), info_gain_u4, sigma_tension_u4}` — the field map's value carrier as an `agree_u4[24] + disagree_u4[24]` PAIR (operator co-architect ruling: the signed net was FALSIFIED — `+3 + −3 = 0` collapsed balanced conflict into silence). Net/polarity/contest/entropy DERIVED; `Contested` is a first-class state that survives one-hop accumulation. Readout adapters grounded in shipped certificates: `info_gain_u4` (Shannon ΔH over candidate counts), `sigma_tension_u4` (quarters of `sigma_propagation::pillar_5plus_bound`; 7 = the 1.75× PASS slack); Hambly-Lyons has NO lane (sigker classification gated on jc Pillar 11, DEFERRED). **No storage minted**: the loci-never-magnitude law is scoped to the A9 READING, not tenant 14's bytes — the bassin is a classid-selected reading of the same physical lane; a separate tenant waits for one real row needing both readings simultaneously (an `EpistemicWitness = 16` mint was built and discarded uncommitted on this ruling). - `epistemic_bassin` Belnap layer — `AXIS_MASK_ALL` + `{support_mask, refute_mask, contested_mask, silent_mask}` (u64, bits 0..24): the two-bit-per-axis Belnap/FDE encoding of the four axis states (K3 as its contested-free restriction); knowledge-join = bitwise OR = provably `accumulate_children`'s state layer (pinned). Composes with `revision::EvidenceMask for u64` for bit-parallel kind-3 question masking; asked-but-silent = the missing-link query in one op. diff --git a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md index c141587d9..5ac2e79a8 100644 --- a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md +++ b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md @@ -32,7 +32,7 @@ | # | area | result | destination | ΔH | status | |---|---|---|---|---|---| -| D1 | D | Hambly-Lyons **Theorem 2/3** (math/0507536v2 §2.4): a lattice path of length L whose first ⌊e·log(1+√2)·L⌋ = ⌊2.3959·L⌋ iterated integrals vanish is tree-like (d=2); general d: ⌊(2⌈log₃(d/2)⌉+3)·2.3959·L⌋. Truncated signature is a homomorphism into G^N, so `S^(N)(X)=S^(N)(Y) ⟺ X∼Y` at `N ≥ ⌈c(d)·(|X|+|Y|)⌉` for unit-step lattice walks | **CERTIFICATE_ONLY — the green path for Pillar 11**, length-parameterized | highest | auditor read §2.4; constant to be re-read before greening | +| D1 | D | Hambly-Lyons **Theorem 2/3** (math/0507536v2 §2.4): a lattice path of length L whose first ⌊e·log(1+√2)·L⌋ = ⌊2.3959·L⌋ iterated integrals vanish is tree-like (d=2); general d: ⌊(2⌈log₃(d/2)⌉+3)·2.3959·L⌋. Truncated signature is a homomorphism into G^N, so `S^(N)(X)=S^(N)(Y) ⟺ X∼Y` at `N ≥ ⌈c(d)·(|X|+|Y|)⌉` for unit-step lattice walks | **CERTIFICATE_ONLY — Pillar 11 FLIPPED GREEN for lattice walks**, length-parameterized | highest | ✔ constant re-read from math/0507536v2 p.11/p.14 on the main thread; W6 leg shipped in `jc/hambly_lyons.rs` (484/484 reduced words separated, 64 tree-like at 2e-15, 64 depth-2 false merges all separated by depth 3, d=1 → 7 classes; disable arm fails) | | D2 | D | The depth-2 forward leg tests membership in `ker(G^∞→G²)`, not tree-likeness: the §1.6 figure-eight has S¹=S²=0 like the out-and-back but S³≠0 | **REJECT** depth-2 as Index regime (necessary condition only) | high | ✔ PROBED (S¹¹²: fig-8 = 1.0, out-and-back = 0.0) | | 1 | E | `pillar_5plus_bound` cites a theorem about the inductive mean of independent samples (K-S Thm 1) to certify a congruence orbit; `sigma_tension_u4` divides a squared distance by a dimensionless CV | **CERTIFICATE_ONLY (falsifies)** | high | ✔ PROBED (code read; aligned-M arm) | | 2 | E | Replacement: deterministic isometry bound `|‖log Σ_n‖_F − ‖log Σ_0‖_F| ≤ 2·Σ‖log M_k‖_F` for any invertible symmetric M | **MACRO_CANDIDATE** (composition of `logm` + Frobenius) | high | ✔ PROBED (max ratio 0.567 on 2000 random 20-hop paths) | diff --git a/crates/jc/src/hambly_lyons.rs b/crates/jc/src/hambly_lyons.rs index 2f399c271..8d0dd2125 100644 --- a/crates/jc/src/hambly_lyons.rs +++ b/crates/jc/src/hambly_lyons.rs @@ -24,6 +24,53 @@ //! visits node X and returns conveys no information beyond visiting the //! start point; the signature respects that. //! +//! # Status — GREEN for lattice walks, length-parameterized (2026-09-01, W6) +//! +//! The pillar was red because Theorem 1 is a depth-∞ statement and the +//! substrate truncates. The finite-depth certificate is in the SAME paper, +//! two sections later (math/0507536v2 §2.4, constant re-read on the main +//! thread against the primary source): +//! +//! **Theorem 2.** A path of length L on the 2-d integer lattice whose +//! first ⌊e·log(1+√2)·L⌋ GL(2,C)-iterated integrals vanish is tree-like +//! and its reduced word is trivial. (e·ln(1+√2) = 2.3958…) +//! +//! **Theorem 3.** In the d-dimensional lattice the depth is +//! ⌊(2⌈log₃(d/2)⌉ + 3)·e·log(1+√2)·L⌋. +//! +//! The GL(2,C) integrals are a projection of the tensor-algebra ones +//! (fn. 2: "a priori contain less information"), so vanishing of the FULL +//! truncated signature to that depth implies the hypothesis a fortiori. +//! Because the truncated signature is a homomorphism into the free +//! nilpotent group, the pair form is +//! +//! S^(N)(X) = S^(N)(Y) ⟺ X ∼ Y for N ≥ ⌊c(d)·(|X|+|Y|)⌋, +//! +//! i.e. the Index regime is LENGTH-PARAMETERIZED: a consumer must carry a +//! walk-length budget and escalate depth (or refuse) beyond it. Depth 2 is +//! a NECESSARY condition only — the paper's own §1.6 figure-of-8 has +//! S¹ = S² = 0 and is not tree-like; the W6 leg below finds 64 such reduced +//! words at length 8 and separates every one by depth 3. +//! +//! Preconditions, both pinned executably in the W6 leg: +//! * `d ≥ 2` — in d = 1 the reduced-path group is Z (Diehl-Ebrahimi-Fard- +//! Tapia Rem. 1.4: every closed 1-d path is tree-like), so a single +//! `u8:u8` rail read as ONE scalar axis carries only its net increment; +//! * unit basis-aligned steps on the integer lattice (p.8: +//! ‖x_k − x_{k+1}‖ = 1, x_k ∈ Z^{|A|}). Arbitrary quantized step vectors +//! are OUTSIDE Theorem 2; for those the applicable statement is +//! Theorem 9 (piecewise-linear, bound in the smallest angle and the +//! shortest edge) which gives non-triviality but no explicit depth. +//! +//! What stays honest: the depth-2 legs certify a necessary condition and +//! the Lévy-area functional form; the depth-∞ PDE leg reads, to leading +//! order, the same Lévy area (dev ≈ ½‖S²‖²) — so it is a second resolution +//! of the same measurement, not independent evidence. Unnormalized +//! truncated features are not characteristic (Chevyrev-Oberhauser 2022 +//! Thm 21 / Rem. 4); the discrimination RATIO below is scale-dependent and +//! is kept as a regression guard, not a discrimination bound. Ledger: +//! `.claude/knowledge/literature-harvest-2026-09-01-post-1132.md` (D1–D8). +//! //! # Activation gate //! //! Active under `--features hambly-lyons` (default: off, JC stays zero-dep). @@ -303,6 +350,207 @@ mod active { } } + // ── W6: the Theorem 2 lattice leg (the finite-depth certificate) ──────── + // + // Hambly-Lyons math/0507536v2 §2.4, Theorem 2 (re-read on the main + // thread 2026-09-01): a lattice path of length L on Z² whose first + // ⌊e·log(1+√2)·L⌋ GL(2,C)-iterated integrals vanish is tree-like and its + // reduced word is trivial. The GL(2,C) integrals are a projection of the + // tensor-algebra ones ("a priori contain less information", fn. 2), so + // vanishing of the FULL truncated signature to that depth implies it a + // fortiori. The truncated signature is a homomorphism into the free + // nilpotent group, so for two words w, v the pair statement is + // S^(N)(w) = S^(N)(v) ⟺ S^(N)(w·v⁻¹) = 1 with N = ⌊c·(|w|+|v|)⌋ — this + // leg therefore tests single words z = w·v⁻¹ of the combined length. + // + // Hypotheses that make the certificate apply, both pinned below: + // * unit basis-aligned steps on the integer lattice (Def. of lattice + // path, p.8: ‖x_k − x_{k+1}‖ = 1, x_k ∈ Z^{|A|}); + // * d ≥ 2 — in d = 1 the reduced-path group is Z (net increment only, + // every closed path is tree-like), so the quotient carries nothing. + /// `e · ln(1 + √2)` — Theorem 2's constant, computed rather than retyped. + fn hl_theorem2_constant() -> f64 { + std::f64::consts::E * (1.0 + 2f64.sqrt()).ln() + } + /// The depth Theorem 2 needs for a word of length `l` (floor, as stated). + fn hl_theorem2_depth(l: usize) -> usize { + (hl_theorem2_constant() * l as f64).floor() as usize + } + /// Longest word the exhaustive theorem arm enumerates. Depth ⌊c·5⌋ = 11 + /// in d = 2 is 4096 coefficients — cheap enough for a debug test. + const LATTICE_L_MAX: usize = 5; + /// Length at which the depth-2 false-merge search runs. The paper's own + /// §1.6 figure-of-8 (two equal, opposite lobes) lives here: ⌊c·8⌋ = 19. + const LATTICE_FALSE_MERGE_L: usize = 8; + const LATTICE_N_TREELIKE: usize = 64; + /// Exactness tolerance: signatures of lattice words are rationals with + /// k! denominators; f64 products of a handful of exponentials round at + /// ~1e-15, and a genuinely nonzero coefficient is ≥ 1/k! ≥ 1/19!. + const LATTICE_EPS: f64 = 1e-12; + + /// Letters a, b, a⁻¹, b⁻¹ as 0..4; inverse is `(l + 2) % 4`. + fn letter_step(l: u8) -> [f64; 2] { + match l { + 0 => [1.0, 0.0], + 1 => [0.0, 1.0], + 2 => [-1.0, 0.0], + _ => [0.0, -1.0], + } + } + fn lattice_path(word: &[u8]) -> Vec> { + let mut p = vec![vec![0.0, 0.0]]; + for &l in word { + let s = letter_step(l); + let last = p.last().unwrap(); + p.push(vec![last[0] + s[0], last[1] + s[1]]); + } + p + } + fn is_reduced(word: &[u8]) -> bool { + word.windows(2).all(|w| (w[0] + 2) % 4 != w[1]) + } + fn distance_from_identity(word: &[u8], depth: usize) -> f64 { + let s = signature_truncated(&lattice_path(word), depth); + signature_distance(&s, &Signature::identity(2, depth)) + } + /// Every word of exactly `len` letters over the 4-letter alphabet. + fn for_each_word(len: usize, mut f: impl FnMut(&[u8])) { + let total = 4usize.pow(len as u32); + let mut w = vec![0u8; len]; + for code in 0..total { + let mut c = code; + for slot in w.iter_mut() { + *slot = (c % 4) as u8; + c /= 4; + } + f(&w); + } + } + /// A tree-like word: grow from empty by inserting `c c⁻¹` at random + /// positions — the generator of tree-like equivalence (Def. 2.1). + fn treelike_word(state: &mut u64, len: usize) -> Vec { + let mut w: Vec = Vec::with_capacity(len); + while w.len() + 2 <= len { + let c = (splitmix64(state) % 4) as u8; + let pos = (splitmix64(state) as usize) % (w.len() + 1); + w.insert(pos, c); + w.insert(pos + 1, (c + 2) % 4); + } + w + } + + struct LatticeLeg { + /// reduced non-empty words of length ≤ L_MAX checked at ⌊c·L⌋ + reduced_checked: usize, + /// how many of them the theorem depth FAILED to separate (must be 0) + reduced_merged: usize, + /// min ‖S − 1‖ over those words at the theorem depth + reduced_min_dist: f64, + /// tree-like words checked; max ‖S − 1‖ (must sit at f64 rounding) + treelike_checked: usize, + treelike_max_dist: f64, + /// reduced words of length FALSE_MERGE_L that depth 2 cannot separate + depth2_false_merges: usize, + /// the largest depth any of those needed to separate (≤ ⌊c·L⌋) + false_merge_max_sep_depth: usize, + /// how many of them stayed merged even at the theorem depth (must be 0) + false_merge_unresolved: usize, + /// d = 1 fence: distinct signature classes among all 2^6 words on + /// {a, a⁻¹} of length 6 — must be exactly 7 (net increment −6..6) + d1_classes: usize, + } + + fn lattice_leg() -> LatticeLeg { + // Arm 1 — the theorem: reduced ⟹ separated at ⌊c·L⌋. + let mut reduced_checked = 0usize; + let mut reduced_merged = 0usize; + let mut reduced_min_dist = f64::INFINITY; + for len in 1..=LATTICE_L_MAX { + let depth = hl_theorem2_depth(len); + for_each_word(len, |w| { + if !is_reduced(w) { + return; + } + let d = distance_from_identity(w, depth); + reduced_checked += 1; + if d < LATTICE_EPS { + reduced_merged += 1; + } + reduced_min_dist = reduced_min_dist.min(d); + }); + } + + // Arm 2 — tree-like words collapse to the identity at the same depth. + let mut state: u64 = 0x5EED_1A77_1CE0_0001; + let mut treelike_max_dist = 0.0f64; + let mut treelike_checked = 0usize; + for i in 0..LATTICE_N_TREELIKE { + let len = 2 + 2 * (i % 3); // 2, 4, 6 + let w = treelike_word(&mut state, len); + let depth = hl_theorem2_depth(len.max(1)); + treelike_max_dist = treelike_max_dist.max(distance_from_identity(&w, depth)); + treelike_checked += 1; + } + + // Arm 3 — depth 2 is NOT the Index regime: find reduced words of + // length FALSE_MERGE_L with S^(2) = 1, then show each separates by + // the theorem depth (and record how deep it had to go). + let theorem_depth = hl_theorem2_depth(LATTICE_FALSE_MERGE_L); + let mut depth2_false_merges = 0usize; + let mut false_merge_max_sep_depth = 0usize; + let mut false_merge_unresolved = 0usize; + for_each_word(LATTICE_FALSE_MERGE_L, |w| { + if !is_reduced(w) || distance_from_identity(w, 2) >= LATTICE_EPS { + return; + } + depth2_false_merges += 1; + let mut separated_at = None; + for depth in 3..=theorem_depth { + if distance_from_identity(w, depth) >= LATTICE_EPS { + separated_at = Some(depth); + break; + } + } + match separated_at { + Some(d) => false_merge_max_sep_depth = false_merge_max_sep_depth.max(d), + None => false_merge_unresolved += 1, + } + }); + + // Arm 4 — the d = 1 fence: 2^6 words on {a, a⁻¹}, signatures keyed + // by their level-1..3 coefficients rounded to 1e-9. + let mut classes: Vec<[i64; 3]> = Vec::new(); + for code in 0..64u32 { + let mut p = vec![vec![0.0f64]]; + for bit in 0..6 { + let step = if (code >> bit) & 1 == 0 { 1.0 } else { -1.0 }; + let last = p.last().unwrap()[0]; + p.push(vec![last + step]); + } + let s = signature_truncated(&p, 3); + let key = [ + (s.levels[1][0] * 1e9).round() as i64, + (s.levels[2][0] * 1e9).round() as i64, + (s.levels[3][0] * 1e9).round() as i64, + ]; + if !classes.contains(&key) { + classes.push(key); + } + } + + LatticeLeg { + reduced_checked, + reduced_merged, + reduced_min_dist, + treelike_checked, + treelike_max_dist, + depth2_false_merges, + false_merge_max_sep_depth, + false_merge_unresolved, + d1_classes: classes.len(), + } + } + pub fn prove() -> PillarResult { let t0 = Instant::now(); @@ -349,6 +597,15 @@ mod active { && pde.edge_dev > PDE_EDGE_MIN_DEV && pde.below_edge_dev < PDE_FLOOR; + // ── W6: Theorem 2 lattice leg ─────────────────────────────────── + let lat = lattice_leg(); + let lattice_pass = lat.reduced_merged == 0 + && lat.treelike_max_dist < LATTICE_EPS + && lat.depth2_false_merges >= 1 + && lat.false_merge_unresolved == 0 + && lat.false_merge_max_sep_depth <= hl_theorem2_depth(LATTICE_FALSE_MERGE_L) + && lat.d1_classes == 7; + let runtime_ms = t0.elapsed().as_millis() as u64; let discrimination_ratio = if max_forward_dist > 0.0 { @@ -360,7 +617,8 @@ mod active { let pass = forward_pairs_pass == N_PAIRS as u64 && converse_pairs_pass == N_PAIRS as u64 && discrimination_ratio >= DISCRIMINATION_RATIO_MIN - && pde_pass; + && pde_pass + && lattice_pass; let detail = format!( "N={} pairs, dim={}, depth={}. \ @@ -382,7 +640,16 @@ mod active { O(h²) discretization artifact rather than a uniqueness failure — \ so that leg certifies the converse FUNCTIONAL FORM (deviation is \ quadratic in enclosed Lévy area) and its own resolution boundary, \ - not a sampled ratio.", + not a sampled ratio. \ + THEOREM 2 LATTICE leg (W6, c = e·ln(1+√2) = {:.4}): {} reduced \ + words of length ≤ {} at depth ⌊c·L⌋, {} merged with the identity \ + (pass if 0), min ‖S − 1‖ = {:.3e}; {} tree-like words, max \ + ‖S − 1‖ = {:.1e} (pass if < {:.0e}); depth-2 false merges among \ + reduced words of length {} = {} (pass if ≥ 1 — depth 2 is NOT \ + the Index regime), all separated by depth {} ≤ ⌊c·{}⌋ = {}, {} \ + unresolved (pass if 0); d = 1 signature classes over the 64 \ + length-6 words = {} (pass if exactly 7: net increment only — \ + the d ≥ 2 precondition).", N_PAIRS, DIM, DEPTH, @@ -408,6 +675,21 @@ mod active { PDE_BELOW_EDGE_H / 2.0, pde.below_edge_dev, PDE_FLOOR, + hl_theorem2_constant(), + lat.reduced_checked, + LATTICE_L_MAX, + lat.reduced_merged, + lat.reduced_min_dist, + lat.treelike_checked, + lat.treelike_max_dist, + LATTICE_EPS, + LATTICE_FALSE_MERGE_L, + lat.depth2_false_merges, + lat.false_merge_max_sep_depth, + LATTICE_FALSE_MERGE_L, + hl_theorem2_depth(LATTICE_FALSE_MERGE_L), + lat.false_merge_unresolved, + lat.d1_classes, ); PillarResult { diff --git a/crates/lance-graph-contract/src/epistemic_bassin.rs b/crates/lance-graph-contract/src/epistemic_bassin.rs index 90c17ebc5..a2fd620d6 100644 --- a/crates/lance-graph-contract/src/epistemic_bassin.rs +++ b/crates/lance-graph-contract/src/epistemic_bassin.rs @@ -9,7 +9,16 @@ //! # Why the signed net was FALSIFIED, not merely limited //! //! In one signed register, `+3` support and `−3` refutation sum to `0` — -//! maximal balanced conflict indistinguishable from silence. If agreement +//! maximal balanced conflict indistinguishable from silence. The `3` is +//! only the illustrative pair: the old lane was true two's-complement i4 +//! over the full `[−8, 7]` (`atoms::I4x32::sext4`, no narrower quantizer +//! ever existed), and the collapse holds for EVERY magnitude `1..=7` +//! (`+x + (−x) = 0`, byte-identical to `SILENT`); only `x = 8` escapes, +//! and only because `+8` is unrepresentable and clamps to `+7`. Widening +//! the lane would not have fixed it — the loss is DIMENSIONAL (two +//! independent counts projected onto one signed coordinate), not RANGE +//! (source audit 2026-09-01, `literature-harvest-2026-09-01-post-1132.md` +//! companion). If agreement //! and disagreement are the interesting information, a representation that //! destroys their coincidence is wrong, not constrained; `basin_lanes`' //! own pinned collapse test is the evidence. The pair keeps both sides: @@ -67,12 +76,17 @@ //! A node's pair expresses its DIRECT children accumulated; whether the //! next hop continues or cancels what it reads is the second hop's //! decision. [`accumulate_children`](EpistemicBassin24::accumulate_children) -//! is exact-sum-then-clamp and therefore order-independent **within one -//! call** — but recursively composing already-clamped child registers is -//! NOT associative (a clamped 15 means "at least 15"). Saturation is -//! monotone and conflict-preserving — a saturated count can understate -//! mass, never convert conflict into silence — which is precisely what the -//! superseded signed net could not guarantee. +//! is exact-sum-then-clamp. Per side that is the MV-monoid `(L₁₆, ⊕, 0)` +//! with `a ⊕ b = min(15, a + b)` (Chang 1958): **associative and +//! commutative even across recursive hops** — any fold order of a hop tree +//! yields a bit-identical register (pinned exhaustively over all 16³ +//! triples, `accumulation_is_associative_and_non_cancellative_per_side`). +//! What the clamp costs is CANCELLATIVITY: `15 ⊕ 1 == 15 ⊕ 2`, so a +//! clamped 15 means "at least 15" and understates mass; it never converts +//! conflict into silence — which is precisely what the superseded signed +//! net could not guarantee. (An earlier wording here said "NOT +//! associative"; that was too weak in the safe direction — corrected +//! 2026-09-01 after the harvest probe.) /// Named axes in one basis register pair. pub const BASIS_AXES: usize = 24; @@ -83,6 +97,12 @@ pub const BASIS_REGISTER_BYTES: usize = 12; /// Wire width of the pair: agree register then disagree register. pub const BASIS_PAIR_BYTES: usize = 2 * BASIS_REGISTER_BYTES; +// The two-register cost is ENFORCED, not narrated: the pair is exactly two +// V3 facet payloads wide and cannot fit one (the superseded `BasinLanes` +// pinned `BASIN_LANE_BYTES == CASCADE_UNITS`; this is the successor's pin). +const _: () = assert!(core::mem::size_of::() == BASIS_PAIR_BYTES); +const _: () = assert!(BASIS_PAIR_BYTES == 2 * crate::facet::CASCADE_UNITS); + /// Per-axis count ceiling (u4). pub const AXIS_COUNT_MAX: u8 = 15; @@ -541,6 +561,66 @@ pub fn sigma_tension_u4(growth: f64, bound: f64) -> u8 { #[cfg(test)] mod tests { + /// The universal form of `basin_lanes`' `+3 / −3` collapse pin: at EVERY + /// representable magnitude the pair keeps balanced conflict distinct from + /// silence, with the old carrier's whole output (`net == 0`) reproduced + /// and the added coordinate (`contest == x`) carrying the difference. + /// Disable arm: derive `axis_state` from `net` instead of the pair and + /// every iteration goes red — exactly the sweep the transcribed old + /// encoder produced (`x = 1..=7` all `SILENT`). + #[test] + fn the_pair_distinguishes_balanced_conflict_from_silence_at_every_magnitude() { + for x in 1u8..=AXIS_COUNT_MAX { + let mut sup = [0u8; BASIS_AXES]; + sup[5] = x; + let mut refu = [0u8; BASIS_AXES]; + refu[5] = x; + let p = EpistemicBassin24::accumulate_children(&[ + EpistemicBassin24::pack(&sup, &[0; BASIS_AXES]), + EpistemicBassin24::pack(&[0; BASIS_AXES], &refu), + ]); + assert_ne!(p, EpistemicBassin24::SILENT, "x={x}"); + assert_eq!(p.axis_state(5), AxisState::Contested, "x={x}"); + assert_eq!(p.net(5), 0, "x={x}"); + assert_eq!(p.contest(5), x, "x={x}"); + } + } + + /// `accumulate_children` is an MV-monoid on L₁₆ per side: exact + /// sum-then-clamp is associative and commutative (Chang 1958), so any + /// hop-tree fold order gives a bit-identical register. What the clamp + /// costs is CANCELLATIVITY (`15 ⊕ 1 == 15 ⊕ 2`), i.e. understated mass — + /// never order-dependence and never conflict turned into silence. + #[test] + fn accumulation_is_associative_and_non_cancellative_per_side() { + let lane = |a: u8, d: u8| { + let mut s = [0u8; BASIS_AXES]; + s[0] = a; + let mut r = [0u8; BASIS_AXES]; + r[0] = d; + EpistemicBassin24::pack(&s, &r) + }; + let acc = EpistemicBassin24::accumulate_children; + let mut non_cancel = 0usize; + for a in 0..=AXIS_COUNT_MAX { + for b in 0..=AXIS_COUNT_MAX { + for c in 0..=AXIS_COUNT_MAX { + let l = acc(&[acc(&[lane(a, c), lane(b, a)]), lane(c, b)]); + let r = acc(&[lane(a, c), acc(&[lane(b, a), lane(c, b)])]); + assert_eq!(l, r, "assoc a={a} b={b} c={c}"); + if b != c && acc(&[lane(a, 0), lane(b, 0)]) == acc(&[lane(a, 0), lane(c, 0)]) { + non_cancel += 1; + } + } + } + } + assert!( + non_cancel > 0, + "saturation must cost cancellativity somewhere" + ); + assert_eq!(non_cancel, 1360, "the L16 non-cancellation census"); + } + use super::*; #[test] diff --git a/crates/sigker/src/codec.rs b/crates/sigker/src/codec.rs index ee0152c21..423637439 100644 --- a/crates/sigker/src/codec.rs +++ b/crates/sigker/src/codec.rs @@ -39,12 +39,21 @@ //! } //! ``` //! -//! # Certification dependency +//! # Certification dependency — LENGTH-PARAMETERIZED (jc Pillar 11, W6) //! -//! This classification is *asserted* until jc Pillar 11 (Hambly-Lyons -//! signature uniqueness on lance-graph paths) lands and verifies it -//! empirically on the actual SPO traversal lengths and carrier widths -//! used in production. See `crates/jc/src/hambly_lyons.rs` (stub). +//! Certified 2026-09-01 by jc Pillar 11's Theorem 2 lattice leg +//! (`crates/jc/src/hambly_lyons.rs`), NOT at a fixed depth: for unit-step +//! lattice walks X, Y in d ≥ 2, `S^(N)(X) = S^(N)(Y) ⟺ X ∼ Y` holds for +//! truncation depth `N ≥ ⌊e·log(1+√2)·(|X|+|Y|)⌋` (d = 2; times +//! `2⌈log₃(d/2)⌉+3` in general — Hambly-Lyons math/0507536v2 Thm 2/3). +//! So "lossless on the tree-quotient" is TRUE ONLY UNDER A WALK-LENGTH +//! BUDGET: a consumer routing paths through `Sigker` must pick its depth +//! from the longest walk it will compare, and escalate or refuse beyond +//! it. Depth 2 is a necessary condition only (64 distinct length-8 reduced +//! words share `S^(2) = 1` with the constant path). A one-dimensional +//! carrier (a single `u8:u8` rail read as one axis) is out of regime: +//! its reduced-path group is Z. Non-lattice piecewise-linear paths are +//! covered by Thm 9 (non-trivial signature) without an explicit depth. /// Sigker's view of the `CodecRoute` enum from lance-graph-contract. /// diff --git a/crates/sigker/src/lib.rs b/crates/sigker/src/lib.rs index 7c37eef6b..2fa26a4ed 100644 --- a/crates/sigker/src/lib.rs +++ b/crates/sigker/src/lib.rs @@ -27,7 +27,9 @@ //! 6. **Codec route integration** (`codec.rs`): exposes sigker as a third //! `CodecRoute` variant alongside Passthrough and CamPq. Sigker is //! **Index regime** — by Hambly-Lyons uniqueness, it is lossless on -//! tree-quotient classes of paths. +//! tree-quotient classes of paths — at a truncation depth that grows +//! LINEARLY with walk length (Thm 2/3; see `codec.rs`), never at a +//! fixed small depth. //! //! ## Why sigker is Index regime, not Argmax //! From f679823f4c2fb9208facd428241df79de0f5aae3 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 20:42:04 +0000 Subject: [PATCH 3/5] harvest: credit jc Pillar 6's own honest framing of the K-S-style CV heuristic; the promotion to a bound was #322/#1129 Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QHVUi6Q9XtmKgxh6pDRayP --- .claude/knowledge/literature-harvest-2026-09-01-post-1132.md | 1 + 1 file changed, 1 insertion(+) diff --git a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md index 5ac2e79a8..9ad4fce48 100644 --- a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md +++ b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md @@ -84,6 +84,7 @@ - **SPECIFIC RESULT** Thm 1 bounds `E[d²(S_n, μ)]` for the **inductive mean** `S_{n+1} = S_n ⊕_{1/(n+1)} X_{n+1}` of **independent** `L²`-valued samples. Its RHS is `O(1/n)`. `pillar_5plus_bound(n) = √(2/n)·√(1+0.08n)` is dimensionless, has no `μ`, `μ_k`, `D_n` or `Var`, and tends to `2σ_step = 0.4` (probed: 1.470, 0.812, 0.534, 0.424, 0.400 at n = 1, 4, 16, 100, 10⁴). jc's own `ewa_sandwich.rs:317` calls it "Köstenberger-Stark-*style*" and derives it from a log-normal/χ² heuristic over a population of random paths. - **CURRENT MAP** `sigma_propagation::pillar_5plus_bound` doc ("per Pillar 5+ proof-in-code"); `sigma_tension_u4(growth, bound)` (#1129); v3 axis TENSION's grounding line in `E-THE-24-AXIS-BASIS-V3…-1`. **Pillar 5+ itself (`jc/koestenberger.rs`) is NOT affected** — it builds a real inductive mean and is a correct use of Thm 1. - **DESTINATION** CERTIFICATE_ONLY (falsification of a citation + a units defect; no new concept). +- **CREDIT WHERE DUE (added after operator review, 2026-09-01):** jc's own Pillar 6 header is honest about this — it states the goal as *"rate consistent with Köstenberger-Stark Theorem 1, even though the aggregation operator is sandwich (not inductive mean)"* and its PASS criterion as *"variance concentration consistent with KS Theorem 1 FORM … with n_eff accounting for path-length-dependent volatility"*. That is a documented consistency heuristic, not a claimed theorem. The promotion from heuristic to "bound" happened downstream: PR #322 exported the CV curve into the contract as `pillar_5plus_bound` with the doc-comment "per Pillar 5+ proof-in-code", and #1129's `sigma_tension_u4` consumed it as a per-path bound. The correction therefore targets the contract's doc-comment and the readout's units, not jc. - **ΔH** Removes "the sandwich walk is concentration-certified by K-S" and the free parameter `σ_step = 0.2`. - **MECHANISM CHECK** `Σ' = MΣMᵀ` is a congruence, an isometry of `d_AI` for invertible M, not a geodesic convex combination; there is no `S_n` in the code (`grep barycenter|frechet|inductive_mean sigma_propagation.rs` → 0 hits). Units: `growth` is `d_AI(Σ_n, I)² − d_AI(Σ_0, I)²`; `bound` is a CV. The 10000/10000 PASS is a property of the i.i.d. rotated-step generator in `ewa_sandwich::prove`, not of the bound. - **CERTIFICATE** Replace with R2. Until then, label `pillar_5plus_bound` "empirical CV reference curve for the jc i.i.d. generator, not a bound". From cb977d8ac40d99ed24f407aca908197f3a23138f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 20:55:50 +0000 Subject: [PATCH 4/5] jc: focused unit tests for the W6 lattice helpers; harvest: escape table pipes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review round (CodeRabbit on #1133): direct tests for hl_theorem2_depth (the paper's floor for L = 1..16), is_reduced, and the figure-of-eight as a depth-2 false merge separated at depth 3; doc comments on the helpers. Markdown table rows with |x| inside code spans escaped. The "2e coefficient / ceiling / Theorems 5–6" finding was checked against the primary source and NOT applied: math/0507536v2 p.11 states Theorem 2 with ⌊e·log(1+√2)·L⌋ and p.14 states Theorem 3; the citation here is to that arXiv version explicitly. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QHVUi6Q9XtmKgxh6pDRayP --- ...literature-harvest-2026-09-01-post-1132.md | 6 +-- crates/jc/src/hambly_lyons.rs | 51 ++++++++++++++++--- 2 files changed, 48 insertions(+), 9 deletions(-) diff --git a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md index 9ad4fce48..76ba03e4f 100644 --- a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md +++ b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md @@ -17,7 +17,7 @@ |---|---| | `EpistemicBassin24` | 24 × `(agree_u4, disagree_u4)`; `net`, `contest = min(a,d)`, `axis_state ∈ {Silent, Agree, Disagree, Contested}`, `entropy_bits` = Shannon over the 4-state census, `stance_entropy_bits(children, axis)`, `accumulate_children` = exact u32 sum per side then clamp 15, `support/refute/contested/silent_mask` u64 | | `info_gain_u4(before, after)` | `floor(log2(before/after))` clamped 0..15; `after == 0 && before > 0` → 15 | -| `sigma_tension_u4(growth, bound)` | `ceil(4·|growth|/bound)` clamped 15; `growth` = `‖log Σ_n‖²_F − ‖log Σ_0‖²_F` (a squared affine-invariant distance), `bound` = `pillar_5plus_bound(n)` | +| `sigma_tension_u4(growth, bound)` | `ceil(4·\|growth\|/bound)` clamped 15; `growth` = `‖log Σ_n‖²_F − ‖log Σ_0‖²_F` (a squared affine-invariant distance), `bound` = `pillar_5plus_bound(n)` | | `pillar_5plus_bound(n)` | `√(2/n)·√(1+2·0.04·n)` — a **coefficient of variation** curve, `σ_step = 0.2` hard-coded; → 0.4 as n→∞ | | `jc::koestenberger::prove` | a genuine Sturm inductive mean `S_{n+1} = S_n ⊕_{1/(n+1)} X_{n+1}` on 2×2 SPD, `E[d²(S_n, I)]` vs K-S Thm 1 RHS — **correct use of K-S** | | `jc::ewa_sandwich::prove` | 10000 random paths of `MΣMᵀ` with i.i.d. rotated log-normal steps; PSD rate ≥ 0.999 and *population* CV of `‖log Σ_n‖²_F` ≤ 1.75 × the curve above; the comment itself says "Köstenberger-Stark-**style**" | @@ -32,10 +32,10 @@ | # | area | result | destination | ΔH | status | |---|---|---|---|---|---| -| D1 | D | Hambly-Lyons **Theorem 2/3** (math/0507536v2 §2.4): a lattice path of length L whose first ⌊e·log(1+√2)·L⌋ = ⌊2.3959·L⌋ iterated integrals vanish is tree-like (d=2); general d: ⌊(2⌈log₃(d/2)⌉+3)·2.3959·L⌋. Truncated signature is a homomorphism into G^N, so `S^(N)(X)=S^(N)(Y) ⟺ X∼Y` at `N ≥ ⌈c(d)·(|X|+|Y|)⌉` for unit-step lattice walks | **CERTIFICATE_ONLY — Pillar 11 FLIPPED GREEN for lattice walks**, length-parameterized | highest | ✔ constant re-read from math/0507536v2 p.11/p.14 on the main thread; W6 leg shipped in `jc/hambly_lyons.rs` (484/484 reduced words separated, 64 tree-like at 2e-15, 64 depth-2 false merges all separated by depth 3, d=1 → 7 classes; disable arm fails) | +| D1 | D | Hambly-Lyons **Theorem 2/3** (math/0507536v2 §2.4): a lattice path of length L whose first ⌊e·log(1+√2)·L⌋ = ⌊2.3959·L⌋ iterated integrals vanish is tree-like (d=2); general d: ⌊(2⌈log₃(d/2)⌉+3)·2.3959·L⌋. Truncated signature is a homomorphism into G^N, so `S^(N)(X)=S^(N)(Y) ⟺ X∼Y` at `N ≥ ⌈c(d)·(\|X\|+\|Y\|)⌉` for unit-step lattice walks | **CERTIFICATE_ONLY — Pillar 11 FLIPPED GREEN for lattice walks**, length-parameterized | highest | ✔ constant re-read from math/0507536v2 p.11/p.14 on the main thread; W6 leg shipped in `jc/hambly_lyons.rs` (484/484 reduced words separated, 64 tree-like at 2e-15, 64 depth-2 false merges all separated by depth 3, d=1 → 7 classes; disable arm fails) | | D2 | D | The depth-2 forward leg tests membership in `ker(G^∞→G²)`, not tree-likeness: the §1.6 figure-eight has S¹=S²=0 like the out-and-back but S³≠0 | **REJECT** depth-2 as Index regime (necessary condition only) | high | ✔ PROBED (S¹¹²: fig-8 = 1.0, out-and-back = 0.0) | | 1 | E | `pillar_5plus_bound` cites a theorem about the inductive mean of independent samples (K-S Thm 1) to certify a congruence orbit; `sigma_tension_u4` divides a squared distance by a dimensionless CV | **CERTIFICATE_ONLY (falsifies)** | high | ✔ PROBED (code read; aligned-M arm) | -| 2 | E | Replacement: deterministic isometry bound `|‖log Σ_n‖_F − ‖log Σ_0‖_F| ≤ 2·Σ‖log M_k‖_F` for any invertible symmetric M | **MACRO_CANDIDATE** (composition of `logm` + Frobenius) | high | ✔ PROBED (max ratio 0.567 on 2000 random 20-hop paths) | +| 2 | E | Replacement: deterministic isometry bound `\|‖log Σ_n‖_F − ‖log Σ_0‖_F\| ≤ 2·Σ‖log M_k‖_F` for any invertible symmetric M | **MACRO_CANDIDATE** (composition of `logm` + Frobenius) | high | ✔ PROBED (max ratio 0.567 on 2000 random 20-hop paths) | | 3 | C | Greedy posterior-based admission (INFO_GAIN, VoI) is Ω(n/log n)-suboptimal (Golovin-Krause-Ray Thm 9); EC² edge-cut objective is adaptive-submodular with a `(2 ln(1/p_min)+1)` bound | CERTIFICATE_ONLY + **MACRO_CANDIDATE** `admit_ec2` | high | literature [G] | | 4 | B | ACCUMULATE (sum-then-clamp on L₁₆) is an MV-monoid: associative, commutative, non-cancellative, top-absorbing — the module's "not claimed associative" is too weak | CERTIFICATE_ONLY (strengthen) | high | ✔ PROBED (0/4096 violations, 1360 non-cancel pairs) | | 5 | A | Independent per-side clamp is not ratio-preserving: (30,2)→(15,2) moves f 0.938→0.882; heavy agreement drifts toward a=d=15 = false Contested | CERTIFICATE_ONLY (saturation flag) | high | arithmetic [G] | diff --git a/crates/jc/src/hambly_lyons.rs b/crates/jc/src/hambly_lyons.rs index 8d0dd2125..db7b2cd82 100644 --- a/crates/jc/src/hambly_lyons.rs +++ b/crates/jc/src/hambly_lyons.rs @@ -369,11 +369,11 @@ mod active { // * d ≥ 2 — in d = 1 the reduced-path group is Z (net increment only, // every closed path is tree-like), so the quotient carries nothing. /// `e · ln(1 + √2)` — Theorem 2's constant, computed rather than retyped. - fn hl_theorem2_constant() -> f64 { + pub(super) fn hl_theorem2_constant() -> f64 { std::f64::consts::E * (1.0 + 2f64.sqrt()).ln() } /// The depth Theorem 2 needs for a word of length `l` (floor, as stated). - fn hl_theorem2_depth(l: usize) -> usize { + pub(super) fn hl_theorem2_depth(l: usize) -> usize { (hl_theorem2_constant() * l as f64).floor() as usize } /// Longest word the exhaustive theorem arm enumerates. Depth ⌊c·5⌋ = 11 @@ -386,9 +386,9 @@ mod active { /// Exactness tolerance: signatures of lattice words are rationals with /// k! denominators; f64 products of a handful of exponentials round at /// ~1e-15, and a genuinely nonzero coefficient is ≥ 1/k! ≥ 1/19!. - const LATTICE_EPS: f64 = 1e-12; + pub(super) const LATTICE_EPS: f64 = 1e-12; - /// Letters a, b, a⁻¹, b⁻¹ as 0..4; inverse is `(l + 2) % 4`. + /// Letters a, b, a⁻¹, b⁻¹ as 0..4; inverse is `(l + 2) % 4`. Unit step of a letter. fn letter_step(l: u8) -> [f64; 2] { match l { 0 => [1.0, 0.0], @@ -397,6 +397,7 @@ mod active { _ => [0.0, -1.0], } } + /// The lattice path of a word: unit steps from the origin, one per letter. fn lattice_path(word: &[u8]) -> Vec> { let mut p = vec![vec![0.0, 0.0]]; for &l in word { @@ -406,10 +407,12 @@ mod active { } p } - fn is_reduced(word: &[u8]) -> bool { + /// Freely reduced: no adjacent `x x⁻¹`. + pub(super) fn is_reduced(word: &[u8]) -> bool { word.windows(2).all(|w| (w[0] + 2) % 4 != w[1]) } - fn distance_from_identity(word: &[u8], depth: usize) -> f64 { + /// `‖S^(depth)(word) − 1‖_F` via `sigker::signature_truncated`. + pub(super) fn distance_from_identity(word: &[u8], depth: usize) -> f64 { let s = signature_truncated(&lattice_path(word), depth); signature_distance(&s, &Signature::identity(2, depth)) } @@ -727,6 +730,42 @@ pub fn prove() -> PillarResult { mod tests { use super::*; + // ── W6 lattice helpers, tested directly (not only through prove()) ────── + + #[test] + fn theorem2_depth_is_the_paper_floor() { + // ⌊e·ln(1+√2)·L⌋, math/0507536v2 Theorem 2, L = 1..16 + let expect = [ + 2usize, 4, 7, 9, 11, 14, 16, 19, 21, 23, 26, 28, 31, 33, 35, 38, + ]; + for (i, &e) in expect.iter().enumerate() { + assert_eq!(active::hl_theorem2_depth(i + 1), e, "L={}", i + 1); + } + assert!((active::hl_theorem2_constant() - 2.3958).abs() < 1e-3); + } + + #[test] + fn is_reduced_rejects_exactly_adjacent_inverse_pairs() { + assert!(active::is_reduced(&[0, 1, 2, 3])); + assert!(!active::is_reduced(&[0, 2])); + assert!(!active::is_reduced(&[1, 0, 2, 3])); + assert!(active::is_reduced(&[0, 0, 0])); + assert!(active::is_reduced(&[])); + } + + #[test] + fn the_figure_of_eight_is_a_depth_2_false_merge_separated_at_depth_3() { + // a b a⁻¹ b⁻¹ · b⁻¹ a⁻¹ b a — the paper's §1.6 counterexample + let w = [0u8, 1, 2, 3, 3, 2, 1, 0]; + assert!(active::is_reduced(&w)); + assert!(active::distance_from_identity(&w, 2) < active::LATTICE_EPS); + assert!(active::distance_from_identity(&w, 3) > 0.1); + // and the genuine out-and-back is the identity at every depth + for depth in 1..=6 { + assert!(active::distance_from_identity(&[0, 2], depth) < active::LATTICE_EPS); + } + } + #[test] fn pillar_passes() { let r = prove(); From 1a3c7294ac5c6991b44639ca8b7652f00168723b Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 21:30:16 +0000 Subject: [PATCH 5/5] =?UTF-8?q?jc:=20Pillar=2011=20constant=20corrected=20?= =?UTF-8?q?to=20the=20published=202e=C2=B7ln(1+=E2=88=9A2)=20(Annals=20Thm?= =?UTF-8?q?=205/6)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CodeRabbit's finding on #1133 was right and my arXiv-only rebuttal was wrong: arXiv math/0507536v2 states the lattice results as Theorems 2/3 with coefficient e, but its proof indexes the odd-degree sum by pairs, and the published Annals 171 (2010) text — verified against the journal PDF — states Theorems 5/6 with 2e·log(1+√2) and takes x = 2·log(1+√2)·L in the proof. hl_theorem2_constant is now 2e·ln(1+√2) = 4.7916 (floor rounding unchanged, as stated). The exhaustive arm shortens to words of length ≤ 3 (52 reduced words, depth 14) because the doubled depth makes length 5 (depth 23) too large; the tree-like arm uses a fixed depth 12 (identity holds at every depth, Cor. 6.4); the false-merge search still escalates and stops at level 3. sigker docs, harvest ledger, LATEST_STATE and a dated ⊘ correction inside the EPIPHANIES entry updated; the version trap is recorded in the pillar header so it is not re-walked. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QHVUi6Q9XtmKgxh6pDRayP --- .claude/board/EPIPHANIES.md | 11 +++ .claude/board/LATEST_STATE.md | 2 +- ...literature-harvest-2026-09-01-post-1132.md | 10 +-- crates/jc/src/hambly_lyons.rs | 76 ++++++++++++------- crates/sigker/src/codec.rs | 7 +- crates/sigker/src/lib.rs | 2 +- 6 files changed, 69 insertions(+), 39 deletions(-) diff --git a/.claude/board/EPIPHANIES.md b/.claude/board/EPIPHANIES.md index 222330752..e4d81e10c 100644 --- a/.claude/board/EPIPHANIES.md +++ b/.claude/board/EPIPHANIES.md @@ -24,6 +24,17 @@ axis is out of regime, and arbitrary quantized step vectors stay outside Theorem 2 (Theorem 9 gives non-triviality without an explicit depth). Default jc build stays zero-dep/DEFERRED. +> **⊘ Correction (same day, review round on #1133):** the constant is +> **`2e·ln(1+√2) = 4.7916`**, and the theorems are **5/6** in the published +> Annals 171 text. The arXiv v2 statement (Theorems 2/3, coefficient `e`) +> that this entry first cited is pre-publication: its proof sums over odd +> degrees `2k−1` with `k > N`, so "first N terms" there is degree ~2N; the +> journal version takes `x = 2·log(1+√2)·L` and states `2e`. Caught by a +> review bot against the arXiv-only reading, verified on the Annals PDF. +> Measured after the fix: 52/52 reduced words of length ≤ 3 separated at +> the doubled depth; every other count above is unchanged (the false-merge +> search escalates depth and still stops at level 3). + **Companion source audit (pre-#1129 signed register), same session:** the old `BasinLanes` lane was true two's-complement i4 over the FULL `[−8, 7]` (`atoms::I4x32::sext4`; 16 states, no quantizer); "−3..+3" is prose only — diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index c1493ebd9..8ca5080ec 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,5 +1,5 @@ ## 2026-09-01 — branch (PR pending): D-DCR-2b EpistemicBassin24 — CONTRACT INVENTORY DELTA -- `jc::hambly_lyons` **Pillar 11 GREEN for lattice walks — length-parameterized (W6, 2026-09-01)**: Theorem 2 lattice leg added (Hambly-Lyons math/0507536v2 §2.4, `c = e·ln(1+√2) = 2.3958`, re-read from the primary source): all 484 reduced words of length ≤ 5 separated at depth ⌊c·L⌋, 64 tree-like words at the identity (2e-15), 64 depth-2 false merges among length-8 reduced words all separated by depth 3 ≤ ⌊c·8⌋ = 19, d = 1 collapses to exactly 7 signature classes (the `d ≥ 2` precondition). `sigker` Index regime re-worded: lossless on the tree-quotient ONLY under a walk-length budget `N ≥ ⌊c(d)·(|X|+|Y|)⌋`; depth 2 is necessary-only. Default build stays zero-dep/DEFERRED. Still red for non-lattice quantized step vectors (Thm 9 gives non-triviality without an explicit depth). +- `jc::hambly_lyons` **Pillar 11 GREEN for lattice walks — length-parameterized (W6, 2026-09-01)**: Theorem 5 lattice leg added (Hambly-Lyons Annals 171 §2.4 — Thm 5/6, `c = 2e·ln(1+√2) = 4.7916`, verified on the published PDF; the arXiv v2 `e` is pre-publication): all 52 reduced words of length ≤ 3 separated at depth ⌊c·L⌋, 64 tree-like words at the identity (2e-15), 64 depth-2 false merges among length-8 reduced words all separated by depth 3 ≤ ⌊c·8⌋ = 38, d = 1 collapses to exactly 7 signature classes (the `d ≥ 2` precondition). `sigker` Index regime re-worded: lossless on the tree-quotient ONLY under a walk-length budget `N ≥ ⌊c(d)·(|X|+|Y|)⌋`; depth 2 is necessary-only. Default build stays zero-dep/DEFERRED. Still red for non-lattice quantized step vectors (Thm 9 gives non-triviality without an explicit depth). - `lance_graph_contract::epistemic_bassin::{EpistemicBassin24, AxisState, BASIS_AXES(24), BASIS_PAIR_BYTES(24), AXIS_COUNT_MAX(15), info_gain_u4, sigma_tension_u4}` — the field map's value carrier as an `agree_u4[24] + disagree_u4[24]` PAIR (operator co-architect ruling: the signed net was FALSIFIED — `+3 + −3 = 0` collapsed balanced conflict into silence). Net/polarity/contest/entropy DERIVED; `Contested` is a first-class state that survives one-hop accumulation. Readout adapters grounded in shipped certificates: `info_gain_u4` (Shannon ΔH over candidate counts), `sigma_tension_u4` (quarters of `sigma_propagation::pillar_5plus_bound`; 7 = the 1.75× PASS slack); Hambly-Lyons has NO lane (sigker classification gated on jc Pillar 11, DEFERRED). **No storage minted**: the loci-never-magnitude law is scoped to the A9 READING, not tenant 14's bytes — the bassin is a classid-selected reading of the same physical lane; a separate tenant waits for one real row needing both readings simultaneously (an `EpistemicWitness = 16` mint was built and discarded uncommitted on this ruling). - `epistemic_bassin` Belnap layer — `AXIS_MASK_ALL` + `{support_mask, refute_mask, contested_mask, silent_mask}` (u64, bits 0..24): the two-bit-per-axis Belnap/FDE encoding of the four axis states (K3 as its contested-free restriction); knowledge-join = bitwise OR = provably `accumulate_children`'s state layer (pinned). Composes with `revision::EvidenceMask for u64` for bit-parallel kind-3 question masking; asked-but-silent = the missing-link query in one op. diff --git a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md index 76ba03e4f..26314a5f6 100644 --- a/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md +++ b/.claude/knowledge/literature-harvest-2026-09-01-post-1132.md @@ -32,7 +32,7 @@ | # | area | result | destination | ΔH | status | |---|---|---|---|---|---| -| D1 | D | Hambly-Lyons **Theorem 2/3** (math/0507536v2 §2.4): a lattice path of length L whose first ⌊e·log(1+√2)·L⌋ = ⌊2.3959·L⌋ iterated integrals vanish is tree-like (d=2); general d: ⌊(2⌈log₃(d/2)⌉+3)·2.3959·L⌋. Truncated signature is a homomorphism into G^N, so `S^(N)(X)=S^(N)(Y) ⟺ X∼Y` at `N ≥ ⌈c(d)·(\|X\|+\|Y\|)⌉` for unit-step lattice walks | **CERTIFICATE_ONLY — Pillar 11 FLIPPED GREEN for lattice walks**, length-parameterized | highest | ✔ constant re-read from math/0507536v2 p.11/p.14 on the main thread; W6 leg shipped in `jc/hambly_lyons.rs` (484/484 reduced words separated, 64 tree-like at 2e-15, 64 depth-2 false merges all separated by depth 3, d=1 → 7 classes; disable arm fails) | +| D1 | D | Hambly-Lyons **Theorem 5/6** (Annals 171, 2010, §2.4; = arXiv v2 Thm 2/3, whose `e` was corrected to `2e` in publication — caught by CodeRabbit on #1133 and verified against the Annals PDF): a lattice path of length L whose first ⌊2e·log(1+√2)·L⌋ = ⌊4.7916·L⌋ iterated integrals vanish is tree-like (d=2); general d: ⌊(2⌈log₃(d/2)⌉+3)·4.7916·L⌋. Truncated signature is a homomorphism into G^N, so `S^(N)(X)=S^(N)(Y) ⟺ X∼Y` at `N ≥ ⌈c(d)·(\|X\|+\|Y\|)⌉` for unit-step lattice walks | **CERTIFICATE_ONLY — Pillar 11 FLIPPED GREEN for lattice walks**, length-parameterized | highest | ✔ constant re-read from math/0507536v2 p.11/p.14 on the main thread; W6 leg shipped in `jc/hambly_lyons.rs` (52/52 reduced words of length ≤ 3 separated at the doubled depth, 64 tree-like at 2e-15, 64 depth-2 false merges all separated by depth 3, d=1 → 7 classes; disable arm fails) | | D2 | D | The depth-2 forward leg tests membership in `ker(G^∞→G²)`, not tree-likeness: the §1.6 figure-eight has S¹=S²=0 like the out-and-back but S³≠0 | **REJECT** depth-2 as Index regime (necessary condition only) | high | ✔ PROBED (S¹¹²: fig-8 = 1.0, out-and-back = 0.0) | | 1 | E | `pillar_5plus_bound` cites a theorem about the inductive mean of independent samples (K-S Thm 1) to certify a congruence orbit; `sigma_tension_u4` divides a squared distance by a dimensionless CV | **CERTIFICATE_ONLY (falsifies)** | high | ✔ PROBED (code read; aligned-M arm) | | 2 | E | Replacement: deterministic isometry bound `\|‖log Σ_n‖_F − ‖log Σ_0‖_F\| ≤ 2·Σ‖log M_k‖_F` for any invertible symmetric M | **MACRO_CANDIDATE** (composition of `logm` + Frobenius) | high | ✔ PROBED (max ratio 0.567 on 2000 random 20-hop paths) | @@ -155,9 +155,9 @@ - **FALSIFIER** Scalar model `A=B=C=Q=1, Σ₀=1, R(x)=1+x²`: `u=0` → gain 0.549 nats, ambiguity 1.419; `u=2` → gain 0.168, ambiguity 2.224; then the Remark-4 level-set arm. - **MINT CONSEQUENCE** None. (Companion collapses: NOVELTY = `½(1/a − 1/a₀)` over Dirichlet counts = a script over REVISION/ACCUMULATE registers, census #13; pragmatic value = consumer prior `C`, census #14.) -### R9 · Hambly-Lyons Theorems 2/3 green Pillar 11 for lattice walks and kill the fixed-depth Index regime — CERTIFICATE_ONLY -- **CLAIM** [G] (theorem as read by the auditor in math/0507536v2 §2.4; the constant must be re-read on the main thread before the pillar flips). For a length-`L` path on the 2-d integer lattice, vanishing of the first `⌊e·log(1+√2)·L⌋ = ⌊2.3959·L⌋` iterated integrals implies tree-likeness (Thm 2); in `R^d`, `⌊(2⌈log₃(d/2)⌉+3)·2.3959·L⌋` (Thm 3). The GL(2,C)-projected integrals carry less than the full tensor algebra, so the full truncated signature satisfies it a fortiori. -- **SPECIFIC RESULT** `S^{(N)}` is a homomorphism into the free nilpotent group `G^N`, so `S^{(N)}(X) = S^{(N)}(Y) ⟺ S^{(N)}(X ⋆ Y^{-1}) = 1`; apply Thm 2/3 to the concatenation: **`N ≥ ⌈c(d)·(|X|+|Y|)⌉`** is a complete two-sided certificate for unit-step lattice walks. +### R9 · Hambly-Lyons Theorems 5/6 green Pillar 11 for lattice walks and kill the fixed-depth Index regime — CERTIFICATE_ONLY +- **CLAIM** [G] (**constant corrected 2026-09-01 after review**: the arXiv v2 text states Theorems 2/3 with `e·log(1+√2)`; the published Annals 171 text states Theorems 5/6 with `2e·log(1+√2)`, its proof taking `x = 2·log(1+√2)·L` — the arXiv proof's index `k` counts pairs of degrees, so the journal form is the corrected one). For a length-`L` path on the 2-d integer lattice, vanishing of the first `⌊2e·log(1+√2)·L⌋ = ⌊4.7916·L⌋` iterated integrals implies tree-likeness (Thm 5); in `R^d`, `⌊(2⌈log₃(d/2)⌉+3)·4.7916·L⌋` (Thm 6). The GL(2,C)-projected integrals carry less than the full tensor algebra, so the full truncated signature satisfies it a fortiori. +- **SPECIFIC RESULT** `S^{(N)}` is a homomorphism into the free nilpotent group `G^N`, so `S^{(N)}(X) = S^{(N)}(Y) ⟺ S^{(N)}(X ⋆ Y^{-1}) = 1`; apply Thm 2/3 to the concatenation: **`N ≥ ⌊c(d)·(|X|+|Y|)⌋`, `c(2) = 2e·ln(1+√2)`** is a complete two-sided certificate for unit-step lattice walks. - **CURRENT MAP** `jc::hambly_lyons` (cites Thm 1/Cor 1.5 only — correct, depth-∞, insufficient); `sigker` `CodecRoute::Sigker` Index regime; the `E-V3-FACET-4-PLUS-12` rails as carrier. - **DESTINATION** CERTIFICATE_ONLY. The auditor proposed CORE_PRIMITIVE_CANDIDATE; **overruled on the main thread**: this greens a *held* primitive (the operator's stated highest-value outcome), it mints nothing new, and the Index regime it certifies is length-parameterized, so `sigker` must carry a walk-length budget and escalate beyond it. Preconditions before flipping: (a) `d ≥ 2` — a `u8:u8` rail read as one scalar axis is d=1 and collapses to the endpoint (census D3); the canon "u8:u8 is two bytes, never widened" is load-bearing here; (b) steps must be unit basis-aligned lattice steps — Thm 2's hypothesis is literally `‖x_k − x_{k+1}‖ = 1` on `Z^{|A|}`; arbitrary quantized vectors are outside it. - **ΔH** Eliminates "no finite-depth Hambly-Lyons exists" and "depth 2 suffices" simultaneously. The depth-2 forward leg (census D2, ✔ PROBED) is a necessary condition only; the 1e6 discrimination ratio is a scale artifact until Λ-normalized (D6). @@ -183,7 +183,7 @@ | `flat_frontier_assert` | Koudahl degenerate regime detector | `stddev(info_gain_u4)` over admitted frontier `> 0` | 32 candidates each 4096→2048 | ## 5. CERTIFICATES TO HARVEST (green or falsify an existing pillar/claim) -1. **Pillar 11 green path** — Hambly-Lyons Thm 2/3 (math/0507536v2 §2.4) + homomorphism into `G^N`; re-read the constant `e·log(1+√2)`; assert `d ≥ 2` and unit-lattice steps in `sigker`; retire fixed depth 2 (necessary-condition only). Companion: Salvi et al. Thm 15 (O(h²)) certifies the 2e-7 floor but Thm 8 needs C¹ — write the segment-wise Chen lemma; add a minimum-loop-scale precondition (figure-eight `dev ∝ ε⁶` sinks under the floor). +1. **Pillar 11 green path** — Hambly-Lyons Annals Thm 5/6 (§2.4) + homomorphism into `G^N`; constant `2e·log(1+√2)` (the arXiv v2 `e` is pre-publication); assert `d ≥ 2` and unit-lattice steps in `sigker`; retire fixed depth 2 (necessary-condition only). Companion: Salvi et al. Thm 15 (O(h²)) certifies the 2e-7 floor but Thm 8 needs C¹ — write the segment-wise Chen lemma; add a minimum-loop-scale precondition (figure-eight `dev ∝ ε⁶` sinks under the floor). 2. **Pillar 5+ scope** — keep `jc/koestenberger.rs` green for inductive means; strike "per Pillar 5+ / K-S" from `sigma_propagation::pillar_5plus_bound`; relabel it as the jc generator's empirical CV curve; fix `sigma_tension_u4` units via R2. If a stochastic pillar is wanted later: Cuny-Dedecker-Merlevède-Peligrad arXiv:2110.10937v2 Thm 2.1/3.1 (i.i.d. M only; the dependent case is OPEN and is the live one). 3. **ACCUMULATE contract** — associative/commutative/non-cancellative/top-absorbing (R4, probed); saturation flag on Contested reads (R5); `δ⁺ > δ⁻` post-clamp for Assumption-of-Failure (census #19). 4. **Frontier admission** — Golovin-Krause-Ray Thm 9 lower bound; EC² adaptive-submodularity as the repair (R3); Koudahl flat-EIG detector (#31). diff --git a/crates/jc/src/hambly_lyons.rs b/crates/jc/src/hambly_lyons.rs index db7b2cd82..fc25a12fa 100644 --- a/crates/jc/src/hambly_lyons.rs +++ b/crates/jc/src/hambly_lyons.rs @@ -26,17 +26,27 @@ //! //! # Status — GREEN for lattice walks, length-parameterized (2026-09-01, W6) //! -//! The pillar was red because Theorem 1 is a depth-∞ statement and the -//! substrate truncates. The finite-depth certificate is in the SAME paper, -//! two sections later (math/0507536v2 §2.4, constant re-read on the main -//! thread against the primary source): -//! -//! **Theorem 2.** A path of length L on the 2-d integer lattice whose -//! first ⌊e·log(1+√2)·L⌋ GL(2,C)-iterated integrals vanish is tree-like -//! and its reduced word is trivial. (e·ln(1+√2) = 2.3958…) -//! -//! **Theorem 3.** In the d-dimensional lattice the depth is -//! ⌊(2⌈log₃(d/2)⌉ + 3)·e·log(1+√2)·L⌋. +//! The pillar was red because the uniqueness theorem is a depth-∞ statement +//! and the substrate truncates. The finite-depth certificate is in the SAME +//! paper, §2.4 — cited from the PUBLISHED text, Annals of Mathematics 171(1) +//! 2010, pp. 109–167 (the constant below was verified against that PDF): +//! +//! **Theorem 5** (Annals numbering; Theorem 1 in the introduction restates +//! it). A path of length L on the 2-d integer lattice whose first +//! ⌊2e·log(1+√2)·L⌋ GL(2,C)-iterated integrals vanish is tree-like and +//! its reduced word is trivial. (2e·ln(1+√2) = 4.7916…) +//! +//! **Theorem 6.** In the d-dimensional lattice the depth is +//! ⌊(2⌈log₃(d/2)⌉ + 3)·2e·log(1+√2)·L⌋. +//! +//! ⚠ Version trap, recorded so it is not re-walked: arXiv math/0507536v2 +//! (Dec 2006) states the same results as Theorems 2/3 with coefficient `e`, +//! and its proof applies Lemma 2.4(2) with `x = log(1+√2)·L` while the sum +//! it bounds runs over ODD degrees `2k−1` — the index `k` counts pairs of +//! degrees, so "first N terms" there means degree up to ~2N. The published +//! version takes `x = 2·log(1+√2)·L` and states `2e`; that is the corrected +//! form and the one this pillar implements. A review bot caught the +//! discrepancy against the arXiv-only reading (lance-graph #1133). //! //! The GL(2,C) integrals are a projection of the tensor-algebra ones //! (fn. 2: "a priori contain less information"), so vanishing of the FULL @@ -44,7 +54,7 @@ //! Because the truncated signature is a homomorphism into the free //! nilpotent group, the pair form is //! -//! S^(N)(X) = S^(N)(Y) ⟺ X ∼ Y for N ≥ ⌊c(d)·(|X|+|Y|)⌋, +//! S^(N)(X) = S^(N)(Y) ⟺ X ∼ Y for N ≥ ⌊c(d)·(|X|+|Y|)⌋, c(2) = 2e·ln(1+√2), //! //! i.e. the Index regime is LENGTH-PARAMETERIZED: a consumer must carry a //! walk-length budget and escalate depth (or refuse) beyond it. Depth 2 is @@ -350,11 +360,12 @@ mod active { } } - // ── W6: the Theorem 2 lattice leg (the finite-depth certificate) ──────── + // ── W6: the Theorem 5 lattice leg (the finite-depth certificate) ──────── // - // Hambly-Lyons math/0507536v2 §2.4, Theorem 2 (re-read on the main - // thread 2026-09-01): a lattice path of length L on Z² whose first - // ⌊e·log(1+√2)·L⌋ GL(2,C)-iterated integrals vanish is tree-like and its + // Hambly-Lyons, Annals 171 (2010) §2.4, Theorem 5 (= arXiv v2 Theorem 2 + // with the published `2e` coefficient; verified against the Annals PDF + // 2026-09-01): a lattice path of length L on Z² whose first + // ⌊2e·log(1+√2)·L⌋ GL(2,C)-iterated integrals vanish is tree-like and its // reduced word is trivial. The GL(2,C) integrals are a projection of the // tensor-algebra ones ("a priori contain less information", fn. 2), so // vanishing of the FULL truncated signature to that depth implies it a @@ -368,21 +379,25 @@ mod active { // path, p.8: ‖x_k − x_{k+1}‖ = 1, x_k ∈ Z^{|A|}); // * d ≥ 2 — in d = 1 the reduced-path group is Z (net increment only, // every closed path is tree-like), so the quotient carries nothing. - /// `e · ln(1 + √2)` — Theorem 2's constant, computed rather than retyped. + /// `2e · ln(1 + √2)` — Theorem 5's constant (Annals), computed rather + /// than retyped. pub(super) fn hl_theorem2_constant() -> f64 { - std::f64::consts::E * (1.0 + 2f64.sqrt()).ln() + 2.0 * std::f64::consts::E * (1.0 + 2f64.sqrt()).ln() } - /// The depth Theorem 2 needs for a word of length `l` (floor, as stated). + /// The depth Theorem 5 needs for a word of length `l` (floor, as stated). pub(super) fn hl_theorem2_depth(l: usize) -> usize { (hl_theorem2_constant() * l as f64).floor() as usize } - /// Longest word the exhaustive theorem arm enumerates. Depth ⌊c·5⌋ = 11 - /// in d = 2 is 4096 coefficients — cheap enough for a debug test. - const LATTICE_L_MAX: usize = 5; + /// Longest word the exhaustive theorem arm enumerates. Depth ⌊c·3⌋ = 14 + /// in d = 2 is 32768 coefficients — cheap enough for a debug test. + const LATTICE_L_MAX: usize = 3; /// Length at which the depth-2 false-merge search runs. The paper's own - /// §1.6 figure-of-8 (two equal, opposite lobes) lives here: ⌊c·8⌋ = 19. + /// §1.6 figure-of-8 (two equal, opposite lobes) lives here: ⌊c·8⌋ = 38 + /// (never materialized — the search escalates depth and stops at 3). const LATTICE_FALSE_MERGE_L: usize = 8; const LATTICE_N_TREELIKE: usize = 64; + /// Depth for the tree-like arm (identity holds at every depth; fixed, cheap). + const LATTICE_TREELIKE_DEPTH: usize = 12; /// Exactness tolerance: signatures of lattice words are rationals with /// k! denominators; f64 products of a handful of exponentials round at /// ~1e-15, and a genuinely nonzero coefficient is ≥ 1/k! ≥ 1/19!. @@ -487,11 +502,14 @@ mod active { let mut state: u64 = 0x5EED_1A77_1CE0_0001; let mut treelike_max_dist = 0.0f64; let mut treelike_checked = 0usize; + // Tree-like words are the identity at EVERY depth (Cor. 6.4), so this + // arm needs no theorem depth — a fixed one keeps the length-6 words + // off the 2^29-coefficient tensors the doubled constant would demand. for i in 0..LATTICE_N_TREELIKE { let len = 2 + 2 * (i % 3); // 2, 4, 6 let w = treelike_word(&mut state, len); - let depth = hl_theorem2_depth(len.max(1)); - treelike_max_dist = treelike_max_dist.max(distance_from_identity(&w, depth)); + treelike_max_dist = + treelike_max_dist.max(distance_from_identity(&w, LATTICE_TREELIKE_DEPTH)); treelike_checked += 1; } @@ -644,7 +662,7 @@ mod active { so that leg certifies the converse FUNCTIONAL FORM (deviation is \ quadratic in enclosed Lévy area) and its own resolution boundary, \ not a sampled ratio. \ - THEOREM 2 LATTICE leg (W6, c = e·ln(1+√2) = {:.4}): {} reduced \ + THEOREM 5 LATTICE leg (W6, Annals numbering, c = 2e·ln(1+√2) = {:.4}): {} reduced \ words of length ≤ {} at depth ⌊c·L⌋, {} merged with the identity \ (pass if 0), min ‖S − 1‖ = {:.3e}; {} tree-like words, max \ ‖S − 1‖ = {:.1e} (pass if < {:.0e}); depth-2 false merges among \ @@ -734,14 +752,14 @@ mod tests { #[test] fn theorem2_depth_is_the_paper_floor() { - // ⌊e·ln(1+√2)·L⌋, math/0507536v2 Theorem 2, L = 1..16 + // ⌊2e·ln(1+√2)·L⌋, Annals 171 Theorem 5, L = 1..16 let expect = [ - 2usize, 4, 7, 9, 11, 14, 16, 19, 21, 23, 26, 28, 31, 33, 35, 38, + 4usize, 9, 14, 19, 23, 28, 33, 38, 43, 47, 52, 57, 62, 67, 71, 76, ]; for (i, &e) in expect.iter().enumerate() { assert_eq!(active::hl_theorem2_depth(i + 1), e, "L={}", i + 1); } - assert!((active::hl_theorem2_constant() - 2.3958).abs() < 1e-3); + assert!((active::hl_theorem2_constant() - 4.7916).abs() < 1e-3); } #[test] diff --git a/crates/sigker/src/codec.rs b/crates/sigker/src/codec.rs index 423637439..c52d5c26a 100644 --- a/crates/sigker/src/codec.rs +++ b/crates/sigker/src/codec.rs @@ -41,11 +41,12 @@ //! //! # Certification dependency — LENGTH-PARAMETERIZED (jc Pillar 11, W6) //! -//! Certified 2026-09-01 by jc Pillar 11's Theorem 2 lattice leg +//! Certified 2026-09-01 by jc Pillar 11's Theorem 5 lattice leg //! (`crates/jc/src/hambly_lyons.rs`), NOT at a fixed depth: for unit-step //! lattice walks X, Y in d ≥ 2, `S^(N)(X) = S^(N)(Y) ⟺ X ∼ Y` holds for -//! truncation depth `N ≥ ⌊e·log(1+√2)·(|X|+|Y|)⌋` (d = 2; times -//! `2⌈log₃(d/2)⌉+3` in general — Hambly-Lyons math/0507536v2 Thm 2/3). +//! truncation depth `N ≥ ⌊2e·log(1+√2)·(|X|+|Y|)⌋` (d = 2; times +//! `2⌈log₃(d/2)⌉+3` in general — Hambly-Lyons, Annals 171 (2010) Thm 5/6; +//! the arXiv v2 statement carries a pre-publication `e`, see the pillar). //! So "lossless on the tree-quotient" is TRUE ONLY UNDER A WALK-LENGTH //! BUDGET: a consumer routing paths through `Sigker` must pick its depth //! from the longest walk it will compare, and escalate or refuse beyond diff --git a/crates/sigker/src/lib.rs b/crates/sigker/src/lib.rs index 2fa26a4ed..e37056ee9 100644 --- a/crates/sigker/src/lib.rs +++ b/crates/sigker/src/lib.rs @@ -28,7 +28,7 @@ //! `CodecRoute` variant alongside Passthrough and CamPq. Sigker is //! **Index regime** — by Hambly-Lyons uniqueness, it is lossless on //! tree-quotient classes of paths — at a truncation depth that grows -//! LINEARLY with walk length (Thm 2/3; see `codec.rs`), never at a +//! LINEARLY with walk length (Annals Thm 5/6; see `codec.rs`), never at a //! fixed small depth. //! //! ## Why sigker is Index regime, not Argmax