pillar: bit-exact i128 lattice signature lane + Hambly-Lyons Thm 5/6 certificate - #292
Conversation
…certificate New src/hpc/pillar/lattice_signature.rs (feature `pillar`). For unit-step lattice walks every level-k signature coefficient has denominator k!, so the lane stores k!·S_k as i128: identity is `==`, no tolerance anywhere. Chen composition with a unit step is a binomial convolution against a tensor supported on (a,…,a) only. Depth policy is integer: theorem2_depth(L) = ceil(23959·L/10000) ≥ floor(e·ln(1+√2)·L), the constant re-read from math/0507536v2 p.11/p.14; theorem3_factor(d) = 2·ceil(log3(d/2))+3 by integer loop. Overflow contract: len^depth < 2^126, checked arithmetic, never wrapped. Pinned: 484/484 reduced d=2 words of length ≤ 5 separated at the theorem depth; 64/64 tree-like words exactly the identity; 64 reduced length-8 words share S^(2)=1 with the constant path (the paper's figure-of-8 class) and all separate at level 3; d=1 collapses the 64 length-6 words to exactly 7 tensors; parity with the f32 signature_d2_deg3 lane on every lattice word of length ≤ 6; FNV bit-exactness digest 0xBFAB3E55601E4E41; prove_pillar_11_lattice() deterministic PillarReport. signature.rs stays the f32 kernel-stability battery; this is the uniqueness half, the ndarray twin of lance-graph jc::hambly_lyons W6 (lance-graph #1133) with the f64 tolerance replaced by integer equality. Scalar integer reference lane by design; the W1.5 vectorised lane must reproduce these tensors bit-for-bit. Gates: 11/11 lane tests + doctest, clippy -D warnings, fmt. Blackboard entry added. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QHVUi6Q9XtmKgxh6pDRayP
|
Caution Review failedThe pull request is closed. ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Essentials Run ID: 📒 Files selected for processing (3)
📝 WalkthroughWalkthroughAdded the Pillar-11 lattice-signature lane. It computes checked, factorial-scaled ChangesPillar-11 lattice signatures
Estimated code review effort: 4 (Complex) | ~45 minutes Sequence Diagram(s)sequenceDiagram
participant Caller
participant prove_pillar_11_lattice
participant lattice_signature
participant PillarReport
Caller->>prove_pillar_11_lattice: request Pillar-11 proof
prove_pillar_11_lattice->>lattice_signature: compute and compare lattice signatures
lattice_signature-->>prove_pillar_11_lattice: return measurements
prove_pillar_11_lattice->>PillarReport: build proof report
PillarReport-->>Caller: return results
Suggested reviewers: Poem
✨ Finishing Touches📝 Generate docstrings
Comment |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_60f5a275-7761-49a9-8a36-80535043a3b5) |
…nals Thm 5/6) The lattice lane's depth policy used e·ln(1+√2) ≈ 2.3958 from the arXiv math/0507536v2 preprint (Theorem 2). The published version — Hambly & Lyons, Annals of Math 171 (2010), Theorem 5 — states ⌊2e·log(1+√2)·L⌋, and its proof sets x = 2·log(1+√2)·L. CodeRabbit flagged the discrepancy on lance-graph #1133; the Annals PDF confirms it. Integer policy is now ⌈47917·L/10000⌉ (upper bound on 4.79164…), and every doc/test names Theorems 5/6 with the preprint's Thm 2/3 numbering noted as a version trap. Consequences of the doubled depth: `LATTICE_L_MAX` drops from 5 to 3 (depth 19 at L=4 already allocates 2^19 coefficients per level; the old L=5 arm hung at 2^24+), the tree-like arm runs at a fixed depth 12 (identity holds at every depth), the figure-of-eight test asserts separation at depth 3, and the bit-exact digest is re-pinned over words of length ≤ 3 (`0x7C9612A734212FC6`). Measured: 52/52 reduced words separated, 64/64 tree-like identity, 64/64 depth-2 false merges separated at level 3, d=1 collapses to 7 classes. 11/11 tests, clippy -D warnings clean, fmt clean. Blackboard entry corrected to match. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QHVUi6Q9XtmKgxh6pDRayP
AdaWorldAPI
changed the title
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_0e850d41-b5ba-413f-bad3-83768f6e69d0) |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e1f0e7211d
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| /// bound `⌈47917·len / 10000⌉ ≥ ⌊2e·ln(1+√2)·len⌋`. No floating point. | ||
| #[must_use] | ||
| pub const fn theorem2_depth(len: usize) -> usize { | ||
| (THEOREM2_C_NUM * len + THEOREM2_C_DEN - 1) / THEOREM2_C_DEN |
There was a problem hiding this comment.
On 32-bit targets, valid and representable results can overflow the numerator: for example, theorem2_depth(100_000) should return 479170, but 47_917 * 100_000 exceeds usize, causing a debug panic or a wrapped, insufficient depth in release mode. Compute the quotient and remainder without forming the full product, or use a wider checked intermediate, so this function preserves its advertised theorem bound.
Useful? React with 👍 / 👎.
| for k in 0..=depth { | ||
| c[k][0] = 1; | ||
| for j in 1..=k { | ||
| c[k][j] = c[k - 1][j - 1] + if j <= k - 1 { c[k - 1][j] } else { 0 }; |
There was a problem hiding this comment.
For an empty or one-step one-dimensional walk at depth 131, fits_i128 returns true and the actual scaled signature coefficients are all representable, but constructing Pascal's triangle overflows at C(131, 65). This makes a small, otherwise valid call such as lattice_signature(&[step], 1, 131) panic in debug builds and silently wrap the table in release builds, contradicting the stated overflow contract.
Useful? React with 👍 / 👎.
| #[must_use] | ||
| pub fn letter(dim: usize, l: usize) -> Step { | ||
| if l < dim { | ||
| Step { axis: l as u8, sign: 1 } |
There was a problem hiding this comment.
When dim > 256, converting the generator index to u8 aliases higher axes: for example, letter(257, 256) returns axis 0 rather than axis 256. Consequently for_each_word(257, 1, ...) emits duplicates and can never enumerate walks using the final axis, while the public APIs and general-dimensional theorem helpers document no 256-dimension limit.
Useful? React with 👍 / 👎.
2 participants
What
src/hpc/pillar/lattice_signature.rs(featurepillar): the bit-exact integer signature of a lattice walk, and the finite-depth Hambly-Lyons certificate it makes executable in ndarray. Twin of lance-graphjc::hambly_lyonsW6 (AdaWorldAPI/lance-graph#1133), with the f64 tolerance replaced by integer equality.ksignature coefficient has denominatork!, so the lane storesk!·S_kasi128. Identity is==. No f32, no f64, no tolerance anywhere in the kernel.σ·e_ais a binomial convolution against a tensor supported on(a,…,a)only:(T·E)_k[w] = Σ_{j≤r(w)} C(k,j)·T_{k−j}[w[..k−j]]·σ^j,O(Σ_k d^k·k)per step.theorem2_depth(L) = ⌈47917·L/10000⌉ ≥ ⌊2e·ln(1+√2)·L⌋. The constant is the published one: Hambly & Lyons, Annals of Math 171 (2010), Theorem 5 states⌊2e·log(1+√2)·L⌋and its proof setsx = 2·log(1+√2)·L. The arXiv math/0507536v2 preprint states Theorem 2 withe— a version trap CodeRabbit caught on the lance-graph twin; corrected here ine1f0e72.theorem3_factor(d) = 2⌈log₃(d/2)⌉+3by integer loop. The transcendental constant never enters the code.len^depth < 2^126(fits_i128), checked arithmetic, never wrapped.prove_pillar_11_lattice()returns aPillarReport(psd_rate= separated fraction,n_paths= reduced words,n_hops= depth-2 false merges,lognorm_concentration= deepest separation level).Pins (all exact)
d=2words of length ≤ 3 at the theorem depth (LATTICE_L_MAX = 3: depth 19 at L=4 already allocates2^19coefficients per level)c c⁻¹insertions, seed0x0516DC5ADD11) at fixed depth 12 (identity holds at every depth; the theorem depth for length 6 is 28)S^(2) = 1(the paper's §1.6 figure-of-8 class)3!·S_xxy = 6for the canonical oned = 1fence: all 64 length-6 words on{a, a⁻¹}signature_d2_deg3lane0x7C9612A734212FC6over all words of length ≤ 3 at theorem deptha b a⁻¹ b⁻¹2!·S = (0, 2, −2, 0)— Lévy area 1Disambiguation kept explicit:
signature.rsremains the f32 depth-3 kernel-STABILITY battery; this lane is the UNIQUENESS half.SIMD
Scalar integer reference lane by design. The W1.5 sigker vectorised lane (gated on this pillar, now unblocked) must reproduce these
i128tensors bit-for-bit;ndarray::simdhas noi128lane today, which is the loose end recorded in the blackboard.Gates
cargo test --lib --features std,linalg,pillar lattice_signature→ 11/11; doctest ok;cargo clippy --lib --features std,linalg,pillar -- -D warningsclean;cargo fmt --checkclean. Blackboard entry added and corrected per the repo protocol.🤖 Generated with Claude Code
https://claude.ai/code/session_01QHVUi6Q9XtmKgxh6pDRayP
Summary by CodeRabbit