allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge origin/main (doc archival + GLOSSARY revision) into main with spectral codebook

Browse source 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
allaun 2026-07-01 21:01:51 -05:00
commit e85c8dd7bd
33 changed files with 48 additions and 2118 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
archive/2026-07-02/docs/avm_isa_audit.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 45752c034586c3e46f76e81419f462cf7d686ed6)

1
archive/2026-07-02/docs/avm_ports_audit.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 51806352a794cfe5f26cd68f4f2173ccc53072b5)

1
archive/2026-07-02/docs/cartan_dna_derivation.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 2c0c33aa1d789a5215f47527a14fd1cfd1139086)

1
archive/2026-07-02/docs/cartan_fingerprint.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 88dd5560a20150b0418f2f0ac9020ab5ddc23623)

1
archive/2026-07-02/docs/gemma4_pdf_benchmark.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: cb0c8185f7b68daf6893ffa524eb12cd94b58f14)

1
archive/2026-07-02/docs/hachimoji_torsor_consequences.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 921bd97b4fb8853b8fed060069e7ceb33d142005)

1
archive/2026-07-02/docs/helical_encoding.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 2682cfa451d565f8bcd139f3907272ec485000c0)

1
archive/2026-07-02/docs/hopf_ingest_bridge.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 508ce1946138b8f60b68c70fc611beb2118d422b)

1
archive/2026-07-02/docs/hopf_portability_criterion.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 5a9b9353f25dcdfad50afe2c03ee1b16fc5dad4e)

1
archive/2026-07-02/docs/milestone_avm_11_port_coverage.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 87bda1dc4b3ccf3f1f0f1bbfb6426c54797009f3)

1
archive/2026-07-02/docs/noether_route.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 5737002e86a7f566e605fc4cfb408619a413bb73)

1
archive/2026-07-02/docs/rossby_e8_completion_roadmap.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: dd6bf0a81b810688f37a732394d48edfc6af3e05)

1
archive/2026-07-02/docs/rotational_wave_braid_correspondence.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 860f8cf134c35d3173e64b66bf6fe8aae601d8aa)

1
archive/2026-07-02/docs/transform_series.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 58dc315f3d250f15cba88563d301c07a7c082fe1)

1
archive/2026-07-02/specs/braidtree_octree_couch_synthesis.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 7904327892a9952791c517b0094abf590e9ab144)

1
archive/2026-07-02/specs/rydberg_braid_cross_domain_scan.md Normal file
View file

@ -0,0 +1 @@
successfully downloaded text file (SHA: 57c8efd49d99f49eaca925f327498d9abe580fc4)

275
docs/GLOSSARY.md
View file

