fix(esn): scale by true spectral radius, not infinity-norm (obligation 1.1)#101
Merged
Conversation
…igation 1.1) scale_to_spectral_radius() scaled the recurrent matrix by its max absolute row sum (the infinity-norm), which only bounds the spectral radius from above — so the configured spectral_radius (e.g. 0.9) was never the value actually realised. - Add estimate_spectral_radius() via power iteration (deterministic start vector, convergence-checked) — the quantity that genuinely governs the Echo State Property. - scale_to_spectral_radius() now scales by the estimated spectral radius, so the configured value is achieved. - Tests: diagonal-matrix radius estimate, and that scaling realises the target ρ. https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
…igration in flight) (#105) ## Summary The `android/` subtree is owner-authored Kotlin/Gradle work-in-flight currently being migrated to Gossamer (see RFC PR #97). It is not vendored upstream — it is intentional code. Two complementary governance checks currently treat it as a banned-language violation: - `Check for Banned Languages` (this repo's `.github/workflows/language-policy.yml` — self-contained `find -name '*.kt' ...`) - `governance / Language / package anti-pattern policy` (the standards reusable's `Check banned-language files` step — honours `.hypatia-ignore` + `.hypatia-baseline.json`) This PR adds a coordinated carve-out for both. After it lands on `main`, the recently-merged PR #101 (ESN spectral-radius scaling — obligation 1.1) inherits the carve-out for any follow-up CI runs, and future Android-touching PRs go green by default until the Gossamer migration lands and `android/` is removed. ## Changes **Commit 1 — `chore(cicd): add android/** carve-out to .hypatia-ignore`** Adds two complementary exemption files at the repo root: - `.hypatia-baseline.json` — canonical glob form (`file_pattern: "android/**"`) with `tracking_issue: "#97"`. Consumed by the standards governance-reusable workflow's `in_baseline()` helper (glob → regex translation: `**` → `.*`). - `.hypatia-ignore` — legacy per-file enumeration (10 lines, one per currently-tracked `.kt`/`.kts` file). Belt-and-braces for any tool that only reads the flat-file form (the governance reusable's `is_exempt()` checks both; `grep -qxF` requires literal lines, not globs). **Commit 2 — `ci(language-policy): exclude android/ from Java/Kotlin banned-language scan (Gossamer migration in flight — RFC #97)`** Edits the `Check for Java/Kotlin files` step in `.github/workflows/language-policy.yml`. The inline workflow does not read `.hypatia-ignore`, so it needs its own path exclusion. Replaces the single-line `find -name '*.kt' ...` with a `-prune` + `-o` form that excludes `./android/` and `./.git/`: ```bash VIOLATIONS=$(find . \ \( -path './android' -o -path './android/*' -o -path './.git/*' \) -prune -o \ \( -name "*.java" -o -name "*.kt" -o -name "*.kts" \) -type f -print) ``` ## Verification Local verification before push: - New `find` pattern returns empty on the current tree. - Old `find` would have caught 10 files under `android/`. - `git ls-files '*.kt' '*.kts' '*.java' | grep -v '^android/'` returns empty — no non-Android Kotlin/Java anywhere, so the carve-out is precise. ## Rollback condition Once the Gossamer migration (RFC PR #97) lands and `android/` is removed from the repo, all three additions (`.hypatia-baseline.json`, `.hypatia-ignore`, and the `find -prune` clause in `language-policy.yml`) should be removed together. ## Related - RFC PR #97 — Android Kotlin → Rust/Gossamer migration (the work that makes this carve-out time-bounded). - PR #101 — ESN spectral-radius scaling (already MERGED; the two governance checks were the last red on it).
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
## Proof-obligation map (#84) — Tiers 0–3, batched Full lowest-tier-first. Entire workspace: `cargo clippy --workspace --all-targets` clean, `cargo test --workspace` all green. ### Tier 0 — foundations - **0.1 panic-freedom (#86)** — 6 operational `unwrap`/`expect` removed; `cfg_attr(not(test), deny(clippy::unwrap_used, expect_used))` on every crate. - **0.2 numeric containment (#87)** — proptest no-NaN/Inf for `esn::step`, `lsm::step`, sensors IIR. - **0.3 unsafe discipline** — `deny`/`forbid` (on main). ### Tier 1 — core algorithmic correctness - **1.1 Echo State Property (#88)** — true spectral radius via power iteration (merged in #101). - **1.2 LSM bounded dynamics (#89)** — same spectral-radius fix in lsm + membrane/spike-history bounds proptest. - **1.3 bridge soundness (#90)** — totality / determinism / bounded-output proptest. ### Tier 2 — system orchestration - **2.1 lifecycle (#91)** — compile-time **typestate** (`Created→Active→Down`, terminal shutdown); illegal transitions don't compile. Matches `proofs/tla/Lifecycle.tla`. - **2.2 concurrency (#92)** — no-lost-updates stress test (8×250); data-race & deadlock freedom argued from safe-Rust + single-lock. - **2.3 resource/affine (#93)** — design spec (`proofs/affine/`); Rust ownership gives acquire-release-once today, AffineScript linear handles deferred. ### Tier 3 — trust boundary - **3.1 data-egress (#94)** — egress allow-list test (API key stays a header; no device/sensor fields in body) + neural-context-not-sent-when-disabled. - **3.2 bounded external interaction (#95)** — saturating/capped backoff (fixes a latent `pow` overflow); injection-safety via typed JSON. Closes #86 #87 #89 #90 #91 #92 #94 #95 (1.1/#88 already merged via #101; 2.3/#93 remains a tracked spec). _The two Kotlin banned-language CI checks are red from `main`'s `android/` app (tracked in #83), not from this PR._ https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw --------- Co-authored-by: Claude <noreply@anthropic.com>
This was referenced Jun 2, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
esn::scale_to_spectral_radiusscaled the recurrent matrix by its max absolute row sum (the matrix ∞-norm), which only bounds the spectral radius from above (ρ(W) ≤ ‖W‖∞). So the configuredspectral_radius(e.g.0.9) was never the value actually realised — the true ρ was some unknown smaller number. This is the genuine correctness bug behind obligation 1.1 (Echo State Property).Fix
estimate_spectral_radius()— power iteration (deterministic non-degenerate start vector, convergence-checked, nilpotent/zero-matrix guards). This estimates |λ_max|, the quantity that actually governs the Echo State Property.scale_to_spectral_radius()now scales by the estimated spectral radius, so the configured value is achieved.Tests (added)
test_spectral_radius_estimate_diagonal— diagonal matrix ρ = max|diag| (exact for power iteration).test_scale_to_spectral_radius_achieves_target— after scaling, the re-estimated ρ = 0.9, proving the target is realised (not merely bounded).cargo test -p esn→ 11 unit + 6 integration pass.Notes
main; clean (no licence churn — that's tracked separately).Closes #88
https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
Generated by Claude Code