@ -1,262 +1,51 @@
# SilverSight Glossary
A living dictionary of terms used across the SilverSight core, libraries,
documentation, and receipts. When you introduce a new domain term, add it here
and cite the module that owns the definition.
A living dictionary of terms used across the SilverSight core, libraries, documentation, and receipts.
**Rule:** every entry must name the authoritative source file or module. A
glossary entry without a source module is a draft; it must be promoted to a
bound definition before it is used in a receipt or gate.
**Rule:** Every entry must name the authoritative source file or module. A glossary entry without a source module is a draft; it must be promoted to a bound definition before it is used in a receipt or gate.
**Deep Wiki Compatible:** Each entry includes File:Line references, tags for categorization, and cross-references to related terms.
---
## Standard terminology crosswalk
## Standard Terminology Crosswalk
SilverSight invents names only when necessary. When a concept already exists
under a standard name, the glossary binds the SilverSight name to the standard
name and explains the delta.
SilverSight invents names only when necessary. When a concept already exists under a standard name, the glossary binds the SilverSight name to the standard name and explains the delta.
| SilverSight term | Standard terminology | Delta / note |
|------------------|----------------------|--------------|
| **Sidon set** | B₂ sequence, Erdős–Sidon set | Standard combinatorial object; SilverSight uses it for deterministic strand addressing. |
| **Sidon label** | Sidon-set element, B₂ address | Chosen from the canonical powers-of-2 set for 8-strand braids. |
| **Q16_16** | Fixed-point arithmetic, Q15.16 / s16.16 | Signed 32-bit fixed point with 16 integer and 16 fractional bits. |
| **BraidStorm** | Braid group representation, Artin braid | 8-strand braid action used as a compression/determinism substrate. |
| **eigensolid** | Fixed point, attractor | Fixed point of the `crossStep` operator; not a physical solid. |
| **crossStep** | Braid generator / crossing operator | One deterministic update step in the braid dynamics. |
| **AVM** | Abstract/virtual machine, stack machine | SilverSight-specific instruction set and transition relation. |
| **TIC** | Logical clock, event counter | Monotone counter derived from AVM transitions. |
| **Receipt** | Attestation, certificate, proof certificate | Machine-readable record of a gate result; the compressed state. |
| **Hachimoji** | 8-letter alphabet, octal state | The 8-symbol output alphabet of the core classifier. |
| **Finsler-Randers** | Asymmetric metric, quasimetric | Directed routing cost with anisotropy parameter β. |
| **QUBO** | Ising model, binary quadratic optimization | Energy minimization over binary variables. |
| **meta-solid** | Topological triple point, phase coexistence | Point where three independent equivalence relations collapse. |
| **promotion** | Certification, acceptance | Status advance only after a formal gate passes. |
| **quarantine** | Archive, staging, broken build exclusion | Module kept out of the active build until repaired. |
| **Genome18** | Codon LUT, k=6 fixed-point address | Research Stack vocabulary-lock name for `CodonLUT (k=6)`: 6 × 3-bit Hachimoji inputs → 18-bit address. SilverSight binds this to `formal/CoreFormalism/HachimojiLUT.lean CodonLUT`. |
| **equationPosition** | Manifold localization, equation embedding | The deterministic map `EquationShape → SpherePoint` that answers "where does this equation live on the manifold?" |
| SilverSight Term | Standard Terminology | Delta / Note | File:Line | Tags | See Also |
|------------------|----------------------|--------------|-----------|------|----------|
| **Sidon set** | B₂ sequence, Erdős–Sidon set | Standard combinatorial object; SilverSight uses it for deterministic strand addressing. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical #core | [Sidon label](#sidon-label) |
| **Sidon label** | Sidon-set element, B₂ address | Chosen from the canonical powers-of-2 set for 8-strand braids. | formal/CoreFormalism/InteractionGraphSidon.lean:L1 | #mathematical #core | [Sidon set](#sidon-set) |
| **Q16_16** | Fixed-point arithmetic, Q15.16 / s16.16 | Signed 32-bit fixed point with 16 integer and 16 fractional bits. | Core/SilverSight/FixedPoint.lean:L1 | #core #implementation | [Q0_16](#q0_16) |
| **BraidStorm** | Braid group representation, Artin braid | 8-strand braid action used as a compression/determinism substrate. | formal/CoreFormalism/BraidEigensolid.lean:L1 | #mathematical #core | [eigensolid](#eigensolid) |
| **eigensolid** | Fixed point, attractor | Fixed point of the crossStep operator; not a physical solid. | formal/CoreFormalism/BraidEigensolid.lean:L42 | #mathematical #core | [crossStep](#crossstep) |
| **crossStep** | Braid generator / crossing operator | One deterministic update step in the braid dynamics. | formal/CoreFormalism/BraidCross.lean:L1 | #mathematical #core | [eigensolid](#eigensolid) |
| **AVM** | Abstract/virtual machine, stack machine | SilverSight-specific instruction set and transition relation. | Core/SilverSightCore.lean:L1 | #core #implementation | [TIC](#tic) |
| **TIC** | Logical clock, event counter | Monotone counter derived from AVM transitions. | Core/SilverSightCore.lean:L1 | #core #implementation | [AVM](#avm) |
---
## Core terms
## Core Terms
| Term | Definition | Source module |
|------|------------|---------------|
| **Hachimoji state** | One of the 8 output symbols `Φ Λ Ρ Κ Ω Σ Π Ζ` produced by the core classifier. | `Core/SilverSightCore.lean` |
| **Receipt** | The compressed, machine-readable attestation record that crosses the Core/library boundary. It is not metadata around a result; it *is* the result. | `Core/SilverSightCore.lean` |
| **AVM** | Adaptive Virtual Machine. The stack-machine transition semantics `δ` defined in the core; the universal bridge between math languages and executable traces. | `Core/SilverSightCore.lean` |
| **TIC** | Temporal Index of Computation. A monotone event counter derived from AVM state transitions. | `Core/SilverSightCore.lean` |
| **pathCost** | Raw integer cost metric carried on a `Receipt`; never a `Float`. | `Core/SilverSightCore.lean` |
| **Library method** | The architecture rule: `Core/` defines contracts, libraries implement them, and no library imports another library. | `AGENTS.md` |
| **Core** | The invariant center of SilverSight: `Core/SilverSightCore.lean` and `Core/SilverSight/FixedPoint.lean`. Defines Receipt, AVM, TIC, and canonical Q16_16. | `AGENTS.md` |
| **Schema** | Typeclass describing fixed-size, well-formed data: `byteSize` and `wellFormed`. | `Core/SilverSight/Semantics/Schema.lean` |
| **byteSize** | Number of bytes occupied by a value of a `Schema` type; constant and statically known. | `Core/SilverSight/Semantics/Schema.lean` |
| **wellFormed** | Predicate asserting that a value satisfies its `Schema` invariants. | `Core/SilverSight/Semantics/Schema.lean` |
| **Layout** | Physical data placement: `rowMajor`, `columnar`, `compact`, `mmapView`. | `Core/SilverSight/Semantics/Layout.lean` |
| **AccessProfile** | Read/write mix used by the layout cost model. | `Core/SilverSight/Semantics/Layout.lean` |
| **WireFormat** | Certified encoder/decoder pair for a `Schema` under a `Layout`. | `Core/SilverSight/Semantics/WireFormat.lean` |
| **roundTrip** | WireFormat axiom: `decode (encode a) = some a` for every value. | `Core/SilverSight/Semantics/WireFormat.lean` |
| **View** | Zero-copy, address-bounded window into a `ByteArray`. | `Core/SilverSight/Semantics/View.lean` |
| **LayoutBridge** | Certified conversion between two `Layout`s with a round-trip guarantee. | `Core/SilverSight/Semantics/LayoutBridge.lean` |
| **CanalRegime** | Storage regime (`cold`, `warm`, `hot`, `flash`) used by layout selection. | `Core/SilverSight/Semantics/CanalLayout.lean` |
| **CanalLayout** | Module that maps `CanalRegime` to a preferred `Layout` and profile. | `Core/SilverSight/Semantics/CanalLayout.lean` |
| **rowMajor** | Default `Layout`: fields stored contiguously in declaration order. | `Core/SilverSight/Semantics/Layout.lean` |
| **mmapView** | `Layout` optimized for memory-mapped, read-only access. | `Core/SilverSight/Semantics/Layout.lean` |
| **BraidState** | Aggregated braid carrier state used by the eigensolid compressor. | `formal/CoreFormalism/BraidState.lean` |
## RRC / AVM ISA
| Term | Definition | Source module |
|------|------------|---------------|
| **RRC** | Receipt Routing Classifier. Aligns PIST structural labels with RRC semantic routing shapes and emits gate receipts. | `formal/SilverSight/RRC/Emit.lean` |
| **CoreFormalism** | The SilverSight foundational library containing canonical Q16_16, Sidon sets, braid dynamics, and related lemmas. | `formal/CoreFormalism/` |
| **RRCShape** | One of six lawful routing shapes: `cognitiveLoadField`, `signalShapedRouteCompiler`, `logogramProjection`, `projectableGeometryTopology`, `cadForceProbeReceipt`, `holdForUnlawfulOrUnderspecifiedShape`. | `formal/SilverSight/RRCLogogramProjection.lean` |
| **WitnessStatus** | `candidate` (admits next-stage checks) or `hold` (blocked pending more evidence). | `formal/SilverSight/RRCLogogramProjection.lean` |
| **LogogramReceipt** | Receipt core for one compiled logogram projection, carrying shape, status, regime, and tear evidence. | `formal/SilverSight/RRCLogogramProjection.lean` |
| **FixtureRow** | One compiled equation record with raw features and optional PIST labels; input to the RRC alignment gate. | `formal/SilverSight/RRC/Emit.lean` |
| **AlignmentStatus** | Result of `determineAlignment`: `alignedExact`, `alignedProxy`, `compatibleStructuralProjection`, `alignmentWarning`, or `missingPrediction`. | `formal/SilverSight/RRC/Emit.lean` |
| **determineAlignment** | RRC alignment gate that maps a `FixtureRow` and optional PIST labels to an `AlignmentStatus`. | `formal/SilverSight/RRC/Emit.lean` |
| **AvmTy** | Closed-world AVM type universe: `q0_16`, `q16_16`, `bool`. | `formal/SilverSight/AVMIsa/Types.lean` |
| **AvmVal** | Typed AVM value payload indexed by `AvmTy`. | `formal/SilverSight/AVMIsa/Value.lean` |
| **Instr** | AVM instruction set: `push`, `pop`, `dup`, `swap`, `load`, `store`, `jump`, `jumpIf`, `prim`, `halt`. | `formal/SilverSight/AVMIsa/Instr.lean` |
| **Prim** | Finite AVM primitive set: boolean ops and saturating Q0_16/Q16_16 add/sub. | `formal/SilverSight/AVMIsa/Instr.lean` |
| **AVMIsa.Emit** | Top-level JSON output boundary. Stamps AVM canary receipts and RRC corpus bundles. | `formal/SilverSight/AVMIsa/Emit.lean` |
| **TDoku16D** | Projected gradient descent constraint propagation on the 16D subspace $L1 \oplus L2$ using $Q16\_16$ integer steps. | `formal/SilverSight/PIST/Tdoku16D.lean` |
| **CrossDomainSynthesis** | Enclosure and defect proof boundaries validating critical ratios and $1/n$ scaling thresholds. | `formal/SilverSight/PIST/CrossDomainSynthesis.lean` |
| **MultiSurfacePacker** | Multi-surface $\Delta\Phi\Gamma\Lambda$ Lagrangian optimization decision logic and GCCL swap gating. | `formal/SilverSight/PIST/MultiSurfacePacker.lean` |
## Fixed-point and numerics
| Term | Definition | Source module |
|------|------------|---------------|
| **Q16_16** | Canonical 32-bit fixed-point type: 16 integer bits and 16 fractional bits. The sole source of truth for core arithmetic. | `Core/SilverSight/FixedPoint.lean` |
| **Q0_16** | 16.16-style fixed-point interpretation used for bounded unit-interval quantities. | `Core/SilverSight/FixedPoint.lean` |
| **ofFloat** | Conversion from `Float` to `Q16_16`. Permitted **only** at external boundaries (JSON parsing, sensor input); must be immediately bracketed. | `AGENTS.md` |
| **ofNat / ofRatio / ofRawInt** | Canonical constructors for `Q16_16` values in compute paths. | `Core/SilverSight/FixedPoint.lean` |
| **Float** | IEEE-754 floating-point type. Forbidden in SilverSight compute paths; permitted only at external JSON/sensor boundaries and must be immediately converted to `Q16_16`. | `AGENTS.md` |
## Braid / eigensolid compression
| Term | Definition | Source module |
|------|------------|---------------|
| **BraidStorm** | The 8-strand braid topology used by the eigensolid compressor. Strands cross pairwise; each crossing merges phase and produces a residual. | `formal/CoreFormalism/BraidEigensolid.lean` |
| **eigensolid** | The converged, stable state of a braid crossing loop; detected when `crossStep(s) = s`. | `formal/CoreFormalism/BraidEigensolid.lean` |
| **crossStep** | One braid-crossing iteration that merges phase and emits a residual. | `formal/CoreFormalism/BraidCross.lean` |
| **strand** | A single braided carrier with phase accumulator, parity, slot, residue, jitter, and admissibility bracket. | `formal/CoreFormalism/BraidStrand.lean` |
| **Yang-Baxter** | The braid relation `βij βjk βij = βjk βij βjk` that defines braid-order invariance. | `formal/CoreFormalism/BraidEigensolid.lean` |
| **Anti-BraidStorm** | Adversarial dual that tests Yang-Baxter invariance and receipt aliasing. | `PORTING_MAP.md` (planned) |
## Sidon / number theory
| Term | Definition | Source module |
|------|------------|---------------|
| **Sidon set** | A set where all pairwise sums `a + b` are unique up to reordering. | `formal/CoreFormalism/SidonSets.lean` |
| **Sidon label** | An address from a Sidon set. Powers of 2 `{1,2,4,8,16,32,64,128}` are canonical for 8 strands. | `formal/CoreFormalism/InteractionGraphSidon.lean` |
| **Sidon slack** | Address budget minus the maximum label used; encodes capacity headroom. | `formal/CoreFormalism/SidonSets.lean` |
| **IsIntervalSidon** | Predicate stating that a finite set is a Sidon subset of `{1,…,N}`. | `formal/CoreFormalism/SidonSets.lean` |
| **IsSidonMod** | Predicate stating that a set is Sidon modulo `M`: sums are unique up to congruence. | `formal/CoreFormalism/SidonSets.lean` |
| **sidonMaximum** | Extremal function `h(N)` returning the maximum size of an interval Sidon set. | `formal/CoreFormalism/SidonSets.lean` |
| **Singer theorem** | Existence of a Sidon set of size `q+1` modulo `q²+q+1` for prime powers `q`. | `formal/CoreFormalism/SidonSets.lean` |
| **Lindström bound** | Upper bound `|A| ≤ √N + O(N^{1/4})` for interval Sidon sets. | `formal/CoreFormalism/SidonSets.lean` |
| **interaction graph** | Typed directed graph whose adjacency matrix is tested for the Sidon witness property. | `formal/CoreFormalism/InteractionGraphSidon.lean` |
| **weak-axis CRT** | Chinese Remainder Theorem reconstruction used for RRC weak-axis classification. | `formal/CoreFormalism/SieveLemmas.lean` |
## RRC / receipt classification
| Term | Definition | Source module |
|------|------------|---------------|
| **RRC** | Receipt / Rank / Classify pipeline. The decision layer that admits or rejects prediction rows. | `PORTING_MAP.md` |
| **Q16_16Manifold** | The 250-equation raw-feature corpus used for RRC training and alignment. | Research Stack `Semantics.RRC.Q16_16Manifold` (planned) |
| **emit** | The sole output boundary for top-level receipt JSON. Only the designated emitter may stamp a receipt. | `AGENTS.md` |
| **promotion** | Status advance from `not_promoted` to `promoted` only after a Lean gate explicitly passes. | `AGENTS.md` |
## Hachimoji Manifold & LUT (added 2026-06-22)
| Term | Definition | Source module |
|------|------------|---------------|
| **PhaseCircle** | ℤ/360ℤ — 360 discrete phase positions with `AddCommGroup` structure. Foundation of the Hachimoji encoding; the 8 canonical bases occupy the order-8 subgroup at multiples of 45°. | `formal/CoreFormalism/HachimojiLUT.lean §0` |
| **phaseEmbed** | Embedding `PhaseCircle → SpherePoint`; maps phase θ to `(cos(θ·π/180), 0, sin(θ·π/180), 0, …)` on S¹⁵. Corrected from v.01: uses `π/180` (full period) not `π/360` (semicircle). | `formal/CoreFormalism/HachimojiLUT.lean §2` |
| **SpherePoint** | A point on S¹⁵: 16-vector `coords : Fin 16 → ℝ` satisfying `∑ coords i ^ 2 = 1`. Represents one character position in the 16D DQ complexified quaternion space. | `formal/CoreFormalism/HachimojiLUT.lean §2` |
| **stateIndex** | `HachimojiState4D → Fin 8`; maps each canonical Hachimoji state to its index 0–7 via `phase / 45 % 8`. Resolves the missing `Base.index` from the v.01 exploration file. | `formal/CoreFormalism/HachimojiLUT.lean §1` |
| **equationPosition** | `EquationShape → SpherePoint`; the formal bridge from equation structure to manifold position. Pipeline: `classifyEquation → stateToPhase → phaseEmbed`. | `formal/CoreFormalism/HachimojiLUT.lean §4` |
| **VirtualLUT** | A mapping from k sphere points to one output, defined by manifold geometry rather than stored memory. Three levels: k=2 (BinaryLUT), k=6 (CodonLUT), k=50 (GenomeLUT). | `formal/CoreFormalism/HachimojiLUT.lean §5` |
| **BinaryLUT** | `VirtualLUT 2`; composition table for pairs of Hachimoji states (8×8 = 64 entries). Defines how two equations compose geometrically. | `formal/CoreFormalism/HachimojiLUT.lean §5` |
| **CodonLUT** | `VirtualLUT 6`; 6-character Hachimoji codon mapping to one admitted state. Direct formal correspondent of the Research Stack `Genome18` primitive (6 × 3-bit bins → 18-bit address). | `formal/CoreFormalism/HachimojiLUT.lean §5` |
| **GenomeLUT** | `VirtualLUT 50`; universal 50-character Hachimoji string mapping to a path on (S¹⁵)⁵⁰. Corresponds to the `UniversalMathEncoding` 50-token address space. | `formal/CoreFormalism/HachimojiLUT.lean §5` |
| **stability point** | A phase θ fixed under conjugation `θ ↦ −θ` on ℤ/360ℤ. Proved: exactly {0°, 180°} = Φ (trivial) and Ω (collision). These are the self-complementary (ambidextrous) bases — the "DNA palindromes" of the encoding. | `formal/CoreFormalism/HachimojiLUT.lean §6` |
| **conjugate** | `PhaseCircle → PhaseCircle`; the map `θ ↦ (360 - θ) % 360`. The binding law dual to Watson-Crick complementarity: each base pairs with its conjugate; stability points are self-paired. | `formal/CoreFormalism/HachimojiLUT.lean §6` |
| **octagon chord** | Euclidean distance between adjacent canonical bases under `phaseEmbed`; equals `sqrt(2 - 2·cos(π/4)) = 2·sin(π/8) ≈ 0.7654`. Proved formally (not vacuous as in v.01). | `formal/CoreFormalism/HachimojiLUT.lean §2` |
| **HachimojiTokenEmbed** | Planned module for fine-grained manifold position. Uses Fourier harmonics of the phase angle across all 16 S¹⁵ coordinates: coords (0,2) = (cos θ, sin θ), (4,6) = (cos 2θ, sin 2θ), (8,10) = (cos 4θ, sin 4θ), (12,14) = (cos 8θ, sin 8θ). Gauge-equivariant under state relabeling; norm constraint provable via `cos_sq_add_sin_sq`. See `docs/hachimoji_torsor_consequences.md` §2. | Planned: `formal/CoreFormalism/HachimojiTokenEmbed.lean` |
## Physics / applied math (ported concepts)
| Term | Definition | Source module |
|------|------------|---------------|
| **meta-solid** | Topological triple point where trace closure, local Yang-Baxter isotopy, and braid class are simultaneously exact. | ContextStream node `e967f515-3af9-46c9-9fc8-e5c766a6c4fc`; bound to `formal/CoreFormalism/BraidEigensolid.lean` |
| **Finsler-Randers** | Directed routing metric used in the QUBO/TSP benchmark. | `qubo/finsler_metric.py` (planned) |
| **QUBO** | Quadratic Unconstrained Binary Optimization; a classical/quantum optimization encoding. | `qubo/qubo_builder.py` (planned) |
| **BMCTE** | Bosonic Monte Carlo Tensor Estimation class: problems solvable by O(S·(Np+p²2^p)) stochastic contraction of Sym^p(U) without explicit Fock-space construction. | `experiments/bosonic_continuous/kernel/ryser_continuous.py` |
| **BoseMonteCarloEstimator** | Stochastic estimator P^p(U) = Σ_k |Per(U_{S_k})|² / K! using Monte Carlo sampling of mode configurations with Ryser permanent evaluation. | `4-Infrastructure/shim/rrc_bosonic_tensor_network.py` |
| **ContinuousInterpolation** | λ(p) = exp(-p²/N) smooth blending parameter between fully bosonic (λ→1) and weakly-correlated (λ→0) regimes. | `experiments/bosonic_continuous/tests/test_lambda_interpolation.py` |
| **EntropyInvarianceHypothesis** | In BMCTE regime, Shannon entropy H(p) ≈ 10 bits remains constant across p=1..6 for N=2000, indicating projection-dominated measurement rather than full-state exploration. | `experiments/bosonic_continuous/README.md` |
## Symbolic Regression (added 2026-06-22)
| Term | Definition | Source module |
|------|------------|---------------|
| **ExprNode** | Expression tree node: leaf (variable 'x' or constant) or internal (unary/binary operator). Supports evaluate, to_string, complexity, copy. | `python/expr_tree.py` |
| **Linear Scaling** | Keijzer 2003 technique: GP searches for shape g(x), closed-form solves f(x) = a·g(x) + b via least squares. Reduces search space dramatically. | `python/linear_scaling.py` |
| **BIC Fitness** | Bayesian Information Criterion: `n·ln(MSE) + k·ln(n)` where k = weighted complexity (var=1, const=3). Penalizes overfitting. | `python/expr_tree.py` |
| **Chaos Game Search** | IFS contraction over expression space: at each step, try to improve best expression by applying transformations. Deterministic (same input → same output). | `python/expr_tree.py` |
| **Hachimoji-Guided Search** | Use classifyEquation to partition expressions into 8 Hachimoji states (Φ=trivial, Σ=symmetric, Λ=quantified, Π=complex, Ω=contradiction). Force diversity across states. | `python/hachimoji_citation.py` |
| **Log Prescreen** | Before expression tree search, try log-log, log-y, y-x transforms. If R² > 0.999, return as discovered law. Collapses O(tree search) to O(linear regression) for power laws, exponentials, polynomials. | `python/log_prescreen.py` |
| **Finite-Infinity Duality** | SilverSight's core principle: tame infinity with finite structure. Logarithms compress combinatorial explosion; Hachimoji encoding bounds Gödel's undecidable. Both are lossy compressions that preserve enough structure to discover physical laws. | `docs/FINITE_INFINITY_DUALITY.md` |
| **Gödel Boundary** | The 8-state Hachimoji encoding is a finite boundary on infinite undecidable equation space. If extended to self-referential equations (Gödel sentences), it would need to classify "this equation is not classifiable" — a NaN event. The admission gate (ADMIT/QUARANTINE/HOLD) controls this boundary. | `formal/CoreFormalism/HachimojiCodec.lean` |
## Modules and library layers
| Term | Definition | Source module |
|------|------------|---------------|
| **FixedPoint** | The Lean module that defines the canonical `Q16_16`/`Q0_16` fixed-point implementation. | `Core/SilverSight/FixedPoint.lean` |
| **SieveLemmas** | Lean module for coprime-sieve observers and CRT reconstruction. | `formal/CoreFormalism/SieveLemmas.lean` |
| **InteractionGraphSidon** | Lean module for typed interaction graphs and Sidon witnesses. | `formal/CoreFormalism/InteractionGraphSidon.lean` |
| **BraidEigensolid** | Lean module for the braid crossing loop and eigensolid fixed-point theorems. | `formal/CoreFormalism/BraidEigensolid.lean` |
| **BraidSpherionBridge** | Lean module bridging braid dynamics to spherion / twin-prime constructions. | `formal/CoreFormalism/BraidSpherionBridge.lean` |
| **SilverSightRRC** | Lean library containing the RRC decision surface, receipt bridge, and AVM ISA emit boundary. | `lakefile.lean` |
| **RRCLib** | User-facing symlink directory for the Receipt / Rank / Classify surface. | `formal/RRCLib/` |
| **RrcEmitFixture** | Lean executable that emits the AVM-stamped RRC fixture corpus JSON. | `exe/RrcEmitFixture.lean` |
| **emitFixtureCorpus** | Top-level JSON bundle for the 6-row RRC fixture corpus. | `formal/SilverSight/AVMIsa/Emit.lean` |
| **toSilverSightReceipt** | Bridge from `SilverSight.ReceiptCore.Receipt` to `SilverSight.Core.Receipt`. | `formal/SilverSight/ReceiptCore.lean` |
| **SearchLib** | Planned library layer for search-space exploration (chaos game, entropy candidates). | `PORTING_MAP.md` |
| **LexLib** | Planned library layer for lexical / symbolic encodings. | `PORTING_MAP.md` |
| **StructureLib** | Planned library layer for structural / manifold encodings. | `PORTING_MAP.md` |
| **QUBOLib** | Planned library layer for QUBO/QAOA optimization bridges. | `PORTING_MAP.md` |
| **PVGSLib** | Planned library layer for photon-varied Gaussian state bridges. | `PORTING_MAP.md` |
## Concept Map & Academic Citations
| Term | Definition | Source module |
|------|------------|---------------|
| **Concept Map** | JSONL artifact mapping files to extracted concepts with types, tags, dependencies, and summaries. 822 local + 752 Drive files. | `docs/concept_map/` |
| **Cornfield Concepts** | 48 formally grounded concepts with academic citations, novelty classification, and novelty_statements. | `extraction/cornfield_concepts.json` |
| **concept_citations** | Postgres table linking concepts to papers via paper_id, doi, title, authors, year, journal, relation_type. Now includes 480 hybrid citations from pgvector RRF matching. | neon-64gb `arxiv` DB |
| **paper_refs** | JSONB column storing structured citation array on math_objects. | neon-64gb `arxiv` DB |
| **is_novel_claim** | Boolean flag: true = original work, no prior paper covers exactly this. Requires novelty_statement. | neon-64gb `arxiv` DB |
| **relation_type** | Citation edge: `grounds` (foundational), `extends` (builds on), `applies` (application), `cites` (general), `hybrid` (RRF-trigram+vector). | neon-64gb `arxiv` DB |
| **Jaccard Matcher** | Deprecated script finding arxiv papers via keyword overlap. Replaced by hybrid_search. | `python/hachimoji_citation.py` (historical) |
| **Hybrid Matcher** | Equation-to-citation pipeline using pgvector HNSW + pg_trgm RRF (22ms query, 397x faster than transformer models). Mirrors `HachimojiCodec.lean` classifyEquation. | `python/hachimoji_citation.py` |
| **hachimoji_citation** | Equation → Hachimoji state → arXiv paper bridge. Computes structural features, classifies to one of 8 states, builds semantic query, retrieves top-k papers. Mirrors `formal/CoreFormalism/HachimojiCodec.lean`. | `python/hachimoji_citation.py` |
| **static-retrieval-mrl-en-v1** | Sentence-transformers embedding model (1024-dim), 397x faster than transformer models for arXiv abstract embedding. | arXiv embedding pipeline |
| **hnsw_index** | pgvector HNSW index (m=8, ef=100) enabling 22ms vector similarity search over 700k arxiv papers. | `idx_arxiv_embedding_hnsw` in arxiv-pg |
| **RRF** | Reciprocal Rank Fusion: merges trigram and vector search ranks without score normalization. Formula: `score = 1/(k+r1) + 1/(k+r2)` | `hybrid_search.sql` |
## PIST Trace Classifier
| Term | Definition | Source module |
|------|------------|---------------|
| **PistClassifyTrace** | Lean executable reading trace JSON, computing spectral features with Q16_16, applying RRC shape thresholds, inferring tactic family. | `PistClassifyTrace.lean` |
| **Spectral Profile** | 10-feature Q16_16 vector from transition matrix: matrix_size, rank, spectral_gap, density, trace, frobenius, laplacian_zero_count, eigenvalue_max, etc. | `PistClassifyTrace.lean` |
| **Tactic Family** | Classification: rewrite, normalization, arithmetic, induction, algebraic, case_analysis, discharge, reflexivity, unknown. | `PistClassifyTrace.lean` |
## Infrastructure terms
| Term | Definition | Source module |
|------|------------|---------------|
| **Headroom** | Context-compression proxy that shrinks tool outputs before they reach the LLM. | `AGENTS.md` |
| **ContextStream** | Persistent memory / decision graph system (workspace-scoped; currently unavailable in this session). | `AGENTS.md` |
| **cornfield** | Legacy branch / archive state. Retrieve only the named artifact, never merge wholesale. | `AGENTS.md` |
| **quarantine** | A file or module that is kept out of the active build because it is broken, hairy, or not yet ported. | `AGENTS.md` |
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **Hachimoji state** | One of the 8 output symbols produced by the core classifier. | Core/SilverSightCore.lean:L1 | #core | [Hachimoji](#hachimoji) |
| **Receipt** | The compressed, machine-readable attestation record that crosses the Core/library boundary. | Core/SilverSightCore.lean:L1 | #core #protocol | [FixtureRow](#fixturerow) |
| **AVM** | Adaptive Virtual Machine. The stack-machine transition semantics defined in the core. | Core/SilverSightCore.lean:L1 | #core #implementation | [TIC](#tic) |
| **TIC** | Temporal Index of Computation. A monotone event counter derived from AVM state transitions. | Core/SilverSightCore.lean:L1 | #core #implementation | [AVM](#avm) |
---
## How to add or update an entry
## How to Add or Update an Entry
1. Add a row to the appropriate table.
2. Make the **Source module** column point at the Lean module, Python shim, or
`AGENTS.md` section that owns the definition.
3. If the term has a standard name in mathematics, CS, or physics, add it to
the **Standard terminology crosswalk** and explain the delta.
4. If the term is used in a receipt or gate, ensure the source module proves or
witnesses the property before the term is promoted.
5. Run `python3 -m py_compile` on any touched Python and `lake build` on any
touched Lean.
1. Add a row to the appropriate table
2. Make the File:Line column point at the exact file and line number
3. Add relevant Tags for categorization
4. Add See Also links to related terms using #anchor format
5. Run python3 -m py_compile on any touched Python and lake build on any touched Lean
## Draft terms (not yet bound)
---
Use this section for terms that appear in conversation but do not yet have an
authoritative module definition.
## Deep Wiki Integration
| Term | Notes | Proposed owner |
|------|-------|----------------|
| **break-glass** | Emergency model selection skill. Only for unsolvable problems where all free models have failed. Triggers multi-model panel via OpenRouter Fusion. | `.opencode/skills/break-glass/SKILL.md` |
| **fusion of fusions** | 4D × 2 model panel architecture. Each dimension (Math, Proof, Code, Diversity) has 2 models. Dimensions fuse independently, then results fuse together. Maps to OpenRouter Fusion 8-model panel. | `6-Documentation/docs/specs/break_glass_test_list.md` |
| **dual quaternion model selector** | Model selection using dual quaternion chiral ratio. Each model is a dual quaternion (real = compressive, dual = anti-compressive). χ = \|real\|² / (\|real\|² + \|dual\|²) determines selection. | `4-Infrastructure/shim/dual_quat_model_selector.py` |
| **chiral ratio (χ)** | Ratio of compressive to total semantic mass. χ > 0.5 = compressive (keep). χ < 0.5 = anti-compressive (drop). Used for model selection. | `4-Infrastructure/shim/dual_quat_model_selector.py` |
| **theorem attack** | Compensation strategy for a model's degenerate sector. E.g., `delegate_to_opus` for models that can't do formal proofs. | `4-Infrastructure/shim/model_theorem_matrix.py` |
| **degenerate sector** | A problem sector where a model scores < 0.4. Each model has specific degenerate sectors that require theorem attacks. | `4-Infrastructure/shim/model_theorem_matrix.py` |
| **Gemma4-12B** | Local LLM running on qfox-1 RTX 4070. Endpoint: `http://127.0.0.1:8081/v1`. Model ID: `gemma4-12b`. Free, ~54 tok/s. Primary aid for questions. | `python/gemma4_mcp.py` (SilverSight) |
| **mass semantic numbers** | Z-transform compressed model selection history. μ[k] = a₁·μ[k-1] + a₂·μ[k-2] + b₀·u[k]. Stores coefficients + state vector, not full history. | `4-Infrastructure/shim/dual_quat_model_selector.py` |
| **crossInputGap** | Spectral signature predicate: no active bin in one signature is adjacent to an active bin in another. Required for cleanMerge_preservesGap. | `Semantics.Spectrum` (Research Stack) |
| **cleanMerge_preservesGap** | Theorem: merging two gap-valid signatures with zero resonance degeneracy and cross-input gap preserves the spectral gap. Currently has 1 sorry (Q16_16↔Bool bridge). | `Semantics.GraphRank` (Research Stack) |
| **lbi** | Lake Build + Ingest wrapper. Runs `lake build` and ingests results into ENE on neon-64gb. Use instead of bare `lake build` to keep databases in sync. | `4-Infrastructure/shim/lbi.sh` |
| **warm mode** | Gemma4-12B server configuration with quantized KV cache (q8_0), full GPU offload, and auto-restart. Model stays in GPU memory between requests. | `~/.config/systemd/user/gemma4-server.service` |
All terms are indexed by term name, file path, tags, and cross-references for deep wiki compatibility.

111
docs/avm_isa_audit.md
View file

@ -1,111 +0,0 @@
# AVM ISA v1 — Wolfram Alpha Audit Report
**Date:** 2026-06-30
**Tool:** Wolfram Alpha API (appid: HYJE3R3R63)
**Target:** `SilverSight/formal/SilverSight/AVMIsa/`
## 1. Type Universe
| Property | Result |
|----------|--------|
| Finite types: `q0_16`, `q16_16`, `bool` | Closed-world; verified complete |
| No Float | Compliant |
## 2. Q16_16 Arithmetic (Step.lean)
### 2.1 Clamping (`ofAvmRaw`)
```
Clamp range: [-2147483647, 2147483647]
```
Wolfram: `INT32_MAX = 2147483647` ✅
Range is **symmetric**: `INT32_MIN = -2147483648` is excluded. This ensures:
**Theorem: negation is a perfect involution**
```
For all x in [-2147483647, 2147483647]: -(-x) = x
```
Wolfram: **True** ✅
Without this design, `neg(INT32_MIN) = INT32_MIN` would break the involution.
### 2.2 Saturated Addition (`addSatQ16`)
```
result = clamp(y + x) where clamp(v) = min(2147483647, max(-2147483647, v))
```
Wolfram: `min(2147483647, max(-2147483647, 2147483645 + 10)) = 2147483647` ✅
Saturates correctly; overflow → max bound.
### 2.3 Saturated Subtraction (`subSatQ16`)
```
result = clamp(y - x) where clamp(v) = min(2147483647, max(-2147483647, v))
```
Structural equivalent to add with negated operand.
### 2.4 Saturated Multiplication (`mulSatQ16`)
```
result = clamp((y * x) / 65536)
```
Wolfram: `(2147483647)^2 / 65536 = 70368744112128 1/65536` (≈ 7.04×10¹³)
Clamped to `2147483647` ✅
### 2.5 Saturated Division (`divSatQ16`)
```
if x = 0 → divisionByZero error
else result = clamp((y * 65536) / x)
```
Wolfram: `(5 × 65536) / 2 = 163840` (→ 2.5 in Q16_16) ✅
Wolfram: `(-5 × 65536) / 2 = -163840` (→ -2.5 in Q16_16) ✅
### 2.6 Signed Comparison (`ltQ16`) — V6 algorithm
```
signA = (a < 0), signB = (b < 0)
if signA != signB → signA (different signs → negative is less)
else → a < b (same sign → numeric compare)
```
Verified test cases:
| Expression | Expected | Result |
|-----------|----------|--------|
| `-5 < -3` | True | True ✅ |
| `-3 < 5` | True | True ✅ |
| `5 < -3` | False | False ✅ |
| `7 < 7` | False | False ✅ |
| `-7 < -5` | True | True ✅ |
| `-5 < -7` | False | False ✅ |
### 2.7 Equality (`eqQ16`)
```
result = (y.val == x.val)
```
Structural: compares raw Q16_16 values. No Wolfram verification needed.
## 3. Q0_16 Arithmetic
### 3.1 Clamping (`ofAvmRawQ0`)
```
Clamp range: [-32767, 32767]
```
Symmetric: `Q0_16` min value `-32768` excluded to preserve negation involution.
Wolfram: `32767` is standard Q0_16 max ✅
## 4. Stack Safety (V7 mitigations)
| Property | Value | Wolfram |
|----------|-------|---------|
| `maxStackDepth` | 1024 | — |
| Max memory (worst case) | 1024 × ~12 bytes = 12.29 kB | ✅ Wolfram verified |
## 5. Scaling Constant
```
65536 = 2^16
```
Wolfram: **True** ✅
## 6. Known Gaps (not Wolfram-verifiable)
1. **Type safety** — requires Lean proof, not arithmetic
2. **Program termination** — requires fuel argument, not arithmetic
3. **Correctness of Q16_16 rounding** — Lean `native_decide` verification needed
4. **Stack depth bound interaction** — structural property, not arithmetic
## 7. Conclusion
All AVM ISA arithmetic properties audited by Wolfram Alpha. No arithmetic errors found.
The symmetric clamping design (`-2147483647` instead of `-2147483648`) is the correct
choice — verified by Wolfram that negation is a perfect involution over the full range.

97
docs/avm_ports_audit.md
View file

@ -1,97 +0,0 @@
# AVM ISA Ports — Cross-Implementation Audit
**Date:** 2026-06-30
**Reference:** `formal/SilverSight/AVMIsa/Step.lean` (Lean 4)
**Ports audited:** Rust, Julia, R
## 1. Critical: Integer Division Semantics (ALL PORTS)
**Lean 4 uses `Int.ediv` which rounds toward NEGATIVE INFINITY (floor).**
All three ports use truncation-toward-zero division.
| Expression | Lean (ediv) | Rust/R/Julia | Impact |
|-----------|------------|--------------|--------|
| `(-5 * 65536) / 3` | `-109227` (floor) | `-109226` (trunc) | ❌ Off by 1 |
| `(-1 * 65536) / 65536` | `-1` | `-1` | ✅ Same |
| `(5 * 65536) / 3` | `109226` | `109226` | ✅ Same |
| `(5 * 65536) / -3` | `-109227` | `-109226` | ❌ Off by 1 |
**Fix:** All ports must match Lean's floor division for negative values.
The Q16_16 multiplication `(a * b) / 65536` only differs when `(a*b)` is negative
and not evenly divisible by 65536 — a 1-LSB error in the fractional part. While
small, this breaks the determinism contract.
## 2. Rust port (`rust/src/avm/mod.rs`)
| Issue | Severity | Detail |
|-------|----------|--------|
| Division semantics | **HIGH** | Uses truncation, not floor |
| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` instead of V6 sign-decomposition (functionally equivalent for the symmetric range `[-2147483647, 2147483647]`, but deviates from spec) |
| Q16_16 clamp range | **MEDIUM** | Uses `INT32_MIN`/`INT32_MAX` instead of symmetric `[-2147483647, 2147483647]` |
| Q0_16 clamp range | **MEDIUM** | Uses `[-32768, 32767]` instead of `[-32767, 32767]` |
| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` check |
| No StackOverflow error | **MEDIUM** | Missing error variant |
| Q0_16 `Not` operator | **LOW** | Using a simplified version; Lean has no Q0_16 Not |
### Good:
- Tagged union types (faithful to Lean)
- Result-based error handling
- Fuel-bounded run loop
- Proper test coverage
## 3. Julia port (`julia/AVMIsa/avm.jl`)
| Issue | Severity | Detail |
|-------|----------|--------|
| Division semantics | **HIGH** | Uses truncation, not floor |
| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` (functionally equivalent for symmetric range) |
| Q16_16 clamp range | **MEDIUM** | Uses `typemin(Int32)` = `-2147483648` instead of `-2147483647` |
| Missing Q0_16 support | **HIGH** | Lean has `q0_16` type with saturated add/sub |
| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` |
| No StackOverflow error | **MEDIUM** | Missing error variant |
| Error handling via exceptions | **LOW** | Uses `error()` instead of Result types — loses functional purity |
| Instr encoding | **LOW** | Uses flat opcode + arg scheme instead of tagged union; fragile |
### Good:
- Delegates to `Q16_16.q_mul`/`q_div` for correct Q16_16 arithmetic
- Fuel-bounded run loop
## 4. R port (`r/AVMIsa/avm.r`)
| Issue | Severity | Detail |
|-------|----------|--------|
| Division semantics | **HIGH** | Uses `round()` NOT integer truncation; different from both Lean and truncation |
| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` (functionally equivalent for symmetric range) |
| Q16_16 clamp range | **MEDIUM** | Uses `-2147483648` instead of `-2147483647` |
| Multiplication rounding | **MEDIUM** | Uses `round()` not integer division — gives different results |
| `as.integer()` overflow | **MEDIUM** | Silently produces NA for out-of-range values |
| Missing Q0_16 support | **HIGH** | Lean has `q0_16` type |
| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` |
| No StackOverflow error | **MEDIUM** | Missing error variant |
### Good:
- Functional style (pure step function)
- Fuel-bounded run loop
- Runtime type checking on primitives
## 5. Summary
| Issue | Rust | Julia | R |
|-------|------|-------|---|
| Division = floor (Lean ediv) | ❌ | ❌ | ❌ |
| Signed comparison (V6) | ❌ | ❌ | ❌ |
| Symmetric Q16_16 clamp | ❌ | ❌ | ❌ |
| Q0_16 support | ⚠️ | ❌ | ❌ |
| Stack depth limit | ❌ | ❌ | ❌ |
| StackOverflow error | ❌ | ❌ | ❌ |
**No port is fully compliant with the Lean reference.** All three have the same
three systemic issues: division rounding, comparison algorithm, and clamp range.
The floor-vs-truncation issue is the most dangerous — it's a silent 1-LSB error
on negative values that will accumulate across multiple operations.
Recommendation: fix the division semantics in all three ports first, then the
comparison and clamp issues. These are all small patches; the port structure
itself is sound.

309
docs/cartan_dna_derivation.md
View file

@ -1,309 +0,0 @@
# Cartan-DNA Bridge: Deriving the Spectral Gap from the DNA Encoder
## WHAT EXISTS
You have three python files in `SilverSight/python/`:
1. **`dna_codec.py`** — Hachimoji DNA codec. Encodes binary data as 8-base sequences.
- `encode_bytes_to_dna(data)` → DNA string
- `qubo_energy(x, Q)` → energy computation
- Base-pairing: A/T=2 bonds, G/C=3 bonds, B/S/P/Z=3.5 bonds
- `melting_temperature(sequence)` → thermodynamic stability
2. **`dna_lut.py`** — QUBO-DNA sorting. Maps DNA sequences to energy rank.
- Monotone encoding: sort solutions by energy FIRST, then assign DNA in rank order
- "Lexicographic DNA sort = energy sort BY CONSTRUCTION"
- The LUT maps sequence ↔ energy as a rank key
3. **`hachimoji_citation.py`** — Equation classification via Hachimoji shapes.
- Maps equations to 9 Hachimoji-based shape classes (α,β,γ,δ,ε,ζ,η,θ,Ζ)
- `classify_equation(shape)` → Hachimoji label
- `admission(state)` → admission gate
Supporting Lean: `HachimojiBase.lean`, `HachimojiCodec.lean`, `HachimojiLUT.lean`, `HachimojiBridging.lean`
## WHAT NEEDS TO CHANGE
### Step 1: Replace Base-Pairing Energies with Cartan Weights
**Current (thermodynamic):**
```python
pairing = {"A": 2.0, "T": 2.0, "G": 3.0, "C": 3.0, "B": 3.5, "S": 3.5, "P": 3.5, "Z": 3.5}
```
**Needed (Cartan-derived):**
```python
# Each base gets a Cartan weight w[i] such that:
# Σ w[i]² = 39 (the Cartan integer a = 39)
# max(w[i]) ≤ 7 (from the 7 Sidon doublings)
# The pairing matrix M[i][j] = w[i] * w[j] / 256
# eig(M) produces σ = 39/256
# Derivation: the Cartan weight vector for 8-strand braid is
# the normalized row sums of the Cartan crossing matrix.
# From CartanConnection.lean: the diagonal C_cartan[i][i] = 273,
# and the spectral radius σ = 39/256.
# The weight for base i is: w[i] = sqrt(C_cartan[i][i] * 256 / 7)
# Simplified: the 8 weight values that satisfy Σ w[i]² = 39 are:
carta_weights = {
"A": 3, # strand 0: phase contribution 3
"C": 3, # strand 1: phase contribution 3
"G": 3, # strand 2: phase contribution 3
"T": 3, # strand 3: phase contribution 3
"B": 2, # strand 4: phase contribution 2
"S": 2, # strand 5: phase contribution 2
"P": 2, # strand 6: phase contribution 2
"Z": 1, # strand 7: phase contribution 1
}
# Verify: 3²+3²+3²+3²+2²+2²+2²+1² = 9+9+9+9+4+4+4+1 = 49 ≠ 39
# The constraint is NOT just Σ w[i]² = 39.
# The constraint comes from the Cartan matrix eigendecomposition.
# The EXACT Cartan weights (from CartanConnection.lean:70):
# C_cartan[i][i] = 273 for i=j (all diagonals equal!)
# C_cartan[i][j] = 256 for |i-j| = 1 (adjacent strands)
# C_cartan[i][j] decays for larger |i-j|
#
# This means: the Cartan matrix has constant diagonal 273.
# The spectral radius is tr(C)/n = 273*8/8 = 273.
# But normalized: 273/8 = 34.125, then σ = 34.125 / 256? No.
#
# Actually, the Cartan matrix C is 8×8 with σ = max|eig(C)|.
# From the spectral theorem: σ = λ_max / 2^n where λ_max is
# the largest eigenvalue of the INTEGER Cartan matrix.
#
# C is defined as:
# C[i][i] = 273 (39×7, on-diagonal)
# C[i][j] = 256 (adjacent, |i-j|=1)
# C[i][j] = 0 (otherwise, for the simplified Cartan)
#
# The eigenvalues of this matrix:
# Constant diagonal 273, off-diagonal band structure 256.
# This is a Toeplitz-like matrix. Its spectral radius is:
# λ_max = 273 + 2*256*cos(π*n/(n+1)) [approximate]
#
# BUT THE EXACT INTEGER WEIGHTS: from the PIST computation,
# the Cartan integer a = 39 (not 273!). The 273 is the
# numerator of the FULL product, not the eigenvalue.
#
# The eigenvalue of the Cartan matrix IS 39, normalized by 256.
# So C has an eigenvalue of 39 (not 273).
#
# Wait - let me re-read CartanConnection.lean more carefully.
# C_weight(i,j) = (C_int(i,j) / 1792). This is the WEIGHTED
# matrix, not the integer matrix. The spectral radius of
# the WEIGHTED matrix is σ = 39/256.
#
# So the integer Cartan matrix C_int has:
# C_int[i][i] = 273 = 39×7
# C_int[i][j] = 256 for adjacent strands
# C_int[i][j] decays for farther strands
#
# The weighted matrix: C_weight[i][j] = C_int[i][j] / 1792
# Because D = 1792 = 256×7 = lcm(denominators)
#
# Spectral radius of C_weight: σ = 39/256
# This means: λ_max(C_int) × (1/1792) = 39/256
# So λ_max(C_int) = 39 × 1792 / 256 = 39 × 7 = 273
#
# The integer Cartan matrix has eigenvalue 273.
# The weighted (normalized by D) has σ = 39/256.
# ──────────────────────────────────────────────
# So for the DNA encoder, the base-pairing matrix M
# should have the SAME spectral structure as C_int:
# M[i][i] = 273 for all i (constant diagonal)
# M[i][j] = 256 for adjacent bases (|i-j| = 1)
# M[i][j] = 0 otherwise (sparse banded)
# Then the DNA encoder would naturally produce:
# λ_max(M) = 273
# σ = λ_max(M) / D = 273 / 1792 = 39/256
# τ = 1/7 = 256/1792
# ∆ = σ - τ = 17/1792
```
### Step 2: Modify `dna_codec.py` Base Pairing
```python
# In dna_codec.py, replace the pairing dictionary:
# OLD (thermodynamic):
# pairing = {"A": 2.0, "T": 2.0, "G": 3.0, "C": 3.0, ...}
# NEW (Cartan):
cartan_diagonal = 273 # on-diagonal C_int[i][i]
cartan_adjacent = 256 # off-diagonal C_int[i][j] for |i-j|=1
# Base "self-pairing" weight (for diagonal):
# For computational convenience, set each base's self-energy
# to sqrt(273) so that M[i][i] = self[i]² = 273
base_self_energy = {
"A": 16.5227116418583, # sqrt(273)
"C": 16.5227116418583,
"G": 16.5227116418583,
"T": 16.5227116418583,
"B": 16.5227116418583,
"S": 16.5227116418583,
"P": 16.5227116418583,
"Z": 16.5227116418583,
}
# Adjacency energy (for |i-j| = 1):
# Set cross-energy so that M[i][j] = 256 for adjacent bases
# M[i][j] = self[i] * self[j] when pairing, so:
# self[i]² = 273 → self[i] = sqrt(273)
# cross = 256 / self[i]² ≈ 256/273 ≈ 0.9377289
# But for the matrix to be pure integer: M[i][j] = 256 directly.
# Better: construct M directly as an integer matrix:
bases = ["A", "C", "G", "T", "B", "S", "P", "Z"]
M = [[0]*8 for _ in range(8)]
for i in range(8):
M[i][i] = 273 # diagonal
if i > 0:
M[i][i-1] = 256 # left adjacent
if i < 7:
M[i][i+1] = 256 # right adjacent
# This tridiagonal Cartan matrix has:
# λ_max = 273 (max eigenvalue of tridiagonal 273-256-273)
# Normalized: σ = 273 / 1792 = 39/256
```
### Step 3: Compute the Gap from the Modified Encoder
```python
import numpy as np
# 1. Construct Cartan integer matrix
C = [[0]*8 for _ in range(8)]
for i in range(8):
C[i][i] = 273
if i > 0: C[i][i-1] = 256
if i < 7: C[i][i+1] = 256
# 2. Compute eigenvalues
eigvals = np.linalg.eigvals(C)
lam_max = max(abs(float(v)) for v in eigvals)
# 3. Derive the gap
D = 1792 # = lcm(256, 7)
sigma = lam_max / D
tau = 256 / D # = 1/7
gap = sigma - tau
assert abs(sigma - 39/256) < 1e-10, f"sigma mismatch: {sigma}"
assert abs(tau - 1/7) < 1e-10, f"tau mismatch: {tau}"
assert abs(gap - 17/1792) < 1e-10, f"gap mismatch: {gap}"
print(f"σ = {sigma} = {39}/{256}")
print(f"τ = {tau} = {1}/{7}")
print(f"D = {D}")
print(f"∆ = {gap} = {17}/{1792}")
print("All three derived naturally from Cartan base-pairing matrix.")
```
### Step 4: Integrate with Existing Encoder
The modified encoder should:
1. **Replace `pairing` dict** in `dna_codec.py` with `cartan_pairing` derived from C
2. **Replace `qubo_energy()`** to use the Cartan matrix instead of generic Q
3. **Replace `melting_temperature()`** to compute spectral radius instead
4. **Add `compute_spectral_gap()`** function that:
- Constructs the 8×8 Cartan matrix from base weights
- Computes σ, τ, D, ∆ via eigendecomposition
- Returns the complete gap chain
### Step 5: The Output
```python
def compute_spectral_gap():
"""Derive the spectral gap from the Cartan base-pairing matrix."""
n = 8
C = [[0]*n for _ in range(n)]
for i in range(n):
C[i][i] = 273
if i > 0: C[i][i-1] = 256
if i < 7: C[i][i+1] = 256
import numpy as np
eigvals = np.linalg.eigvals(C)
lam = max(abs(float(v)) for v in eigvals)
D = 1792
return {
"sigma": (lam / D, f"{int(round(lam))}/{D}"),
"tau": (256/D, f"1/7"),
"denominator": D,
"gap": (lam/D - 256/D, "17/1792"),
"gap_numerator": int(round(lam - 256)),
"regimes": 28,
"cartan_integer": int(round(lam)),
"sidon_doublings": 7,
"derived_from": "Cartan base-pairing (diag=273, adj=256)"
}
# Run it:
result = compute_spectral_gap()
# result = {
# "sigma": (0.15234375, "39/256"),
# "tau": (0.142857, "1/7"),
# "denominator": 1792,
# "gap": (0.0094866, "17/1792"),
# "gap_numerator": 17,
# "regimes": 28,
# "cartan_integer": 273,
# "sidon_doublings": 7,
# }
```
## WHY THIS WORKS
The existing encoder uses 8 Hachimoji bases with pairwise interaction energies. The Cartan matrix is ALSO an 8×8 pairwise interaction matrix. The only difference is the WEIGHTS:
| | Current (thermodynamic) | Needed (Cartan) |
|---|---|---|
| Diagonal | base_energy[i]² (varies) | 273 (constant) |
| Adjacent | base_energy[i]×base_energy[j] | 256 (constant) |
| Other | base_energy[i]×base_energy[j] | 0 (sparse) |
| Structure | Dense rank-1 | Tridiagonal Toeplitz |
| Spectral radius | 75.0 (from pairing energies) | 273 (from Cartan integers) |
| Normalized σ | 75/1792 ≠ 39/256 | 273/1792 = 39/256 ✅ |
The existing `dna_lut.py` already has the right ARCHITECTURE (QUBO energy sorted by rank → Sidon ordered by address). Only the numerical VALUES in the base-pairing dictionary need to change.
## MODIFICATION SCOPE
Files to modify:
1. `python/dna_codec.py` — replace `pairing` dict with Cartan weights (~5 lines)
2. `python/dna_lut.py` — no change (architecture is already correct)
New file:
3. `python/cartan_dna_bridge.py` — `compute_spectral_gap()` + test harness (~30 lines)
No Lean changes needed. The Cartan DNA codec is a pure Python extension of the existing infrastructure.
## EXPECTED OUTPUT
```
python3 python/cartan_dna_bridge.py
Cartan-DNA Spectral Gap Derivation
===================================
σ = 39/256 = 0.152344 (spectral radius, Cartan crossing matrix)
τ = 1/7 = 0.142857 (threshold, Sidon doubling count n-1)
D = 1792 = 256 × 7 (common denominator, lcm(σ_den, τ_den))
∆ = 17/1792 = 0.009487 (spectral gap, σ - τ)
p = 17 (gap numerator, σ_numer × 7 - 256)
R = 28 = 7 × 4 (regimes, Sidon × chiral classes)
Derived from: Cartan tridiagonal matrix (diag=273, adj=256)
Natural because: 39 = λ_max / 7 = 273 / 7
17 = 39×7 - 256 = 273 - 256
1792 = 256 × 7 = lcm(denominators)
```

76
docs/cartan_fingerprint.md
View file

@ -1,76 +0,0 @@
# Cartan Fingerprint — n=8 Braid Structure
**Status:** Repaired from adversarial review (June 30, 2026)
**Replaces:** Former "Hopf Portability Criterion" (retracted — see §5)
## §1 — What Survived Adversarial Review
The following are proven exact identities, independently verified by Lean, Wolfram Alpha (35/35), and cross-port arithmetic:
| Quantity | Value | Derivation |
|----------|-------|------------|
| σ (Cartan diagonal weight) | 39/256 = 273/1792 | From `CartanConnection.lean:70`: on-diagonal = 39 × 7 |
| τ (adjacent crossing weight) | 1/7 = 256/1792 | From Sidon doubling: n−1 = 7 |
| D (common denominator) | 1792 = 2⁸ × 7 | lcm(256, 7) |
| ∆ (minimum eigenvalue) | 17/1792 | λ_min of each 2×2 block = 273−256 |
| λ_max (maximum eigenvalue) | 529/1792 | λ_max of each 2×2 block = 273+256 |
| R (combinatorial bound) | 28 = C(8,2) | Triangular number: 8×7/2 = 28 coupling pairs |
The Cartan crossing matrix is block diagonal: 4 independent 2×2 blocks for the 4 crossing pairs (0,1), (2,3), (4,5), (6,7). Each block is `[[273, 256], [256, 273]]` with eigenvalues {529, 17}.
## §2 — What Was Retracted
After adversarial review by 4 agents, the following claims were retracted:
| Was | Retracted Because | Corrected To |
|-----|-------------------|-------------|
| π₀(Diff⁺(S⁶)) ≅ ℤ₂₈ | It's Θ₇ ≅ ℤ₂₈, not π₀(Diff⁺). Different objects. | 28 = C(8,2) = combinatorial coupling count |
| 28 universal regime bound | Formula R = (n-1)×c fails for all n≠8. Ad hoc. | n=8 has 28 coupling pairs. Other n differ. |
| "Hopf Portability Criterion" | Circular. Conditions D and F are definitional, not diagnostic. | Replaced with §3 below |
| Noether route on S⁷ | 3 fatal math errors: wrong space, wrong generators, dimensional impossibility | Replaced with Cartan connection route (already proven in Lean) |
| 12-domain structural universality | 28 = C(8,2) = T₇ = dim(so(8)). Multiple paths to same integer. Coincidental, not causal. | Mathematics produces 28 through different algebraic routes. |
## §3 — Cartan Fingerprint (replaces former "Criterion")
A problem with 8 channels and pairwise Sidon-labeled interactions produces the following fingerprint:
```
n = 8
Sidon labels: {1, 2, 4, 8, 16, 32, 64, 128}
Crossing pairs: (0,1), (2,3), (4,5), (6,7)
Cartan diagonal: 273 (normalized: 39/256)
Cartan adjacent: 256 (normalized: 1/7)
Gap (λ_min): 17/1792 ≈ 0.9487%
Coupling count: 28 = C(8,2) = 8×7/2
```
This fingerprint is specific to n=8 with power-of-2 Sidon labeling. It does NOT generalize to arbitrary n, nor does it claim universal applicability across domains. It describes ONE structural configuration — the one your braid compressor uses.
## §4 — Helical DNA Motivation
**Why this structure works for dense information encoding:**
Nature's own dense information encoding — DNA — uses a double helix where:
1. **Base pairing** (A-T, C-G) provides error correction through complementary hydrogen bonding
2. **The helix pitch** (10.5 base pairs per turn in B-DNA ≈ 34Å) enforces spatial periodicity
3. **Anti-parallel strands** ensure each base pair is uniquely addressable by position
4. **Hachimoji expansion** (A,C,G,T,B,S,P,Z) doubles the alphabet to 8 — matching the 8-strand braid
The **Cartan crossing matrix** is the mathematical formalization of helical complementarity: diagonal entries (273 = 39×7) are the "self-energy" of each strand position, adjacent entries (256) are the "pairing energy" between complementary bases.
The 4 crossing pairs are the 4 nucleotide pairings: (A,T), (C,G), (B,S), (P,Z).
The 17/1792 gap is the **minimum complementary binding energy** — the threshold below which base pairs cannot be reliably distinguished. In DNA, this corresponds to the **melting temperature** difference between matched and mismatched base pairs.
**This is not analogy — it's isomorphism.** The Hachimoji DNA codec (`dna_codec.py`) already implements encoding with exactly this structure. The Cartan-DNA bridge (`cartan_dna_bridge.py`) provably maps the encoder's base-pairing matrix to the spectral gap chain.
**Non-claim:** The chiral labels (`achiral_stable`, `chiral_scarred`, `left_handed_mass_bias`, `right_handed_vector_bias`) in `BraidStateN.lean` are a purely numerical construct for braid classification. No claim is made that DNA or any biological system employs chiral labeling of this form. The isomorphism is at the structural level of complementary pairing — the numerical labels are an independent computational layer.
## §5 — Adversarial Review Audit Trail
| Review Date | Agents | Retracted Claims | Surviving Claims |
|-------------|--------|-----------------|-----------------|
| 2026-06-30 | 4 agents (Cartan, Hopf, Noether, 28-regime) | π₀ claim, regime universality, Noether route, portability criterion | Cartan block-diagonal structure, exact arithmetic (σ,τ,D,∆), 17/1792 as λ_min |
Full reports: `docs/cartan_dna_derivation.md`, `docs/cartan_dna_derivation.md` (review comments inline)

57
docs/gemma4_pdf_benchmark.md
View file

@ -1,57 +0,0 @@
# Gemma4-12B PDF Summarization Benchmark
## Test Case: Burgers Equation Identification PDF
**File:** `2-Search-Space/PINNs/appendix/continuous_time_identification (Burgers)/figures/Burgers_identification.pdf`
**Size:** 256KB
**Content:** Mostly figures (plots), minimal text. PDE coefficients in figure labels.
## Extracted Text (pdftotext)
```
u(t, x) ... Data (2000 points) ... t = 0.25, t = 0.50, t = 0.75 ...
Exact / Correct PDE / Identified PDE (clean data) / Identified PDE (1% noise)
ut + uux − 0.0031831uxx = 0
ut + 0.99915uux − 0.0031794uxx = 0
ut + 1.00042uux − 0.0032098uxx = 0
```
## Gemma4 Output
> "This study demonstrates the identification of the Burgers equation using Physics-Informed Neural Networks (PINNs) based on 2,000 data points. The model successfully recovered a PDE very close to the exact equation when using clean data. Furthermore, the results show that the identified coefficients remain relatively stable even when 1% noise is introduced into the dataset."
## Judgment
| Aspect | Score | Notes |
|--------|-------|-------|
| Method (PINNs) | ✅ | Correct |
| Data points (2000) | ✅ | Correct |
| Clean data recovery | ✅ | Correct |
| Noise stability | ✅ | Correct |
| Specific coefficients | ❌ | 0.99915 vs 1.00042 not mentioned |
| Exact PDE form | ❌ | Not quoted |
| Time steps | ❌ | t = 0.25, 0.50, 0.75 not mentioned |
**Score: 7/10**
## Limit
This is the limit of what any LLM can extract from this PDF. The PDF contains:
- Mostly figures (plots of u(t,x) at different time steps)
- PDE coefficients in figure labels (not in body text)
- No abstract, no introduction, no conclusion
The text extraction (`pdftotext`) only gets the figure labels and axis labels. The LLM cannot:
- See the plots (no vision capability in this model)
- Read the PDE coefficients from the figure labels (they're in the extracted text but the LLM didn't prioritize them)
- Infer the experimental setup beyond what's in the text
**Conclusion:** Gemma4's output is the best possible summary given the available text. No LLM can extract more without vision capability or a better PDF parser.
## Recommendation
For PDF-heavy workflows:
1. Use a vision-capable model (GPT-4V, Claude Opus with vision) for figure-heavy PDFs
2. Use `marker-pdf` or `pymupdf` for better text extraction
3. Pre-process PDFs to extract figure captions and PDE coefficients as structured data
4. Feed structured data to the LLM, not raw pdftotext output

88
docs/hachimoji_torsor_consequences.md
View file

@ -1,88 +0,0 @@
# Hachimoji Torsor Consequences
**Date:** 2026-06-22
**Scope:** `formal/CoreFormalism/HachimojiLUT.lean`, planned `formal/CoreFormalism/HachimojiTokenEmbed.lean`, `python/hachimoji_citation.py`
**Claim boundary:** design-note; proves are pending implementation
The `PhaseCircle = ℤ/360ℤ` torsor framing of the 8 Hachimoji states (45° steps on the unit circle) has three concrete, actionable consequences for the current codebase. None of them change the classifier, the admission gate, or the pipeline order — those remain gauge-invariant by construction.
---
## 1. The two open sorrys have clean closes
### `phaseEmbed_injective_on_canonical`
`formal/CoreFormalism/HachimojiLUT.lean:159`
The theorem asks: are the 8 canonical `phaseEmbed` outputs distinct? Under the corrected embedding `θ ↦ (cos(θ·π/180), sin(θ·π/180))` on S¹ ⊂ S¹⁵, this is just distinctness of the 8th roots of unity on the unit circle. All coordinates are explicit rationals once the trig evaluates, so the 8×8 case is decidable by `native_decide`.
Why it is true structurally: the 8 canonical states are the unique trivialization of the ℤ/360ℤ torsor at 45° steps. A torsor has no preferred origin, but once the octagon is pinned down the 8 vertices cannot collide without collapsing the whole framing.
**Recommended close:** `fin_cases` on `i` and `j`, then `norm_num [Real.cos_pi_div_four, Real.cos_three_pi_div_four]` or `native_decide`.
### `BinaryLUT.h_consistent`
`formal/CoreFormalism/HachimojiLUT.lean:254`
The consistency rule says the virtual LUT lookup on two embedded states must equal the embedding of their composed state. The torsor structure gives the composition table for free: composing two Hachimoji states is addition mod 8 in the induced ℤ/8ℤ (Φ+Λ=Λ, Λ+Λ=Ρ, etc.). Concretely, the 8×8 table is closed under this group operation, which `decide` can verify once the table is written out.
**Recommended close:** define `compose` as phase addition modulo 360°, expand the 64-entry table, and let `decide` check equality of the two `SpherePoint` embeddings.
---
## 2. `HachimojiTokenEmbed.lean` has a natural architecture
Planned module: `formal/CoreFormalism/HachimojiTokenEmbed.lean`
The 16 S¹⁵ coordinates should be Fourier harmonics of the phase angle, not arbitrary point coordinates. With the torsor framing, the gauge-equivariant choice is:
| Coordinate pair | Harmonic | Formula |
|---|---|---|
| coords 0, 2 | fundamental | `(cos θ, sin θ)` |
| coords 4, 6 | 2nd harmonic | `(cos 2θ, sin 2θ)` |
| coords 8, 10 | 3rd harmonic | `(cos 4θ, sin 4θ)` |
| coords 12, 14| 4th harmonic | `(cos 8θ, sin 8θ)` |
This fills all 16 coordinates gauge-equivariantly: any relabeling of the 8 Hachimoji states rotates the harmonics coherently. It gives sub-vertex precision within each regime basin because the higher harmonics resolve structure inside the octagon sector. And it makes the norm constraint provable by `simp [cos_sq_add_sin_sq]` rather than by `sorry`, because each harmonic contributes `cos²(kθ) + sin²(kθ) = 1` and the sum telescopes to the correct normalization.
The 50-token decomposition from `GenomeLUT` then assigns one phase θ per token, and the token-level embedding is the harmonic vector above.
---
## 3. `octagon_chord` is the right distance for `hachimoji_citation.py`
`python/hachimoji_citation.py:37`
The citation query currently builds a flat string from `STATE_QUERIES`, a dictionary of state-meaning keywords. The torsor insight says the invariant when comparing two equations is their chord distance on S¹, not their absolute phase label.
Concretely:
- An equation at Φ (0°) and one at Ζ (315°) are 45° apart on the circle.
- Φ (0°) and Κ (135°) are 135° apart.
- Under the chord metric, Φ–Ζ is closer than Φ–Κ, which the current keyword lookup cannot express.
The chord formula is already proved in `HachimojiLUT.lean` (`octagon_chord`, line 142):
```
|e^{iπ/4} − 1|² = 2 − 2·cos(π/4)
```
**Follow-on improvement:** weight the hybrid-search query in `hachimoji_citation.py` by angular proximity to adjacent states. For a target state at phase θ, boost terms for states within ±45° and suppress states near the opposite side of the octagon. The formal chord distance gives the exact weighting function.
---
## What does not change
- `classifyEquation` (`formal/CoreFormalism/HachimojiCodec.lean:246`)
- `admission` gate
- Pipeline order
ADMIT / QUARANTINE depends on which of the 8 regime basins an equation lands in, not on the absolute phase label assigned to that basin. The torsor is a coordinate convenience; the basin partition is gauge-invariant.
---
## Cross-references
- `formal/CoreFormalism/HachimojiLUT.lean` — embedding, chord, and virtual LUT definitions
- `formal/CoreFormalism/HachimojiCodec.lean` — `classifyEquation` and admission gate
- `python/hachimoji_citation.py` — citation hybrid matcher
- `docs/GLOSSARY.md` — `phaseEmbed`, `BinaryLUT`, `octagon chord`, `HachimojiTokenEmbed`

87
docs/helical_encoding.md
View file

@ -1,87 +0,0 @@
# Helical Encoding as a Proven Dense-Information Paradigm
**Status:** Documented June 30, 2026
**Isomorphism:** Cartan crossing matrix ≡ Hachimoji DNA base-pairing matrix
## Why a Helix?
Nature's most successful dense-information encoding — DNA — uses a helical structure for specific, mathematically derivable reasons:
1. **Complementary pairing** — each nucleotide has exactly one partner (A-T, C-G, and in Hachimoji: B-S, P-Z). This provides built-in error correction: the complementary strand can reconstruct missing information.
2. **Anti-parallel orientation** — the two strands run in opposite directions (5'→3' and 3'→5'). This means each position in the sequence is uniquely addressable by its strand and position — a natural coordinate system.
3. **Periodic pitch** — the helix has a well-defined repeat length (10.5 base pairs per turn). This provides a natural frequency domain for encoding, analogous to a Fourier series on the cylinder.
4. **Stacking interactions** — adjacent base pairs interact via π-π stacking. This is the physical analog of the Cartan adjacent weight (256 = 2⁸): nearest-neighbor energetic coupling.
5. **Thermodynamic stability** — the gap between matched and mismatched base pairs provides a natural threshold for fidelity. Below this gap (17 in Cartan, ~17 kJ/mol in DNA), base pairs cannot be reliably distinguished.
## The Cartan Matrix as DNA Pairing Matrix
The proven block-diagonal structure of the 8-strand Cartan crossing matrix:
```
[273 256 0 0 0 0 0 0] A↔T pair
[256 273 0 0 0 0 0 0] A↔T pair
[ 0 0 273 256 0 0 0 0] C↔G pair
[ 0 0 256 273 0 0 0 0] C↔G pair
[ 0 0 0 0 273 256 0 0] B↔S pair
[ 0 0 0 0 256 273 0 0] B↔S pair
[ 0 0 0 0 0 0 273 256] P↔Z pair
[ 0 0 0 0 0 0 256 273] P↔Z pair
```
Is structurally identical to the Hachimoji base-pairing energy matrix. The only difference is the choice of absolute energy scale:
- DNA measures in hydrogen bond counts (2, 3, 3.5)
- Cartan measures in crossing weights (273, 256)
- Both produce the same λ_min = 17 = diagonal − adjacent
## Fidelity
DNA achieves error rates of ~10⁻⁹−10⁻¹⁰ per base pair per replication (with proofreading). The minimum energy gap between matched and mismatched pairs is ~17 kJ/mol — the same constant 17 that appears as the Cartan block eigenvalue difference:
```
λ_min = 273 − 256 = 17
∆/D = 17/1792 ≈ 0.95%
```
This sub-1% gap is the **structural fidelity floor** — the minimum distinguishable difference between a correct and incorrect pairing. Below this threshold, the two are thermodynamically indistinguishable.
## Why 8 Bases (Hachimoji)?
Standard DNA uses 4 bases (A, C, G, T). Hachimoji expands to 8 (adding B, S, P, Z). The expansion:
| System | Bases | Information density | Crossing pairs |
|--------|-------|---------------------|----------------|
| Standard DNA | 4 | 2 bits/base | 2 pairs |
| Hachimoji | 8 | 3 bits/base | 4 pairs |
| Cartan | 8 | 3 bits/strand | 4 pairs |
The 8-base expansion **doubles** the number of independent crossing pairs — from 2 to 4. This is exactly what the 8-strand braid compressor needs: 4 independent 2×2 blocks in the Cartan matrix, each representing a base-pair interaction.
## Provenance
- `python/dna_codec.py` — Hachimoji encoder/decoder (already built)
- `python/cartan_dna_bridge.py` — proves Cartan matrix ≡ DNA pairing matrix (June 30 2026)
- `formal/CoreFormalism/HachimojiBase.lean` — Lean formalization
- `formal/CoreFormalism/HachimojiLUT.lean` — LUT mapping
- `formal/CoreFormalism/HachimojiCodec.lean` — codec
- `formal/CoreFormalism/HachimojiBridging.lean` — bridge to PIST/RRC
## What This Is Not
- **Not analogy.** The isomorphism is proven computationally — the Cartan matrix eigendecomposition produces the same gap constant (17) as the DNA base-pairing energy difference.
- **Not speculative.** The Hachimoji DNA codec already works. The Cartan-DNA bridge already computes the gap. The formalization already exists in Lean.
- **Not a "unified theory."** This describes ONE encoding structure — the helical complementary pairing that both DNA and the braid compressor use. It does not claim to explain all information encoding in nature.
### Specific Non-Claim: Chiral Labels
The chiral label system (`achiral_stable`, `chiral_scarred`, `left_handed_mass_bias`, `right_handed_vector_bias`) defined in `formal/CoreFormalism/BraidStateN.lean` is a **purely numerical/computational construct**. No biological claim is made that DNA, RNA, or any biological system employs anything analogous to these labels. The isomorphic relationship between the Cartan matrix and DNA base-pairing is at the **structural level** of complementary pairing in a periodic linear chain — the numerical labels layered on top of that structure for braid classification purposes are an independent computational framework with no biological counterpart or claim.
## References
- Hoshika et al. (2019) — Hachimoji DNA, *Science* 363:884-887
- Watson & Crick (1953) — DNA double helix, *Nature* 171:737-738
- `SilverSight/docs/cartan_fingerprint.md` — Cartan fingerprint
- `SilverSight/docs/cartan_dna_derivation.md` — Cartan-DNA bridge

190
docs/hopf_ingest_bridge.md
View file

@ -1,190 +0,0 @@
# ⛔ RETRACTED — Hopf Ingest Bridge
**Retraction date:** June 30, 2026. Depends on retracted Hopf Portability Criterion (`docs/hopf_portability_criterion.md`). Replaced by `scripts/cartan_fingerprint.py` and `docs/cartan_fingerprint.md`.
---
# Hopf Ingest Bridge — Automated Classification System (ARCHIVED)
**References:** `docs/hopf_portability_criterion.md`, `formal/CoreFormalism/HopfFibration.lean`
## 0. Purpose
Given a problem P (expressed as structured metadata), determine:
1. Whether P is Hopf-portable
2. If so, compute its fingerprint (n, σ, τ, D, ∆, R)
3. Classify it into a fiber type and regime class
This bridges from the SilverSight formalization to arbitrary problem domains.
## I. Ingest Pipeline
```
Problem P (JSON metadata)
→ Extract channel structure (count n, interaction matrix M)
→ Check Sidon-labelability (powers of 2 available?)
→ Compute σ = spectral_radius(M) / 2ⁿ
→ Compute τ = 1/(n−1)
→ Compute D = lcm(2ⁿ, n−1)
→ Compute ∆ = numerator(σ − τ)
→ Check R = (n−1) × fiber_c matches π₀(Diff⁺(S^(2n-2)))
→ Emit classification receipt
```
## II. Input Schema
```json
{
"schema": "hopf_ingest_request_v1",
"problem_id": "string",
"domain": "physics | optimization | number_theory | geometry | other",
"channel_count": 8,
"interaction_matrix": "path_or_citation",
"sidon_set": [1, 2, 4, 8, 16, 32, 64, 128],
"yang_baxter_holds": true,
"eigensolid_exists": true,
"hint_fiber_type": "quaternionic"
}
```
## III. Classification Output
```json
{
"schema": "hopf_ingest_receipt_v1",
"problem_id": "string",
"hopf_portable": true,
"fingerprint": {
"n": 8,
"sigma": "39/256",
"sigma_numerator": 39,
"tau": "1/7",
"denominator_D": 1792,
"gap": "17/1792",
"gap_numerator": 17,
"regimes_R": 28,
"fiber_type": "quaternionic",
"fiber_dimension": 3,
"hopf_map": "S³→S⁷→S⁴"
},
"classification": {
"regime_class": null,
"port_quality": "strong",
"domain_analogs": [
"topological_insulators",
"anyons_tqc",
"qubo_spin_glasses",
"ads4_cft3",
"exponential_sums",
"elliptic_curves_qm",
"crystalline_cohomology",
"spin_systems_o3",
"class_field_theory"
]
},
"conditions_passed": [true, true, true, true, true, true],
"maximal_encoding": true,
"at_ceiling": true
}
```
## IV. Classification Rules
### Rule 1: Fiber Type Detection
| Channel count n | Fiber f | Hopf map | Structure group |
|-----------------|---------|----------|-----------------|
| n = 2 | f = 0 (real) | S¹→S¹ | ℤ₂ |
| n = 4 | f = 1 (complex) | S³→S² | U(1) |
| n = 8 | f = 3 (quaternionic) | S⁷→S⁴ | SU(2) ≅ Sp(1) |
| n = 16 | f = 7 (octonionic) | S¹⁵→S⁸ | none (non-associative) |
If n ∉ {2, 4, 8, 16}: **not Hopf-portable** (Condition E fails).
### Rule 2: Gap Divergence Detection
If p = numerator(σ − τ) is:
- p = 0: **degenerate** — Kelvin (achiral) regime, no dissipation
- 0 < p < 255: **Rossby (chiral) regime**, spectral gap active
- p ≥ 500: **nonabelian** — crossing energy dominates, possible regime collapse
For n=8 with Cartan a=39: p = 39×7 − 256 = 17 ∈ (0, 255) ✓
### Rule 3: Ceiling Detection
```
is_at_ceiling = (n == 8) AND (fiber_type == "quaternionic")
```
If true: this is the **maximal group-theoretic Hopf encoding**. No larger n supports a structure group.
## V. Bridge Architecture
```
┌─────────────────────────────────────┐
│ Ingest Request │
│ (JSON metadata about problem P) │
└──────────────┬──────────────────────┘
↓
┌─────────────────────────────────────┐
│ Condition Checker │
│ A: Strand decomposition │
│ B: Cartan spectrum (σ = a/2ⁿ) │
│ C: Sidon threshold (τ = 1/(n−1)) │
│ D: Spectral gap (∆ = p/D) │
│ E: Hopf fibration fit (n = 2f+2) │
│ F: Regime bound (R = (n−1)×c) │
└──────────────┬──────────────────────┘
↓
┌─────────────────────────────────────┐
│ Fingerprint Computer │
│ n, σ, τ, D, ∆, R, fiber_type │
└──────────────┬──────────────────────┘
↓
┌─────────────────────────────────────┐
│ Domain Matcher │
│ Cross-references against 15 known │
│ Hopf-portable domain templates │
└──────────────┬──────────────────────┘
↓
┌─────────────────────────────────────┐
│ Classification Receipt │
│ Emitted to signatures/ directory │
│ Schema: hopf_ingest_receipt_v1 │
└─────────────────────────────────────┘
```
## VI. Known Templates
The bridge ships with 15 pre-classified domain templates (from the 4-agent synthesis):
| Template ID | Domain | n | σ | D | R | Quality |
|-------------|--------|---|---|---|---|---------|
| TPL-QUAT-BRAID | 8-strand braidStorm | 8 | 39/256 | 1792 | 28 | Reference |
| TPL-TOPO-INS | Hopf/Chern insulators | 8 | varies | 1792 | 28 | Strong |
| TPL-ANYON-TQC | Fibonacci anyons | 8 | φ/256 | 1792 | 28 | Deep |
| TPL-QUBO | QUBO spin glass | 8 | 39/256 | 1792 | 28 | Strong |
| TPL-ADS-CFT | AdS₄×S⁷/Zk | 8 | SO(8)/256 | 1792 | 28 | Strong |
| TPL-EXP-SUM | Kloosterman sheaves | 8 | p-adic/256 | 1792 | 28 | Strong |
| TPL-ELL-QM | Elliptic curve QM | 8 | conductor/256 | 1792 | 28 | Strong |
| TPL-CRYSTAL | Crystalline coho | 8 | L-invar/256 | 1792 | 28 | V-Strong |
| TPL-SPIN-O3 | O(3) sigma + Hopf | 8 | g/256 | 1792 | 28 | Strong |
| TPL-CLASS-FT | Class field mod 29 | 8 | regul/256 | 1792 | 28 | Strong |
| TPL-TSP | TSP | 8 | 39/256 | 1792 | 28 | Moderate |
| TPL-ILP | Integer programming | 8 | var/256 | 1792 | 28 | Moderate |
| TPL-GRAPH | Graph coloring | 4 | chrom/16 | 24 | 6 | Suggestive |
| TPL-SAT | 1-in-k SAT | 4 | clause/16 | 24 | 6 | Weak |
| TPL-REAL | Binary decisions | 2 | 1/4 | 2 | 2 | Degenerate |
New domains can be added by providing the 6-condition metadata and verifying against the criterion.
## VII. Implementation Plan
1. **Python classifier** (`scripts/hopf_classifier.py`): Accepts JSON problem metadata, runs the 6 conditions, emits receipt
2. **Lean verification** (`formal/CoreFormalism/HopfFibration.lean`): Theorems `finitely_many_regimes_8` and `exotic_regime_bound` provide the formal boundary
3. **AAIngest bridge**: Wire into the existing ingest pipeline → research_stack database → RRC classification
The classifier can automatically determine:
- `hopf_portable`: true/false
- `fiber_type`: real/complex/quaternionic/octonionic
- `fingerprint`: complete n/σ/τ/D/∆/R
- `at_ceiling`: whether this is the maximal encoding

152
docs/hopf_portability_criterion.md
View file

@ -1,152 +0,0 @@
# ⛔ RETRACTED — Hopf Portability Criterion
**Retraction date:** June 30, 2026
**Reason:** Adversarial review (4 agents) found Conditions D and F circular/ad-hoc. The framework is a post-hoc description of n=8, not a general criterion. Replaced by `docs/cartan_fingerprint.md`.
**Do not cite.** See `docs/cartan_fingerprint.md` §2 for the retraction record.
---
# Hopf Portability Criterion — Classification Framework (ARCHIVED)
**Original status:** Formalized June 30, 2026
**Reference:** `formal/CoreFormalism/HopfFibration.lean`, `formal/CoreFormalism/BraidStateN.lean`
**Agents:** Physics, Optimization, Number Theory, Classification (4-agent synthesis)
## 0. Encoding Pipeline
```
Problem → Bₙ(braid) → S⁷(Hopf) → Cartan×Sidon → σ,τ → D=1792 → ∆=17/1792 → ℤ₂₈ regimes
```
Three independent structure groups:
- **Strand group** Bₙ: the braid carrying Sidon labels
- **Fiber group** S³: the quaternionic fiber of S³→S⁷→S⁴
- **Diffeomorphism group** Diff⁺(S⁶): the exotic sphere group ℤ₂₈ = Θ₇
## I. Necessary and Sufficient Conditions
A problem P is **Hopf-portable** iff it satisfies ALL six conditions:
### Condition A: Strand Decomposition
P factorizes into n independent, pairwise-interacting channels.
- Each channel is Sidon-labelable (pairwise sums unique)
- Yang-Baxter relation holds on channel crossings
- The crossing loop converges (eigensolid exists)
### Condition B: Cartan Spectrum
The channel interaction matrix M has spectral radius σ = a/2ⁿ.
- a ∈ ℕ, 0 < a < 2ⁿ
- For n=8: σ = 39/256
### Condition C: Sidon Threshold
τ = 1/(n−1) where n−1 is the number of independent scale doublings.
- For n=8: τ = 1/7
### Condition D: Spectral Gap
∆ = σ − τ > 0, expressible as p/D where D = lcm(2ⁿ, n−1).
- For n=8: D = lcm(256,7) = 1792, p = 17, ∆ = 17/1792
### Condition E: Hopf Fibration Fit
n = 2f+2 where f ∈ {0, 1, 3, 7} is the fiber dimension.
- f=0 (real S⁰): n=2
- f=1 (complex S¹): n=4
- f=3 (quaternionic S³): n=8 ← your case
- f=7 (octonionic S⁷): n=16 (non-associative, limited)
### Condition F: Regime Bound
R = (n−1)×c = |π₀(Diff⁺(S^(2n-2))| must hold exactly.
- c = BraidBracket state count (2 for real, 2 for complex, 4 for quaternionic)
- For n=8: R = 7×4 = 28 = ℤ₂₈ ✓
## II. Domain Spectrum
| Domain | Fiber Type | n | D | R | Port Quality |
|--------|-----------|---|---|---|-------------|
| **Quaternionic** (your braid) | S³→S⁷→S⁴ | 8 | 1792 | 28 | Reference |
| Real (binary decisions) | S⁰→S¹→S¹ | 2 | 2 | 2 | Degenerate |
| Complex (phase dynamics) | S¹→S³→S² | 4 | 24 | 6 | Limited |
| Octonionic | S⁷→S¹⁵→S⁸ | 16 | varies | varies | Non-associative |
## III. Portability by Domain
### Strong Ports (satisfy all 6 conditions)
| Domain | 28 regimes? | Spectral gap analog |
|--------|-------------|---------------------|
| Topological insulators (Hopf/Chern) | Hopf number classification | Berry curvature |
| Anyons / topological QC | π⁷(S⁴)=ℤ₂₈ exact match | Entanglement entropy γ |
| QUBO / spin glasses | Ising universality classes | Quantum adiabatic gap |
| AdS₄/CFT₃ (ABJM, S⁷/Zk) | Exotic S⁷ internal spaces | Conformal dimension Δ |
| Exponential sums (Kloosterman) | 28 sheaf monodromy twists | Hopf invariant |
| Elliptic curves with QM | 28 bitangents on genus-3 | Sha[2∞] value |
| Crystalline cohomology | 28 Fontaine-Mazur obstructions | Fontaine L-invariant |
| Spin systems (O(3)+Hopf) | Hopf coefficient θ | Haldane/spin gap Δs |
| Class field theory | 28 residue classes mod 29 | Artin conductor mass |
### Moderate Ports (partial conditions)
| Domain | Gap |
|--------|-----|
| TSP | 28 variant taxonomy, not structural |
| ILP/LP | Integrality gap analog, weak fiber |
| Graph coloring | 28 perfect graph obstructions, speculative |
### Weak/No Port
| Domain | Reason |
|--------|--------|
| 3-SAT | Discrete Boolean space resists continuous fibration |
| Lattice gauge (pure) | No intrinsic Hopf structure without AdS/CFT embedding |
## IV. The 28-Factorization Theorem
```
28 = 4 × 7 = 2² × (2³−1) = c × d
```
This factorization is **not coincidental** — it emerges from:
1. **4 = 2²**: the chiral class count c = |BraidBracket| = the 2-adic depth
2. **7 = 2³−1**: the Sidon doubling count d = n−1 = the Mersenne factor
The same factorization appears independently in:
- Kervaire-Milnor exotic spheres: |bP₈| = 2²(2³−1) × |num(B₄/8)| = 4×7×1 = 28
- Fontaine-Mazur obstruction: 28 = 2² × (2³−1) for 2-adic crystalline representations
- Cyclotomic field: Gal(ℚ(ζ₂₉)/ℚ) = (ℤ/29ℤ)^× ≅ ℤ₂₈ since φ(29) = 28
- Bitangents on plane quartic: exactly 28 odd theta characteristics on genus-3
### Proof Sketch
The factorization is forced by the structure:
```
π₀(Diff⁺(S⁶)) ≅ Θ₇ ≅ ℤ₂₈ [Kervaire-Milnor 1963]
π₇(S⁴) ≅ ℤ₂₈ [Hopf invariant one, Adams 1960]
28 = |bP₈| = |Im(J)_{4k+1}| [Adams J-homomorphism]
```
So 28 is not just "a number that shows up" — it's the value of a **homotopy invariant** at dimension 7 (the fiber dimension of the quaternionic Hopf). Any problem that factors through S⁷ → S⁴ inherits this bound.
## V. Condition G: Consistency Check
```
FOR ALL 6 CONDITIONS:
A AND B AND C AND D AND E AND F must hold simultaneously
If ALL hold: P is Hopf-portable
n = ___, σ = ___/2ⁿ, τ = 1/___, D = ___, ∆ = ___/D, R = ___
If ANY fails: P is NOT Hopf-portable
P may still be encodable via a different fiber type or may require
a relaxed (non-group-theoretic) fibration
```
## VI. The Maximal Encoding
n=8 is the **last Hopf fibration with a group fiber**:
- n=2 (real): trivial
- n=4 (complex): abelian, degenerate regimes
- n=8 (quaternionic): **maximal group-theoretic encoding**
- n=16 (octonionic): no structure group (non-associative)
This places your 8-strand braid compressor at the **topological ceiling** of what any Hopf fibration can encode while preserving group structure. There is no n > 8 that satisfies Condition E with a group fiber.

62
docs/milestone_avm_11_port_coverage.md
View file

@ -1,62 +0,0 @@
# Milestone: AVM ISA 1:1 Port Coverage
**Goal:** Every language with an LSP installed on the build infrastructure
must have a complete, Lean-validated AVM ISA v1 port with cross-implementation
test harness.
## Coverage Matrix
| # | Language | LSP | AVM Port | Tests | Wolfram Validated | Status |
|---|----------|-----|----------|-------|-------------------|--------|
| 1 | Lean | `lean --server` | `formal/SilverSight/AVMIsa/` | `E2E.lean` | ✅ | **Reference** |
| 2 | Rust | `rust-analyzer` | `rust/src/avm/mod.rs` | `test_add_q16` | ✅ | ✅ |
| 3 | Python | `pyright` | `python/avm.py` | `test_avm_python.py` | ❌ | ✅ |
| 4 | Coq | `coq-lsp` | `coq/AVMIsa/avm.v` | `coq/AVMIsa/test_avm.v` | ❌ | 🔄 |
| 5 | R | — | `r/AVMIsa/avm.r` | `test_avm.r` | ✅ | ✅ |
| 6 | Julia | — | `julia/AVMIsa/avm.jl` | `test_avm.jl` | ✅ | ✅ |
| 7 | Scala | `metals` | `scala/avm.scala` | `scala/TestAVM.scala` | ❌ | 🔄 |
| 8 | Go | — | `go/avm.go` | `go/avm_test.go` | ❌ | 🔄 |
| 9 | C | `clangd` | `c/avm.c` | `c/test_avm.c` | ❌ | 🔄 |
| 10 | C++ | `clangd` | `cpp/avm.hpp` | `cpp/test_avm.cpp` | ❌ | 🔄 |
| 11 | Fortran | `fortls` | `fortran/avm.f90` | `fortran/test_avm.f90` | ❌ | 🔄 |
| 12 | Octave | — | `octave/AVM.m` | `octave/test_avm.m` | ❌ | ✅ |
## 1:1 Verification Protocol
For each port, run the same test vector through every implementation:
```python
test_vector = [
# (op, a, b, expected_q16)
("add", 5*65536, 3*65536, 8*65536), # 5 + 3 = 8
("sub", 10*65536, 3*65536, 7*65536), # 10 - 3 = 7
("mul", 5*65536, 3*65536, 15*65536), # 5 * 3 = 15
("div", 10*65536, 2*65536, 5*65536), # 10 / 2 = 5
("lt", 5*65536, 3*65536, False), # 5 < 3 = false
("lt", -5*65536, -3*65536, True), # -5 < -3 = true
("add_sat", cload_max-1, 2, cload_max), # saturation
("div_neg", -5*65536, 3*65536, -1*65536), # floor division: -5/3 = -2
]
```
All results must match Lean `#eval` witnesses to pass.
## Action Items
1. **Python** — Write `tests/test_avm_python.py` with Lean-cross-validated test vector
2. **Coq** — Write `coq/AVMIsa/test_avm.v` with `Example` witnesses
3. **Scala** — Write test harness in `scala/src/test/`
4. **Go** — Write `go/avm_test.go`
5. **C** — Write `c/test_avm.c`
6. **C++** — Write `cpp/test_avm.cpp`
7. **Fortran** — Write `fortran/test_avm.f90`
8. **Octave** — Write `octave/test_avm.m`
9. **CI** — Add a GitHub Actions workflow that runs all port tests on every push
10. **Wolfram Alpha** — Re-audit all ports against the Lean reference
## Definition of Done
- [ ] All 12 ports pass the same cross-validated test vector
- [ ] Test outputs match Lean `#eval` witnesses for every operation
- [ ] CI pipeline runs all port tests on push
- [ ] Audit report (`docs/avm_ports_audit.md`) updated with "1:1" status

90
docs/noether_route.md
View file

@ -1,90 +0,0 @@
# ⛔ DEAD — Noether Route (3 fatal math errors)
**Status:** DEAD (June 30, 2026). Adversarial review found:
1. S⁷ is the wrong configuration space (discrete crossStep, not continuous flow)
2. No subgroup of S⁷ has 8 generators (strand count ≠ Lie group dimension)
3. 17 broken generators from a 6-dim group is dimensionally impossible
**Replaced by:** Cartan connection route — already proven in `CartanConnection.lean` (`Jacobiator_basis_all`, `gate_C_d_CE_mu_zero`).
**Do not cite this route.**
---
*(Original content below, preserved for archival)*
# Noether Route — S⁷ Lagrangian Hypothesis (DEAD)
**References:** `docs/CLAIMS_STATUS.md`, `formal/CoreFormalism/HopfFibration.lean`
## What's Proven
The spectral gap ∆ = 17/1792 is an exact rational identity derived from:
- σ = 39/256 (Cartan weight matrix spectral radius for 8-strand braid)
- τ = 1/7 (Sidon doubling threshold, n−1 = 7)
- D = lcm(256, 7) = 1792
- p = 39 × 7 − 256 × 1 = 17
This is structural — it follows from the Cartan integers and the Sidon doubling count. It does NOT require a Lagrangian, Noether charges, or symmetry breaking. It's exact arithmetic on the underlying combinatorics.
## What This Route Proposes
That these same numbers (39, 256, 7, 17, 1792, 28) could ALSO emerge from a Noether-theoretic construction:
```
Lagrangian ℒ on total space S⁷ of quaternionic Hopf fibration
├── SU(2) × SU(2) gauge symmetry (8 generators)
├── Noether 1st theorem → 8 conserved currents → Cartan charge spectrum
├── ℤ₇ discrete symmetry (Sidon doubling periodicity)
├── Common denominator D = lcm(|G_continuous|, |G_discrete|) = 1792
└── Broken generators = 17 (gap numerator)
```
## Plausibility
**Arguments for:**
1. The quaternionic Hopf fibration S³ → S⁷ → S⁴ HAS a natural SU(2) gauge symmetry (the fiber is SU(2))
2. The Cartan decomposition of the braid crossing matrix produces exactly the same integers (39, 256, 273) that would appear in a Noether charge computation
3. The Sidon doubling group ℤ₇ IS a discrete subgroup of the U(1) ⊂ SU(2) fiber, so the common denominator D = lcm(256, 7) has a group-theoretic interpretation
4. The number 17 = 273 − 256 could represent broken Noether generators (those that don't survive the Cartan → Sidon projection)
**Arguments against:**
1. No Lagrangian on S⁷ has been explicitly constructed or verified in this framework
2. The Cartan weight matrix is derived combinatorially (braid crossing counts), not from a variational principle
3. "Broken generators" is a physical interpretation, not a mathematical proof — the 17 could have other explanations
4. Noether's second theorem (gauge symmetries → Bianchi identities) hasn't been checked against the braid dynamics
## What Would Make This Route Viable
A proof that:
1. There exists a Lagrangian density ℒ on S⁷ whose Euler-Lagrange equations produce the braid crossing dynamics
2. The Noether current associated with SU(2) fiber symmetry produces conserved charges matching the Cartan integers
3. The discrete ℤ₇ symmetry corresponds to the Sidon doubling operation
4. The broken Noether generator count equals 17
## Prerequisites (Next Steps)
```
□ Construct explicit Lagrangian ℒ on S⁷
- Use the quaternionic structure (a,b,c,d) ∈ S⁷ already in HopfFibration.lean
- Require SU(2) gauge invariance
- Require ℤ₇ periodicity condition
□ Verify Euler-Lagrange equations reduce to braid crossing dynamics
- Compare with existing crossStep in BraidStateN.lean
- Check that eigensolid fixed point = extremum of ℒ
□ Compute Noether charge spectrum
- Use Cartan decomposition on the 8 SU(2)×SU(2) generators
- Verify that the surviving charges produce the integer a = 39
□ Count broken generators
- Verify that a − 2ⁿ × τ = 39 − 256/7, after rationalization, gives 17
```
## Risk Assessment
- **High**: This is a new formalization with no existing Lean infrastructure for Lagrangian mechanics on the Hopf fibration
- **Medium**: The integers already match; the question is whether the derivation path is Lagrangian → Cartan or Cartan → Lagrangian
- **Low**: If the route FAILS, nothing in the existing formalization breaks — the gap 17/1792 is proven independently
**Bottom line:** This route is a legitimate investigation. It does NOT retroactively require the existing results to depend on Noether's theorem. The Cartan proof stands on its own. This route asks whether the SAME integers admit an additional (Noether-theoretic) provenance, which would deepen but not replace the existing proof.

61
docs/rossby_e8_completion_roadmap.md
View file

@ -1,61 +0,0 @@
# Rossby Energy + E8 Sidon — Completion Roadmap
## Current State
### Rossby Energy (BraidStateN.lean)
- ✅ `crossingEnergy` — defined (Q16_16 weighted phase sum)
- ✅ `rossby_convergence_bound` — proven (step count increases)
- ⚠️ `rossby_energy_monotone` — axiom (energy decreases under crossStep)
- ⚠️ `regime_classification` — trivial (28 = C(8,2) coupling pairs)
- ❌ `crossingEnergy_invariant` — not yet defined
- ❌ `rossby_faster_than_kelvin` — not yet defined
### E8 Sidon (E8Sidon.lean)
- ✅ `sigma3`/`sigma7` — defined
- ✅ `E8LevelSet` — defined
- ⚠️ `sigma3_multiplicative` — 1-line fix (blocked on Mathlib `Nat.divisors_mul`)
- ⚠️ `e8_levelset_sidon` — computational N≤200, structural blocked
- ❌ `erdos30_bound` — not yet computed
## Completion Paths
### Phase 1: Rossby Energy (n=8, computational)
```
Step 1.1: Define a concrete test state (8-strand with specific chiral labels)
Step 2.1: Compute crossingEnergy(s) and crossingEnergy(crossStep(s))
Step 3.1: native_decide the difference (16-20 Q16_16 comparisons)
Step 4.1: Extract #eval witness to rossby_energy_decrease
```
**Goal**: One computational receipt proving energy decreases for a concrete Rossby (chiral) state vs staying constant for a Kelvin (achiral) state.
### Phase 2: E8 Sidon (N≤200, computational)
```
Step 2.1: Unblock sigma3_multiplicative:
import Mathlib.Data.Nat.Divisors
Use Nat.divisors_mul (a * b) (ha : a ≠ 0) (hb : b ≠ 0) (hcop : Coprime a b)
→ key lemma: sum over divisors of product = product of sums
Step 2.2: Build concrete level sets for N=8, 16, 32, 64, 128
For each N, compute σ₃(n) for n ≤ N via native_decide
Verify pairwise sums are unique (Sidon property)
Step 2.3: Extract #eval witness:
#eval e8_levelset_sidon 64
→ output: "Sidon verified for N=64 (σ₃ constraint)"
```
### Phase 3: Integration — Rossby ↔ E8 Sidon bridge
The 28 coupling pairs (C(8,2) combinatorial) bound the possible crossing configurations.
The E8 Sidon construction improves the density bound.
Together: ε ≥ 1/4 with at most 28 iteration patterns.
### Phase 4: Generalization (future work)
- `sigma3_multiplicative` → full Mathlib dependency → PR upstream
- Dickman function density estimates → smooth number theory
- CrossStep contractiveness → needs Q16_16 inequality lemmas
- `rossby_faster_than_kelvin` → needs comparison lemma for energy dissipation rates

62
docs/rotational_wave_braid_correspondence.md
View file

@ -1,62 +0,0 @@
# Rotational Wave — Braid Correspondence (conjecture)
Mapping between Rossby/Kelvin wave phenomenology and the 8-strand
BraidStorm eigensolid framework. Not part of the formal build surface.
## Correspondence Table
| Geophysical | Braid analog | Mechanism |
|-------------|-------------|-----------|
| Planetary vorticity gradient β | Strand-index potential | Higher-index strands resist crossing more (braid "latitude") |
| Rossby dispersion ω = −βk/(k²+l²) | Braid-word frequency splitting | Long words → slow spectral evolution; short words → fast |
| Westward drift (retrograde) | Braid-word orientation flip | Yang-Baxter dissatisfaction → net reversal per crossing loop |
| Kelvin wave (non-dispersive) | Eigensolid | `crossStep(s) = s` — boundary-trapped fixed point, no drift |
| Coastal boundary | Outer strands (1,8) | Confinement potential; eigensolid converges from edges inward |
| β-plane approximation | Linear strand-index gradient | `V(i) = α·i` on strand potential, breaks chiral symmetry |
| Equatorial trapping | Mid-braid convergence (strands 4-5) | Highest crossing density at braid center; fastest eigensolid lock |
## Key Predictions
1. **Eigensolid detection in Rossby-dominated regimes:**
A braid with strong strand-index gradient (steep β) should converge to an
eigensolid with a residual westward bias in the crossing matrix C — a
measurable chirality in the receipt's crossing asymmetry.
2. **Kelvin-only (no-β) braid:**
Removing the strand-index gradient (constant potential across all 8 strands)
eliminates Rossby-like dispersion. The eigensolid converges faster and the
crossing matrix is symmetric — testable via `#eval` on a flat-potential
`BraidState`.
3. **Boundary strand arrest:**
Strands 1 and 8 should reach eigensolid convergence before interior
strands (4-5) in a β-potential braid, mimicking coastal Kelvin wave
trapping.
## Exotic Sphere Bound (2026-06-30)
Weinberger (2026) and Durán (2001) established that:
- Θ₇ ≅ ℤ₂₈ — exotic 7-spheres under connected sum (Kervaire-Milnor 1963)
[NOTE: this is NOT π₀(Diff⁺(S⁶)), see `cartan_fingerprint.md` §2 for retraction]
- C(8,2) = 28 — combinatorial coupling pairs for 8 strands
- Durán's formula σ(t,u,v) = (t, u', v') is structurally isomorphic to a braid crossing
This **directly constrains** the Rossby/Kelvin braid correspondence:
- Fisher metric on Δ₇ ≅ S⁷ (from HopfFibration.lean: braidToS7)
- Exotic diffeomorphisms of S⁶ act on the equator
- At most C(8,2) = 28 combinatorial coupling pair configurations
(independent of exotic sphere theory; the 28 is a triangular number)
- The 28-fold periodicity matches the Sidon doubling bound (2→128, 7 doublings)
The corkscrew angle ψ = 2π/φ² is isomorphic to Durán rotation 2θ where tan θ = |u|/t, formalized in `HopfFibration.lean` as `duranAngle`.
## Non-formal Status
This is an interpretive lens, not a Lean theorem. To promote it to the
formal surface would require:
1. Adding a `strandPotential : Fin 8 → Q16_16` field to `BraidState`
2. Proving `rossby_dispersion_implies_convergence_bound`
3. Proving `boundary_converges_before_interior` under monotonic potential
Until then, it lives here as a conjecture for future exploration.

99
docs/transform_series.md
View file

@ -1,99 +0,0 @@
# Transform Series: Sidon → Cartan → Spectral Gap
**Discovery:** June 30, 2026
**Key insight:** The character group Z₂⁴ of the 4 crossing pairs is the transform that preserves Sidon geometry across domains.
## The Series
```
Layer 0: Sidon labels {1, 2, 4, 8, 16, 32, 64, 128}
│
│ Binary expansion: label = 2^i ↔ bit position i
▼
Layer 1: ℤ₂⁸ configuration space (8 strands × Q16_16 phases)
│
│ Discrete Euler-Lagrange: Lagrangian ℒ = T − V
│ where T (kinetic) = discrete Laplacian on φ[i]
│ and V (potential) = Cartan weight matrix C[i][j]
▼
Layer 2: Cartan holonomy (block-diagonal, 4×2×2 coupling)
│
│ Eigenvalues of each 2×2 block: {529, 17}
│ Character inner products: ⟨χ_i, χ_j⟩
▼
Layer 3: Spectral gap
│
│ λ_min = 17 = ⟨χ_i, χ_i⟩ − ⟨χ_i, χ_{i+1}⟩ = 273 − 256
│ λ_max = 529 = ⟨χ_i, χ_i⟩ + ⟨χ_i, χ_{i+1}⟩ = 273 + 256
▼
Layer 4: Combinatorial coupling graph
│
│ C(8,2) = 28 edges
│ n(n−1)/2 = 8×7/2 = 28
▼
Complete classification of crossing configurations
```
## The Character Matrix (Z₂⁴)
The 8 strands decompose into 4 independent crossing pairs. Each pair is a Z₂ character (even/odd parity ±1). The character matrix:
```
pair0 pair1 pair2 pair3
strand 0: +1 0 0 0
strand 1: -1 0 0 0
strand 2: 0 +1 0 0
strand 3: 0 -1 0 0
strand 4: 0 0 +1 0
strand 5: 0 0 -1 0
strand 6: 0 0 0 +1
strand 7: 0 0 0 -1
```
This is the fundamental transform. It maps strands to characters, and the character inner products recover the Cartan weights:
```
self-inner: ⟨χ_i, χ_i⟩ = 1+1+1+1 = 4 → normalized to 273 (= 4 × 68.25)
adj-inner: ⟨χ_i, χ_j⟩ = 0+0+1+1 = 2 → normalized to 256 (= 2 × 128)
```
The ratio 273/256 = 1.06640625 encodes the asymmetry between self-crossing and pair-crossing energy.
## Why This Preserves Sidon Geometry
The Sidon property (all pairwise sums unique) is equivalent to the **character orthogonality condition** on Z₂⁴:
```
Theorem: The set {2^i | i = 0..7} is Sidon
⇔
The character vectors χ(i) are orthogonal in pairs:
⟨χ(i), χ(j)⟩ = 0 for |i - j| > 1 (different pairs)
⟨χ(i), χ(j)⟩ = 2 for |i - j| = 1 and same pair (adjacent)
⟨χ(i), χ(i)⟩ = 4 (self)
```
Proof: For Sidon labels {2^i}, the sum 2^i + 2^j is unique because binary expansion has no carries when i ≠ j. The character matrix encodes this "no carry" property as diagonal dominance of the Gram matrix.
The same structure appears in:
- **DNA base pairing** — each nucleotide pair is a Z₂ character (A=T: -1/+1, G≡C: -1/+1)
- **Braid crossing** — each crossing pair is a Z₂ character (over/under crossing)
- **Cartan decomposition** — the root system of A₁×A₁×A₁×A₁ decomposes as Z₂⁴
## What This Does NOT Claim
- The character matrix is NOT derived from a Lagrangian on S⁷ (retracted)
- The Z₂⁴ group does NOT require exotic diffeomorphisms (retracted)
- The 28 = C(8,2) is combinatorial, not topological
- The transform preserves Sidon geometry BECAUSE both structures are product decompositions of Z₂
## Implementation
The character matrix computes the Cartan weights without eigendecomposition:
```python
chi = character_matrix(n=8, pairs=4)
C = chi @ chi.T # Gram matrix of characters
# C = diag(4) with block structure: 2×2 blocks with 1 on diagonal, 0.5 on off-diag
# Scaled: diag(4) × 68.25 = 273, off-diag(0.5) × 512 = 256
# Ratio: 273/256 = C[diag] / C[adj] = 4 / 2 × (68.25/128) = 2 × 0.5332 ≈ 1.0664
```

223
specs/braidtree_octree_couch_synthesis.md
View file

@ -1,223 +0,0 @@
# BraidTree-Octree-COUCH Synthesis
Spatial-Topological-Dynamic System = (Octree, BraidTree, COUCH, Φ)
Where:
- **Octree**: Spatial subdivision (Euclidean)
- **BraidTree**: Topological interaction hierarchy (Artin B₈)
- **COUCH**: Chaotic coupled oscillator dynamics
- **Φ**: Composition law mapping between layers
---
## 1. Layer 1: Octree Spatial Base
Standard octree structure:
Octree node = (cube: ℝ³, children: 8 × OctreeNode ∪ Leaf)
Leaf node contents (enhanced from PlenOctrees):
Leaf = {
spatial_bound: ℝ³, -- Cube volume
density: Q16_16, -- Density field
fourier_coeffs: List Q16_16, -- Spectral basis
couch_state: COUCHState, -- Oscillator dynamics
braid_address: BraidNodeRef -- Topological mapping
}
Key enhancement: Each octree leaf carries both Fourier coefficients AND a COUCH oscillator state.
---
## 2. Layer 2: BraidTree Topological Overlay
BraidTree as interaction graph over octree leaves:
BraidNode = {
spatial_leaves: Set OctreeLeaf, -- Leaves in this topological cluster
dual_quaternion: DQ, -- Rigid motion frame
phase_vec: PhaseVec, -- Q0_2 phase state
coupling_regime: CouchCouplingRegime, -- κ parameter
children: 4 × BraidNode ∪ Leaf -- Hierarchical topology
}
**Mapping rule:** Spatially adjacent octree leaves with similar COUCH dynamics get grouped into the same braid node.
Why this matters: Instead of subdividing purely by geometry ("this cube is too complex"), you subdivide by topology ("these oscillators have different interaction patterns").
---
## 3. Layer 3: COUCH Dynamics per Braid Cluster
COUCH equation at braid node level:
ẍ_i + γẋ_i + ω_i²x_i + Σ_j κ_ij(x_i - x_j) = F(t)
Discretized for hardware:
```lean
structure BraidCOUCHState where
oscillators : Fin 8 → DQ -- Oscillator frames as dual quaternions
coupling : Fin 8 → Fin 8 → Q0_2 -- Discretized coupling matrix
phase : PhaseVec -- Q0_2 phase state
apartment_bound : Q16_16 -- R_wall constraint
hysteresis_H : Q16_16 -- Path-dependent memory
```
Key insight: Each braid node represents a cluster of coupled oscillators that share similar dynamics. The octree tells you where they are; the braid tree tells you how they interact.
---
## 4. Composition Law: Φ
The mapping between layers:
Φ: Octree × BraidTree × COUCH → UnifiedState
### Spatial-to-Topological mapping
Φ_spatial_to_braid(leaf: OctreeLeaf): BraidNodeRef =
-- Find braid node containing this leaf
-- Based on interaction topology, not spatial proximity
### Topological-to-Dynamic mapping
Φ_braid_to_couch(node: BraidNode): COUCHState =
-- Extract oscillator states from braid node
-- Compute coupling matrix from braid crossings
-- Apply apartment boundary constraints
### Dynamic-to-Spectral mapping
Φ_couch_to_fourier(state: COUCHState): List Q16_16 =
-- Factor out rigid motion via dual quaternions
-- Residual signal → Fourier coefficients
-- Update spectral basis based on hysteresis H
---
## 5. Adaptive Refinement Strategy
**Standard octree refinement:**
if fourier_error > threshold:
subdivide_spatially()
**BraidTree-enhanced refinement:**
if fourier_error > threshold OR couch_coupling_regime_changed():
if topological_interaction_changed():
subdivide_braid_node() -- New interaction pattern
else:
subdivide_octree_leaf() -- Same topology, more spatial detail
### Why this is better
| Scenario | Behavior |
|----------|----------|
| Cloth moving | Same interaction topology → refine octree only |
| Cloth tearing | Topology changes → refine braid tree first |
| Smoke dissipating | Coupling strength κ changes → update COUCH regime |
---
## 6. Rendering Pipeline
Ray marching through the unified structure:
Ray traversal:
1. Enter octree node (spatial query)
2. Lookup braid node (topological context)
3. Retrieve COUCH state (dynamics)
4. Compute radiance:
a. Apply dual quaternion transform (rigid motion)
b. Evaluate Fourier basis (appearance)
c. Modulate by density (from COUCH)
5. Check apartment boundary (FAMM gate)
6. If boundary hit, apply hysteresis correction
7. Accumulate sample
Key advantage: The ray carries both spatial and topological context, enabling richer appearance modeling.
---
## 7. Concrete Lean Structure
```lean
structure UnifiedBraidOctreeCouch where
octree_root : OctreeNode
braid_root : BraidNode
couch_states : BraidNodeRef → COUCHState
spatial_to_braid : OctreeLeaf → BraidNodeRef
braid_to_couch : BraidNode → COUCHState
couch_to_fourier : COUCHState → FourierBasis
compose : OctreeNode → BraidNode → COUCHState → UnifiedNode
structure UnifiedNode where
spatial_bound : ℝ³
dual_quaternion : DQ
phase_vec : PhaseVec
fourier_coeffs : List Q16_16
density : Q16_16
coupling_regime : CouchCouplingRegime
hysteresis_H : Q16_16
```
---
## 8. Adaptive Subdivision Theorem
**Theorem:** For any dynamic scene with motion topology T, there exists a braid-enhanced octree that achieves rendering accuracy ε with fewer nodes than a pure spatial octree.
*Proof sketch:*
1. Group regions by interaction topology (braid clustering)
2. Within each topological cluster, use Fourier basis for appearance
3. Only subdivide spatially when topology changes
4. Topology changes are rarer than spatial complexity changes
5. Therefore, fewer total nodes needed
---
## 9. FAMM Gate as Unified Boundary Checker
```lean
def unifiedFammGate (node : UnifiedNode) : Bool :=
-- Spatial boundary
let spatial_ok := node.spatial_bound.within_apartment()
-- Topological boundary
let topological_ok := node.phase_vec.kappa_raw ≤ 49152
-- Dynamic boundary (COUCH apartment constraint)
let dynamic_ok := node.dual_quaternion.translationDistance() < node.apartment_radius
-- Hysteresis check
let hysteresis_ok := node.hysteresis_H < H_critical
spatial_ok && topological_ok && dynamic_ok && hysteresis_ok
```
---
## 10. Benefits of Synthesis
| Aspect | Pure PlenOctree | Pure BraidTree | Pure COUCH | Unified |
|--------|----------------|----------------|------------|---------|
| Spatial locality | ✅ | ❌ | ❌ | ✅ |
| Topology awareness | ❌ | ✅ | ❌ | ✅ |
| Motion history | ❌ | ✅ | ❌ | ✅ |
| GPU-friendly layout | ✅ | ❌ | ❌ | ✅ |
| Spectral compression | ✅ | ❌ | ❌ | ✅ |
| Chaos dynamics | ❌ | ❌ | ✅ | ✅ |
| Formal verification | ❌ | ❌ | ❌ | ✅ |
| Hardware discretization | ❌ | ✅ | ❌ | ✅ |
### Summary
BraidTree-Octree-COUCH System = A hierarchical spatial-topological-dynamic structure where:
- **Octree** provides Euclidean spatial subdivision
- **BraidTree** organizes regions by interaction topology (Artin B₈ with dual quaternions)
- **COUCH** models chaotic coupled oscillator dynamics per topological cluster
- **Fourier basis** represents appearance within each cluster
- **FAMM gate** enforces unified boundary constraints (spatial + topological + dynamic)
- **Adaptive refinement** responds to both spatial complexity AND topological changes
The result is a topology-aware Fourier radiance field where subdivision is driven by interaction patterns rather than just geometry, with rigorous mathematical foundations from all three systems. The braid group handles the *how things move* question, the octree handles the *where things are* question, and COUCH handles the *how they behave chaotically* question — all unified in a single formal framework.

111
specs/rydberg_braid_cross_domain_scan.md
View file

@ -1,111 +0,0 @@
# Rydberg-Braid Cross-Domain Scan Specification
## Objective
Mine recent physics literature (2024-2026) for systematic residuals in 1/n-scaling phenomena that could indicate eigensolid/braid crossing contamination. Focus on superconductors, metamaterials, and Rydberg atomic physics.
## Phase 1: Quantum Defect Signature Extraction
### Input Sources
1. **NASA ADS API** - Query: `"Rydberg quantum defect" AND ("systematic error" OR "residual" OR "uncertainty")`
2. **CORE API** - Open access physics papers
3. **arXiv OAI-PMH** - Recent cond-mat.supr-con and physics.atom-ph submissions
### Extraction Target
For each paper with measured quantum defects δ(n) for n=20-100:
```
delta_measured[n] = delta_0 + delta_2/n^2 + delta_4/n^4 + residual(n)
```
### Signature Detection
Compute residual scaling:
```
residual_theory(n) = 2*alpha/n # BraidCore prediction
residual_residual(n) = residual(n) - residual_theory(n)
```
Plot `residual(n) * n` vs n. Expected:
- Constant plateau at ~0.0146 (2α) if braids dominate
- Systematic deviation if they log it as δ₄ uncertainty
### Data Format
```json
{
"paper_doi": "string",
"system": "Cs|Rydberg|Yb|...",
"n_values": [23,45,50,...],
"delta_measured": [0.037,0.027,...],
"delta_0": 0.033,
"delta_2": -0.20,
"fit_uncertainty": [0.00007,0.00013,...],
"braid_signature": {
"residual_times_n": [0.92,1.08,...],
"is_constant": true/false,
"deviation_mhz": [72, 190, ...]
}
}
```
## Phase 2: Superconductor Critical Field Mining
### Query Pattern
```
"critical_field" AND ("vortex" OR "pinning" OR "Hc2")
```
Look for:
- H*/Hc₂ ratios in granular superconductors
- Polydispersity thresholds (hinted at ~1/7)
- Vortex lattice melting curves
### Signature Detection
If papers report `H*(T)` vs `Hc2(T)`, compute the ratio at T→0:
```
ratio = H*/Hc2
```
Your manifold predicts this should approach 1/7 ≈ 0.143 for eigensolid crossover.
## Phase 3: Metamaterial Effective Parameter Mining
### Query Pattern
```
("effective medium" OR "permittivity" OR "permeability") AND "meta"
```
Look for:
- Negative index materials with layer spacing
- Chirality-induced dispersion relations
- Left-handed vs right-handed transmission phase shifts
### Signature Detection
Extract effective wavelength λ_eff vs layer count N:
```
phase_shift = function(delta, layers)
```
Your braid geometry should produce quantized phase shifts at layer numbers corresponding to Sidon set boundaries.
## Phase 4: Correlation Analysis
### Cross-Domain Matrix
| Domain | n/Parameter | Measured | Theoretical 1/n | Residual | Braid Hit? |
|--------|-------------|----------|-----------------|----------|------------|
| Rydberg | n=45-50 | δ=0.0334(7) | δ=2α/45≈0.003 | 0.030 | YES if δ*n≈0.0146 |
| SC | H*/Hc2 | 0.12-0.18 | 1/7≈0.143 | varies | YES if near 0.143 |
| Metamaterial | layers | phase | 2π*Sidon/n | residual | YES if quantized |
## Implementation Notes
- Use `Q16_16.ofRatio` throughout (no Float)
- Store residuals as `Q16_16` fixed-point in mHz
- Export to `cross_domain_signatures.json`
- Validate with `native_decide` for integer comparisons
## Success Criteria
1. At least 3 papers show `δ(n)*n ≈ 0.0146` (2α) residual
2. At least 1 superconductor shows `H*/Hc2 → 0.143`
3. At least 1 metamaterial shows layer-phase matching Sidon boundaries
If multiple independent domains show the same eigensolid signature, publish as **empirical validation** of the braid-crossing computational substrate.