Merge origin/main (docs + CFF updates) into main with spectral codebook

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
allaun 2026-07-01 21:17:24 -05:00
commit 6eae21513e
3 changed files with 248 additions and 601 deletions

View file

@ -1,15 +1,30 @@
cff-version: "1.2.0" cff-version: "1.2.0"
message: "When using SilverSight, please cite this repository." message: "If you use SilverSight in your work, please cite this repository using the metadata from this file."
type: software type: software
title: "SilverSight: Deterministic Equation Search and Classification" title: "SilverSight"
version: "0.1.0"
abstract: "A formally verified, hardware-native computation stack for braid topology analysis, eigensolid compression, and cross-domain 1/n-scaling signature mining."
keywords:
- formal verification
- lean 4
- braid topology
- spectral classification
- fixed-point arithmetic
- eigensolid compression
- signature mining
authors: authors:
- family-names: "Schneider" - family-names: "Schneider"
given-names: "Brandon" given-names: "Brandon"
alias: "allaunthefox" alias: "allaunthefox"
affiliation: "Independent Researcher"
orcid: "https://orcid.org/0000-0000-0000-0000"
repository: "https://github.com/allaunthefox/SilverSight"
repository-code: "https://github.com/allaunthefox/SilverSight" repository-code: "https://github.com/allaunthefox/SilverSight"
url: "https://github.com/allaunthefox/SilverSight" url: "https://github.com/allaunthefox/SilverSight"
date-released: "2026-06-21" date-released: "2026-06-21"
license: MIT license: Apache-2.0
commit: "4abd17ffeba2593767ecfc7ca82711de2a2eb921"
references: references:
- type: article - type: article
@ -18,6 +33,7 @@ references:
- family-names: "Imaginary" - family-names: "Imaginary"
given-names: "ICERM" given-names: "ICERM"
url: "https://www.imaginary.org/snapshot/solving-inverse-problems-with-bayes-theorem" url: "https://www.imaginary.org/snapshot/solving-inverse-problems-with-bayes-theorem"
year: 2025
notes: "Free-floating concept: Fisher-Rao geometry connection to Bayesian inference, inverse proof machinery alignment." notes: "Free-floating concept: Fisher-Rao geometry connection to Bayesian inference, inverse proof machinery alignment."
- type: software - type: software
@ -29,20 +45,21 @@ references:
repository-code: "https://github.com/allaunthefox/Research-Stack" repository-code: "https://github.com/allaunthefox/Research-Stack"
url: "https://github.com/allaunthefox/Research-Stack" url: "https://github.com/allaunthefox/Research-Stack"
date-released: "2026-05-08" date-released: "2026-05-08"
license: "Apache-2.0" license: Apache-2.0
notes: "Parent research repository (https://github.com/allaunthefox/Research-Stack). SilverSight ports proven Lean modules (`Semantics.FixedPoint`, `Semantics.SidonSets`, `Semantics.SieveLemmas`, `Semantics.InteractionGraphSidon`, `Semantics.BraidEigensolid`, `Semantics.BraidSpherionBridge`, etc.), agent co" notes: "Parent research repository. SilverSight ports proven Lean modules (Semantics.FixedPoint, Semantics.SidonSets, Semantics.SieveLemmas, Semantics.InteractionGraphSidon, Semantics.BraidEigensolid, Semantics.BraidSpherionBridge)."
- type: software - type: software
title: "GP_ELITE: Régression symbolique par programmation génétique" title: "GP_ELITE: Regression symbolique par programmation genetique"
authors: authors:
- name: "Sabri Hakou" - name: "Sabri Hakou"
version: "0.1.0" version: "0.1.0"
date-released: "2026-06-13" date-released: "2026-06-13"
license: "MIT" license: MIT
repository-code: "https://github.com/ariel95500-create/gp-elite" repository-code: "https://github.com/ariel95500-create/gp-elite"
notes: "Inspired SilverSight's native symbolic regression design. GP-ELITE uses genetic programming with asymmetric island model, BIC fitness, linear scaling (Keijzer 2003), ε-lexicase selection, and stigmergic memory. SilverSight reimplements these concepts using existing infrastructure: HachimojiCodec cla" notes: "Inspired SilverSight's native symbolic regression design. GP-ELITE uses genetic programming with asymmetric island model, BIC fitness, linear scaling (Keijzer 2003), epsilon-lexicase selection, and stigmergic memory."
- type: unpublished - type: unpublished
title: "Photon-Varied Gaussian States"
authors: authors:
- family-names: "Giani" - family-names: "Giani"
given-names: "A." given-names: "A."
@ -50,39 +67,38 @@ references:
given-names: "S." given-names: "S."
- family-names: "Conti" - family-names: "Conti"
given-names: "C." given-names: "C."
title: "Photon-Varied Gaussian States" year: 2025
year: "2025" notes: "Binds to Research Stack Semantics.PVGS_DQ_Bridge -> SilverSight formal/PVGS_DQ_Bridge/; preprint identifier pending confirmation."
notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; preprint identifier pending confirmation."
- type: unpublished - type: unpublished
title: "Stellar representation of non-Gaussian quantum states"
authors: authors:
- family-names: "Chabaud" - family-names: "Chabaud"
given-names: "U." given-names: "U."
- family-names: "Mehraban" - family-names: "Mehraban"
given-names: "S." given-names: "S."
title: "Stellar representation of non-Gaussian quantum states" year: 2022
year: "2022" notes: "Binds to Research Stack Semantics.PVGS_DQ_Bridge -> SilverSight formal/PVGS_DQ_Bridge/; full citation details pending DOI or arXiv ID."
notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; full citation details pending DOI or arXiv ID."
- type: unpublished - type: unpublished
title: "Wigner negativity of superpositions"
authors: authors:
- family-names: "Pizzimenti" - family-names: "Pizzimenti"
given-names: "C." given-names: "C."
- family-names: "et al." - literal: "et al."
title: "Wigner negativity of superpositions" year: 2024
year: "2024" notes: "Binds to Research Stack Semantics.BindingSite / Semantics.PVGS_DQ_Bridge -> SilverSight formal/BindingSite/; full citation details pending DOI or arXiv ID."
notes: "Binds to Research Stack `Semantics.BindingSite` / `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/BindingSite/`; full citation details pending DOI or arXiv ID."
- type: unpublished - type: unpublished
title: "Single quadrature noise tomography"
authors: authors:
- family-names: "Wassner" - family-names: "Wassner"
given-names: "M." given-names: "M."
- family-names: "et al." - literal: "et al."
title: "Single quadrature noise tomography" year: 2025
year: "2025" notes: "Binds to Research Stack Semantics.PVGS_DQ_Bridge -> SilverSight formal/PVGS_DQ_Bridge/; full citation details pending DOI or arXiv ID."
notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; full citation details pending DOI or arXiv ID."
- type: thesis - type: article
title: "Pascal's Triangle, Pascal's Pyramid, and the Trinomial Triangle" title: "Pascal's Triangle, Pascal's Pyramid, and the Trinomial Triangle"
authors: authors:
- family-names: "Saucedo" - family-names: "Saucedo"
@ -92,7 +108,7 @@ references:
name: "California State University, San Bernardino" name: "California State University, San Bernardino"
collection-title: "Electronic Theses, Projects, and Dissertations" collection-title: "Electronic Theses, Projects, and Dissertations"
url: "https://scholarworks.lib.csusb.edu/etd/855" url: "https://scholarworks.lib.csusb.edu/etd/855"
notes: "Binds to Research Stack `Semantics.SidonSets` → SilverSight `formal/CoreFormalism/SidonSets.lean`; supports Sidon-set constructions, Singer-theorem residues, and number-theory fixtures. The chaos-game appendix was dropped during porting." notes: "Binds to Research Stack Semantics.SidonSets -> SilverSight formal/CoreFormalism/SidonSets.lean; supports Sidon-set constructions, Singer-theorem residues, and number-theory fixtures."
- type: article - type: article
title: "Close packing density of polydisperse hard spheres" title: "Close packing density of polydisperse hard spheres"
@ -104,7 +120,7 @@ references:
date-published: "2009-12" date-published: "2009-12"
doi: "10.1063/1.3276799" doi: "10.1063/1.3276799"
journal: "The Journal of Chemical Physics" journal: "The Journal of Chemical Physics"
notes: "Binds to Research Stack `Semantics.BraidEigensolid` / `Semantics.BraidSpherionBridge` / `Semantics.BaselineComparison` → SilverSight `formal/CoreFormalism/BraidEigensolid.lean` / `formal/CoreFormalism/BraidSpherionBridge.lean`; anchor paper for polydisperse close-packing theory used in eigensolid co" notes: "Binds to Research Stack Semantics.BraidEigensolid / Semantics.BraidSpherionBridge / Semantics.BaselineComparison -> SilverSight formal/CoreFormalism/BraidEigensolid.lean / formal/CoreFormalism/BraidSpherionBridge.lean."
- type: article - type: article
title: "Fractionation effects in phase equilibria of polydisperse hard-sphere colloids" title: "Fractionation effects in phase equilibria of polydisperse hard-sphere colloids"
@ -116,7 +132,7 @@ references:
date-published: "2004-10" date-published: "2004-10"
doi: "10.1103/physreve.70.041410" doi: "10.1103/physreve.70.041410"
journal: "Physical Review E" journal: "Physical Review E"
notes: "Binds to Research Stack `Semantics.BraidEigensolid` (meta-solid concept captured in ContextStream node `e967f515-...`) → SilverSight `formal/CoreFormalism/BraidEigensolid.lean`; terminal polydispersity ~14% underpins the meta-solid 1/7 mixing threshold (one complete Sidon doubling step)." notes: "Binds to Research Stack Semantics.BraidEigensolid; terminal polydispersity ~14% underpins the meta-solid 1/7 mixing threshold."
- type: article - type: article
title: "Random-close packing limits for monodisperse and polydisperse hard spheres" title: "Random-close packing limits for monodisperse and polydisperse hard spheres"
@ -128,7 +144,7 @@ references:
date-published: "2014" date-published: "2014"
doi: "10.1039/c3sm52959b" doi: "10.1039/c3sm52959b"
journal: "Soft Matter" journal: "Soft Matter"
notes: "Binds to Research Stack `Semantics.BraidEigensolid` → SilverSight `formal/CoreFormalism/BraidEigensolid.lean`; definitive random-close-packing limits for monodisperse (~0.64) and polydisperse spheres used in eigensolid packing-bound claims." notes: "Binds to Research Stack Semantics.BraidEigensolid -> SilverSight formal/CoreFormalism/BraidEigensolid.lean; definitive random-close-packing limits."
- type: article - type: article
title: "Freezing of polydisperse hard spheres" title: "Freezing of polydisperse hard spheres"
@ -140,7 +156,7 @@ references:
date-published: "1999" date-published: "1999"
doi: "10.1103/physreve.59.618" doi: "10.1103/physreve.59.618"
journal: "Physical Review E" journal: "Physical Review E"
notes: "Binds to Research Stack `Semantics.BraidEigensolid` / `Semantics.BaselineComparison` → SilverSight `formal/CoreFormalism/BraidEigensolid.lean`; fractionating phase behavior of polydisperse hard spheres used in braid/meta-solid phase-transition fixtures." notes: "Binds to Research Stack Semantics.BraidEigensolid / Semantics.BaselineComparison -> SilverSight formal/CoreFormalism/BraidEigensolid.lean."
- type: article - type: article
title: "A Differentiable Interior-Point Method in Single Precision" title: "A Differentiable Interior-Point Method in Single Precision"
@ -153,7 +169,7 @@ references:
given-names: "Zachary" given-names: "Zachary"
date-published: "2026-05" date-published: "2026-05"
url: "https://arxiv.org/abs/2605.17913" url: "https://arxiv.org/abs/2605.17913"
notes: "Binds to Research Stack `Semantics.FixedPoint` (inverse-proof machinery in `Semantics.Q16InverseProof`) → SilverSight `formal/CoreFormalism/FixedPoint.lean`; differentiable primal-dual IPM with bounded KKT systems for low-precision / fixed-point arithmetic, justifying the no-Float compute boundary." notes: "Binds to Research Stack Semantics.FixedPoint -> SilverSight formal/CoreFormalism/FixedPoint.lean; differentiable primal-dual IPM with bounded KKT systems."
- type: article - type: article
title: "Everything Is Logarithms" title: "Everything Is Logarithms"
@ -162,7 +178,7 @@ references:
given-names: "Alex" given-names: "Alex"
date-published: "2026-05-25" date-published: "2026-05-25"
url: "https://alexkritchevsky.com/2026/05/25/everything-is-logarithms.html" url: "https://alexkritchevsky.com/2026/05/25/everything-is-logarithms.html"
notes: "Binds to SilverSight `formal/CoreFormalism/HachimojiLUT.lean` (PhaseCircle, phaseEmbed) and `formal/CoreFormalism/ChentsovFinite.lean` (Fisher metric uniqueness). Core claim: logarithms are coordinate-free objects; units emerge from ratios (log N / log 2), and dim(U⊗V) = dim(U)×dim(V) mirrors the a" notes: "Binds to SilverSight formal/CoreFormalism/HachimojiLUT.lean and formal/CoreFormalism/ChentsovFinite.lean. Core claim: logarithms are coordinate-free objects."
- type: article - type: article
title: "Stabilizing Recurrent Dynamics for Test-Time Scalable Latent Reasoning in Looped Language Models" title: "Stabilizing Recurrent Dynamics for Test-Time Scalable Latent Reasoning in Looped Language Models"
@ -183,17 +199,15 @@ references:
given-names: "Yu-Feng" given-names: "Yu-Feng"
date-published: "2026-05" date-published: "2026-05"
url: "https://arxiv.org/abs/2605.26733" url: "https://arxiv.org/abs/2605.26733"
notes: "Binds to Research Stack `Semantics.AVMIsa.*` / `Semantics.Run` → SilverSight `Core/SilverSightCore.lean` AVM transition function; STARS regularizes spectral radius of the Jacobian using power iterations with JVPs, relevant to recurrent / looped AVM search dynamics." notes: "Binds to Research Stack Semantics.AVMIsa.* / Semantics.Run -> SilverSight Core/SilverSightCore.lean AVM transition function; STARS regularizes spectral radius."
- type: online - type: online
title: "Tangent lines to parabola at ends of focal chord are perpendicular (calculus proof)" title: "Tangent lines to parabola at ends of focal chord are perpendicular (calculus proof)"
authors: authors:
- family-names: "Unknown" - literal: "Unknown"
date-published: "2025" date-published: "2025"
url: "https://www.reddit.com/r/calculus/comments/1udl2t6/show_lines_tangent_to_parabola_at_the_ends_of_a/" url: "https://www.reddit.com/r/calculus/comments/1udl2t6/show_lines_tangent_to_parabola_at_the_ends_of_a/"
notes: "Demonstrates focal chord perpendicularity: s₁·s₂ = -1. Maps to Hachimoji eigensolid conjugate pairs with 1/n scaling - one slope grows as m, other decays as 1/m, product = -1 constant. Structural identity to softplus complementarity b_κ(v)·b_κ(-v) = κ. Key geometric rigidty pattern for Fisher manifold braids." notes: "Demonstrates focal chord perpendicularity. Maps to Hachimoji eigensolid conjugate pairs with 1/n scaling."
# ── Implemented references ported from Research Stack ──────────────
- type: article - type: article
title: "Brownian dynamics of polydisperse colloidal hard spheres: Equilibrium structures and random close packings" title: "Brownian dynamics of polydisperse colloidal hard spheres: Equilibrium structures and random close packings"
@ -224,7 +238,7 @@ references:
authors: authors:
- family-names: "Santiso" - family-names: "Santiso"
given-names: "E." given-names: "E."
- family-names: "Müller" - family-names: "Muller"
given-names: "E. A." given-names: "E. A."
date-published: "2002" date-published: "2002"
doi: "10.1080/00268970210125313" doi: "10.1080/00268970210125313"
@ -234,7 +248,7 @@ references:
- type: article - type: article
title: "Freezing line of polydisperse hard spheres via direct-coexistence simulations" title: "Freezing line of polydisperse hard spheres via direct-coexistence simulations"
authors: authors:
- family-names: "Castagnède" - family-names: "Castagnede"
given-names: "A." given-names: "A."
- family-names: "Filion" - family-names: "Filion"
given-names: "L." given-names: "L."
@ -257,7 +271,6 @@ references:
- family-names: "Zia" - family-names: "Zia"
given-names: "R." given-names: "R."
date-published: "2025" date-published: "2025"
doi: "10.1017/jfm.2026.11287"
journal: "Journal of Fluid Mechanics" journal: "Journal of Fluid Mechanics"
notes: "Entropy-exchange mechanism to access monodisperse hard-sphere fluid-crystal coexistence." notes: "Entropy-exchange mechanism to access monodisperse hard-sphere fluid-crystal coexistence."
@ -282,7 +295,7 @@ references:
authors: authors:
- family-names: "De Jager" - family-names: "De Jager"
given-names: "M." given-names: "M."
- family-names: "Castagnède" - family-names: "Castagnede"
given-names: "A." given-names: "A."
- family-names: "Smallenburg" - family-names: "Smallenburg"
given-names: "F." given-names: "F."
@ -297,8 +310,8 @@ references:
authors: authors:
- family-names: "Cantor" - family-names: "Cantor"
given-names: "D." given-names: "D."
- family-names: "Azéma" - family-names: "Azema"
given-names: "É." given-names: "E."
- family-names: "Sornay" - family-names: "Sornay"
given-names: "P." given-names: "P."
- family-names: "Radjai" - family-names: "Radjai"
@ -346,553 +359,3 @@ references:
institution: institution:
name: "University of Twente" name: "University of Twente"
notes: "Polydisperse hard-sphere EOS, moments, glassy regime." notes: "Polydisperse hard-sphere EOS, moments, glassy regime."
- type: article
title: "The plane-wall effect on monodisperse and polydisperse sphere packings"
authors:
- family-names: "Zhou"
given-names: "X."
- family-names: "Huang"
given-names: "Z."
- family-names: "Li"
given-names: "S."
date-published: "2025"
doi: "10.1016/j.powtec.2025.120669"
journal: "Powder Technology"
notes: "Wall effects in monodisperse vs polydisperse packings."
- type: article
title: "Random packing fraction of binary similar particles: Onsager's model revisited"
authors:
- family-names: "Brouwers"
given-names: "H."
date-published: "2022"
doi: "10.3367/ufne.2023.11.039606"
journal: "Uspekhi Fizicheskih Nauk"
notes: "Binary packing density theory."
- type: article
title: "Mechanical response of particle packings at jamming onset"
authors:
- family-names: "Huang"
given-names: "Z."
- family-names: "Zhou"
given-names: "X."
- family-names: "Li"
given-names: "S."
date-published: "2025"
doi: "10.1039/d5sm00762c"
journal: "Soft Matter"
notes: "Bulk modulus reduction from rattlers at jamming onset."
- type: article
title: "Dynamical coexistence in moderately polydisperse hard-sphere glasses"
authors:
- family-names: "Campo"
given-names: "M."
- family-names: "Speck"
given-names: "T."
date-published: "2019"
doi: "10.1063/1.5134842"
journal: "The Journal of Chemical Physics"
notes: "Dynamical heterogeneity in polydisperse glasses."
- type: article
title: "Reentrant melting in polydispersed hard spheres"
authors:
- family-names: "Bartlett"
given-names: "P."
- family-names: "Warren"
given-names: "P. B."
date-published: "1999"
doi: "10.1103/physrevlett.82.1979"
journal: "Physical Review Letters"
notes: "Predicted reentrant melting at high polydispersity; later challenged by full fractionation calculations."
- type: article
title: "Molecular dynamics simulations of crystallization of hard spheres"
authors:
- family-names: "Volkov"
given-names: "I."
- family-names: "Cieplak"
given-names: "M."
- family-names: "Koplik"
given-names: "J."
- family-names: "Banavar"
given-names: "J."
date-published: "2002"
doi: "10.1103/physreve.66.061401"
journal: "Physical Review E"
notes: "MD comparison of monodisperse vs polydisperse crystallization rates."
- type: article
title: "Sedimentation of monodisperse and bidisperse hard-sphere colloidal suspensions"
authors:
- family-names: "Al-Naafa"
given-names: "M."
- family-names: "Selim"
given-names: "M."
date-published: "1992"
doi: "10.1002/aic.690381012"
journal: "AIChE Journal"
notes: "Early monodisperse/bidisperse sedimentation theory."
- type: article
title: "Destruction of the Meissner effect in granular high-temperature superconductors"
authors:
- family-names: "Johnston"
given-names: "K."
date-published: "1992"
doi: "10.1103/physrevlett.69.2268"
journal: "Physical Review Letters"
notes: "Experimental/computational destruction of Meissner in granular HTSC."
- type: article
title: "Thermal fluctuations, quenched disorder, phase transitions, and transport in type-II superconductors"
authors:
- family-names: "Fisher"
given-names: "D."
- family-names: "Fisher"
given-names: "M."
- family-names: "Huse"
given-names: "D."
date-published: "1991"
doi: "10.1103/physrevb.43.130"
journal: "Physical Review B"
notes: "Foundational vortex-glass theory; continuous transitions from scaling."
- type: article
title: "Phase transitions in a disordered granular superconductor near percolation"
authors:
- family-names: "J."
given-names: "J."
- family-names: "L."
given-names: "L."
date-published: "1986"
doi: "10.1103/physrevb.34.4815"
journal: "Physical Review B"
notes: "Granular Josephson-network glass phases near percolation threshold."
- type: article
title: "Superconducting transition in disordered granular superconductors in magnetic fields"
authors:
- family-names: "Ikeda"
given-names: "R."
date-published: "2005"
doi: "10.1103/physrevb.74.054510"
journal: "Physical Review B"
notes: "Field-driven glass transitions in granular superconductors."
- type: article
title: "Vortex-glass superconductivity: A possible new phase in bulk high-Tc oxides"
authors:
- family-names: "Fisher"
given-names: "M. P. A."
date-published: "1989"
doi: "10.1103/physrevlett.62.1415"
journal: "Physical Review Letters"
notes: "Original vortex-glass superconductivity proposal (zero linear resistivity)."
- type: article
title: "Vortex Glass—Vortex Liquid Transition in BaFe2(As1-xPx)2 and CaKFe4As4 Superconductors from Multi-Harmonic AC Magnetic Susceptibility Studies"
authors:
- family-names: "Ivan"
given-names: "I."
- family-names: "Ionescu"
given-names: "A."
- family-names: "Crisan"
given-names: "D."
- family-names: "Crisan"
given-names: "A."
date-published: "2023"
doi: "10.3390/ijms24097896"
journal: "International Journal of Molecular Sciences"
notes: "Multi-harmonic AC susceptibility identification of VG-VL transition."
- type: article
title: "Evidence of the Vortex-Glass Transition in Homogeneously Disordered Thick Films of a-MoxSi1-x"
authors:
- family-names: "Okuma"
given-names: "S."
- family-names: "Arai"
given-names: "M."
date-published: "2000"
doi: "10.1143/jpsj.69.2747"
journal: "Journal of the Physical Society of Japan"
notes: "Continuous VG transition from scaling in homogeneous disordered films."
- type: article
title: "Universal scaling behaviour near vortex-solid/glass to vortex-fluid transition in type-II superconductors in two and three dimensions"
authors:
- family-names: "Kundu"
given-names: "H. K."
- family-names: "Jesudasan"
given-names: "J."
- family-names: "Raychaudhuri"
given-names: "P."
- family-names: "Mukerjee"
given-names: "S."
- family-names: "Bid"
given-names: "A."
date-published: "2019"
doi: "10.1209/0295-5075/128/27001"
journal: "Europhysics Letters"
notes: "Universal scaling of VG-VL transitions in 2D and 3D."
- type: article
title: "Peak effect, vortex-lattice melting line, and order-disorder transition in conventional and high-Tc superconductors"
authors:
- family-names: "Mikitik"
given-names: "G."
- family-names: "Brandt"
given-names: "E."
date-published: "2001"
doi: "10.1103/physrevb.64.184514"
journal: "Physical Review B"
notes: "Order-disorder transitions and characteristic fields in vortex matter."
- type: article
title: "Observation of predicted superconductivity in Gd1.4Ce0.6Sr2Cu2TiOx with x ≈ 10"
authors:
- family-names: "Blackstead"
given-names: "H. A."
- family-names: "Dow"
given-names: "J."
- family-names: "Goldschmidt"
given-names: "D."
- family-names: "Pulling"
given-names: "D. B."
date-published: "1998"
doi: "10.1016/s0375-9601(98)00348-x"
journal: "Physics Letters A"
notes: "Granular superconductivity with mesoscopic Meissner and vortex dissipation."
- type: article
title: "Observation of the Granular Josephson Mechanism and the Vortex-Glass Transition in the Polycrystalline GdBa2Cu3O7-δ Superconductor"
authors:
- family-names: "Vargas-Pineda"
given-names: "E. M."
- family-names: "Rivera-Contreras"
given-names: "L. J."
- family-names: "Pineda-Peña"
given-names: "G."
- family-names: "Téllez"
given-names: "D."
- family-names: "Roa-Rojas"
given-names: "J."
date-published: "2024"
doi: "10.1007/s10948-024-06783-w"
journal: "Journal of Superconductivity and Novel Magnetism"
notes: "Granular Josephson + VG in polycrystalline Gd-123."
- type: article
title: "Long-Range Superconducting Transition Limited by Phase Slip or Vortex Glass Phase in SmFe1-xCoxAsO Polycrystalline Thin Films"
authors:
- family-names: "Aguilar-Mendoza"
given-names: "K."
- family-names: "Guillen-Cervantes"
given-names: "A."
- family-names: "Corrales-Mendoza"
given-names: "I."
- family-names: "Conde-Gallardo"
given-names: "A."
date-published: "2025"
doi: "10.1007/s10948-025-06949-0"
journal: "Journal of Superconductivity and Novel Magnetism"
notes: "Metallic intergranular connectivity required for VG phase in Sm-1111 films."
- type: article
title: "Vortex-glass transition and vortex pinning behavior in three-dimensional NbTiN epitaxial films"
authors:
- family-names: "Han"
given-names: "Z."
- family-names: "Jing"
given-names: "T."
- family-names: "Yang"
given-names: "J."
- family-names: "Cai"
given-names: "W."
- family-names: "Li"
given-names: "Z."
date-published: "2024"
doi: "10.1088/1361-6668/ad3f82"
journal: "Superconductor Science and Technology"
notes: "3D NbTiN epitaxial film VG transition from transport scaling."
- type: article
title: "Vortex-glass transitions in low-Tc superconducting Nb thin films and Nb/Cu superlattices"
authors:
- family-names: "Villegas"
given-names: "J."
- family-names: "Vicent"
given-names: "J."
date-published: "2005"
doi: "10.1103/physrevb.71.144522"
journal: "Physical Review B"
notes: "VG transitions in Nb films and superlattices from transport."
- type: article
title: "Unveiling the vortex glass phase in the surface and volume of a type-II superconductor"
authors:
- family-names: "Sánchez"
given-names: "J. A."
- family-names: "Maldonado"
given-names: "R. C."
- family-names: "Bolecek"
given-names: "N. R. C."
date-published: "2019"
doi: "10.1038/s42005-019-0243-4"
journal: "Communications Physics"
notes: "First-order BG-VG transition in Bi-2212 from surface and volume probes."
- type: article
title: "Study of vortex glass-liquid transition in superconducting Fe(Te, Se) thin films on LaAlO3 substrates"
authors:
- family-names: "Kumar"
given-names: "R."
- family-names: "Mitra"
given-names: "A."
- family-names: "Varma"
given-names: "G. D."
date-published: "2019"
doi: "10.1063/1.5093284"
journal: "Journal of Applied Physics"
notes: "Material-specific crossover near 2 T in Fe(Te,Se) films."
- type: article
title: "Vortex-glass phases in type-II superconductors"
authors:
- family-names: "Nattermann"
given-names: "T."
- family-names: "Scheidl"
given-names: "S."
date-published: "2000"
doi: "10.1080/000187300412257"
journal: "Advances in Physics"
notes: "Comprehensive review of vortex-glass phases."
- type: article
title: "Effects of line disorder on the vortex-glass transition induced by point disorder"
authors:
- family-names: "Ikeda"
given-names: "R."
date-published: "2001"
doi: "10.1143/jpsj.70.219"
journal: "Journal of the Physical Society of Japan"
notes: "Line vs point disorder effects on VG transition; slush regimes."
- type: article
title: "Theory of Magnetic Domain Phases in Ferromagnetic Superconductors"
authors:
- family-names: "Devizorova"
given-names: "Z. A."
- family-names: "Mironov"
given-names: "S."
- family-names: "Buzdin"
given-names: "A."
date-published: "2019"
doi: "10.1103/physrevlett.122.117002"
journal: "Physical Review Letters"
notes: "First-order transitions in ferromagnetic superconductor domain phases."
- type: article
title: "Exotic diffeomorphisms and the 7th dimension"
authors:
- family-names: "Weinberger"
given-names: "Akiva"
date-published: "2026-06-24"
url: "https://akivaweinberger.wordpress.com/2026/06/24/exotic-diffeos-and-the-7th-dim/"
notes: "Exotic diffeomorphisms of S⁶: 28 connected components of Diff⁺(S⁶), explicit Durán formula using quaternionic rotations. Directly applicable to SilverSight Fisher metric on Δ₇ ≅ S⁷: (1) 28-fold periodicity constrains max smooth eigensolid equivalence classes; (2) corkscrew angle ψ = 2π/φ² isomorphic to Durán rotation 2θ where tan θ = |u|/t; (3) Durán's formula σ(t,u,v) = (t,u',v') with rotation about W by 2π|v| is a braid crossing (two 3-vectors u,v with depth t). Corollary: at most 28 isotopy-distinct braid convergence regimes in Fisher metric."
- type: article
title: "Pointed Wiedersehen Metrics on Exotic Spheres and Diffeomorphisms of S⁶"
authors:
- family-names: "Durán"
given-names: "Carlos E."
date-published: "2001"
doi: "10.1023/A:1013163427655"
journal: "Geometriae Dedicata"
volume: "88"
pages: "199-210"
notes: "Explicit quaternionic formula for exotic diffeomorphism σ: S⁶ → S⁶ not isotopic to identity, σ²⁸ ≃ id. SilverSight Durán map is projection onto Fisher simplex boundary."
- type: article
title: "On Manifolds Homeomorphic to the 7-Sphere"
authors:
- family-names: "Milnor"
given-names: "John W."
date-published: "1956"
journal: "Annals of Mathematics"
volume: "64"
number: "2"
pages: "399-405"
notes: "Original construction of exotic 7-spheres via S³-bundle over S⁴ from quaternionic Hopf fibration. Foundation for Durán exotic diffeomorphism of S⁶."
- type: article
title: "Some geometric formulas and cancellations in algebraic and differential topology"
authors:
- family-names: "Durán"
given-names: "C."
- family-names: "Püttmann"
given-names: "T."
- family-names: "Rigas"
given-names: "A."
date-published: "2005"
journal: "Matemática Contemporânea"
volume: "28"
pages: "1-26"
doi: "10.21711/231766362005/rmc287"
notes: "Extended exotic diffeomorphism analysis with explicit formulas and geometric cancellation in quaternionic formulation."
# ── TODO: Not yet implemented in SilverSight ────────────────────────
# Uncomment when modules are ported from Research Stack.
# - type: thesis
# title: "Addressing Rural Mental Health Crises: An Alternative to Police"
# authors:
# - family-names: "Weatheral-block"
# given-names: "Faith Ann"
# date-published: "2024-05"
# institution:
# name: "California State University, San Bernardino"
# collection-title: "Electronic Theses, Projects, and Dissertations"
# url: "https://scholarworks.lib.csusb.edu/etd/1957"
# notes: "Exploratory qualitative social-work project for rural crisis-response domain fixtures and route-token provenance; not evidence for quantitative safety or formal claims."
# - type: article
# title: "Effects of Polydispersity on Structuring and Rheology in Flowing Suspensions"
# authors:
# - family-names: "Rosenbaum"
# given-names: "E."
# - family-names: "Massoudi"
# given-names: "M."
# - family-names: "Dayal"
# given-names: "K."
# date-published: "2019"
# doi: "10.1115/1.4043094"
# journal: "Journal of Applied Mechanics"
# notes: "Shear-induced ordering suppressed by small polydispersity."
# - type: article
# title: "Lattice-Boltzmann simulations of low-Reynolds-number flow past mono- and bidisperse arrays of spheres: results for the permeability and drag force"
# authors:
# - family-names: "van der Hoef"
# given-names: "M. A."
# - family-names: "Beetstra"
# given-names: "R."
# - family-names: "Kuipers"
# given-names: "J. A. M."
# date-published: "2005"
# doi: "10.1017/s0022112004003295"
# journal: "Journal of Fluid Mechanics"
# notes: "Drag force changes up to 5× in bidisperse arrays."
# - type: article
# title: "Orbital glass in HTSC: a new state of condensed matter"
# authors:
# - family-names: "Kusmartsev"
# given-names: "F."
# date-published: "1992"
# doi: "10.1007/bf00620505"
# journal: "Journal of Superconductivity"
# notes: "Orbital-glass state from frustrated Josephson loops in granular HTSC; Meissner disappearance at low fields."
# - type: article
# title: "Paramagnetic Meissner effect and related dynamical phenomena"
# authors:
# - family-names: "Li"
# given-names: "M."
# date-published: "2003"
# doi: "10.1016/s0370-1573(02)00635-x"
# journal: "Physics Reports"
# notes: "Review of paramagnetic Meissner effect in granular Bi-2212."
# - type: article
# title: "Fragile-to-strong glass transition in two-dimensional vortex liquids"
# authors:
# - family-names: "Maccari"
# given-names: "I."
# - family-names: "Benfatto"
# given-names: "L."
# - family-names: "Castellani"
# given-names: "C."
# - family-names: "Lorenzana"
# given-names: "J."
# - family-names: "De Michele"
# given-names: "C."
# date-published: "2024"
# doi: "10.1103/physrevresearch.7.013160"
# journal: "Physical Review Research"
# notes: "Fragile-to-strong glass transition in 2D vortex liquids."
# - type: article
# title: "Unveiling of Bragg glass to vortex glass transition by an ac driving force in a single crystal of Yb3Rh4Sn13"
# authors:
# - family-names: "Kumar"
# given-names: "S."
# - family-names: "Singh"
# given-names: "R."
# - family-names: "Thamizhavel"
# given-names: "A."
# - family-names: "Tomy"
# given-names: "C."
# - family-names: "Grover"
# given-names: "A."
# date-published: "2015"
# doi: "10.1088/0953-2048/28/8/085013"
# journal: "Superconductor Science and Technology"
# notes: "Material-specific H* ~4 kOe for BG-VG transition in Yb3Rh4Sn13."
# - type: article
# title: "Paramagnetic Meissner effect in YBa2Cu3O7/La0.7Ca0.3MnO3 superlattices"
# authors:
# - family-names: "Torre"
# given-names: "M. A. L. L."
# - family-names: "Peña"
# given-names: "V."
# - family-names: "Sefrioui"
# given-names: "Z."
# date-published: "2006"
# doi: "10.1103/physrevb.73.052503"
# journal: "Physical Review B"
# notes: "PME in YBCO/LCMO superlattices with granular manganite layers."
# - type: article
# title: "Critical currents at the Bragg glass to vortex glass transition"
# authors:
# - family-names: "Hernández"
# given-names: "A. D."
# - family-names: "Domínguez"
# given-names: "D."
# date-published: "2003"
# doi: "10.1103/physrevlett.92.117002"
# journal: "Physical Review Letters"
# notes: "Simulated first-order BG-VG transition with critical current signature."
# - type: article
# title: "Second magnetization peak, rhombic-to-square Bragg vortex glass transition, and intersecting magnetic hysteresis curves in overdoped BaFe2(As1xPx)2 single crystals"
# authors:
# - family-names: "Miu"
# given-names: "L."
# - family-names: "Ionescu"
# given-names: "A."
# - family-names: "Miu"
# given-names: "D."
# date-published: "2020"
# doi: "10.1038/s41598-020-74156-z"
# journal: "Scientific Reports"
# notes: "SMP and rhombic-square Bragg glass transition."
# - type: article
# title: "Vortex phase diagram in 12442-type RbCa2Fe4As4F2 single crystal revealed by magneto-transport and magnetization measurements"
# authors:
# - family-names: "Xing"
# given-names: "X."
# - family-names: "Yi"
# given-names: "X."
# - family-names: "Li"
# given-names: "M."
# date-published: "2020"
# doi: "10.1088/1361-6668/abb35f"
# journal: "Superconductor Science and Technology"
# notes: "Vortex slush and intermediate regimes between VG and VL."

View file

@ -61,3 +61,52 @@ Standalone formula for the hardest Layer 3 conjecture: a Cartan connection of ty
--- ---
## Pre-2026-06-26 ## Pre-2026-06-26
---
## 2026-07-02
### Integer Spiral Packing Fix
**Status:** RESOLVED
- Upstream rewrote phi_corkscrew_index: packed signed coefficients without offset encoding
- Bug: Not injective ((-1,1) and (1,0) both give 1 in base 2)
- Fixed in upstream
- Added canonical corpus-wide version to spectral_codebook.py
- Base: 328,469 / Offset: 164,234 recorded in JSON header
- Unpack inverts exactly
- Round-trip verified over all 250 matrices
### f(n) Layout (Decorative) - NEW
**Status:** IMPLEMENTED
- Each entry gets radius_sq (= spiral index) and angle_frac
- Computed in decimal (indices reach ~10^44 where float64 keeps zero fractional bits)
- Verified against VERIFICATION_LOG V007: f(20121) reproduces (-137.80079576, -33.64432624)
- Min angular separation: ≈ 4.6×10^-6 of a turn
### Cartan Δ-Floor Enhancement
**Status:** IMPLEMENTED
- Upstream only had 1-D ρ-snapping
- Added Fisher version on Δ_7 with Δ = 17/1792 exact (CartanConnection.lean:70)
- 13 fingerprint pairs fall below Δ
- Merging 196 fingerprints into 187 Δ-resolution codewords vs 9 gap-rule clusters
- Both rules emitted side by side
- **Caveat:** |c|/Σ|c| projection destroys sign/scale
- This corpus has two distinct fingerprints at Fisher distance exactly 0
- Fisher layer is similarity, not identity
### Torus Winding Improvement
**Status:** IMPLEMENTED
- Upstream's _safe variant only detected saturation
- TorusWinding now carries a_exact/b_exact (plain )
- torus_to_spiral_index prefers them
- Round trip lossless
- Regression-tested at n = 10^9
- **Note:** Lean mirror in BraidEigensolid.lean needs same widening (noted in docstring, Lean untouched)
### Fingerprint Discrepancy Resolution
**Status:** RESOLVED
- 192-vs-196 fingerprint discrepancy was stale docstring
- Both methods agree coefficient-for-coefficient on all 250 matrices (196 unique)
- 43/43 tests pass (19 new)
- Docs extended with exact-vs-decorative labels per layer

View file

@ -14,14 +14,23 @@ SilverSight invents names only when necessary. When a concept already exists und
| SilverSight Term | Standard Terminology | Delta / Note | File:Line | Tags | See Also | | SilverSight Term | Standard Terminology | Delta / Note | File:Line | Tags | See Also |
|------------------|----------------------|--------------|-----------|------|----------| |------------------|----------------------|--------------|-----------|------|----------|
| **Sidon set** | B₂ sequence, ErdősSidon set | Standard combinatorial object; SilverSight uses it for deterministic strand addressing. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical #core | [Sidon label](#sidon-label) | | **Sidon set** | B₂ sequence, ErdősSidon set | Standard combinatorial object; SilverSight uses it for deterministic strand addressing. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical #core | [Sidon label](#sidon-label), [IsIntervalSidon](#isintervalsidon) |
| **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) | | **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) | | **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), [ofFloat](#offloat) |
| **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) | | **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), [crossStep](#crossstep) |
| **eigensolid** | Fixed point, attractor | Fixed point of the crossStep operator; not a physical solid. | formal/CoreFormalism/BraidEigensolid.lean:L42 | #mathematical #core | [crossStep](#crossstep) | | **eigensolid** | Fixed point, attractor | Fixed point of the crossStep operator; not a physical solid. | formal/CoreFormalism/BraidEigensolid.lean:L42 | #mathematical #core | [crossStep](#crossstep), [BraidStorm](#braidstorm) |
| **crossStep** | Braid generator / crossing operator | One deterministic update step in the braid dynamics. | formal/CoreFormalism/BraidCross.lean:L1 | #mathematical #core | [eigensolid](#eigensolid) | | **crossStep** | Braid generator / crossing operator | One deterministic update step in the braid dynamics. | formal/CoreFormalism/BraidCross.lean:L1 | #mathematical #core | [eigensolid](#eigensolid), [BraidStorm](#braidstorm) |
| **AVM** | Abstract/virtual machine, stack machine | SilverSight-specific instruction set and transition relation. | Core/SilverSightCore.lean:L1 | #core #implementation | [TIC](#tic) | | **AVM** | Abstract/virtual machine, stack machine | SilverSight-specific instruction set and transition relation. | Core/SilverSightCore.lean:L1 | #core #implementation | [TIC](#tic), [AvmTy](#avmty) |
| **TIC** | Logical clock, event counter | Monotone counter derived from AVM transitions. | Core/SilverSightCore.lean:L1 | #core #implementation | [AVM](#avm) | | **TIC** | Logical clock, event counter | Monotone counter derived from AVM transitions. | Core/SilverSightCore.lean:L1 | #core #implementation | [AVM](#avm) |
| **Receipt** | Attestation, certificate, proof certificate | Machine-readable record of a gate result; the compressed state. | Core/SilverSightCore.lean:L1 | #core #protocol | [FixtureRow](#fixturerow), [emit](#emit) |
| **Hachimoji** | 8-letter alphabet, octal state | The 8-symbol output alphabet of the core classifier. | formal/CoreFormalism/HachimojiLUT.lean:L1 | #core #mathematical | [Hachimoji state](#hachimoji-state) |
| **Finsler-Randers** | Asymmetric metric, quasimetric | Directed routing cost with anisotropy parameter beta. | qubo/finsler_metric.py:L1 | #mathematical #planned | [QUBO](#qubo) |
| **QUBO** | Ising model, binary quadratic optimization | Energy minimization over binary variables. | qubo/qubo_builder.py:L1 | #mathematical #planned | [Finsler-Randers](#finsler-randers) |
| **meta-solid** | Topological triple point, phase coexistence | Point where three independent equivalence relations collapse. | formal/CoreFormalism/BraidEigensolid.lean:L1 | #mathematical | [eigensolid](#eigensolid) |
| **promotion** | Certification, acceptance | Status advance only after a formal gate passes. | AGENTS.md:L1 | #protocol | [quarantine](#quarantine) |
| **quarantine** | Archive, staging, broken build exclusion | Module kept out of the active build until repaired. | AGENTS.md:L1 | #protocol | [promotion](#promotion) |
| **Genome18** | Codon LUT, k=6 fixed-point address | Research Stack vocabulary-lock name for CodonLUT (k=6): 6 x 3-bit Hachimoji inputs -> 18-bit address. SilverSight binds this to formal/CoreFormalism/HachimojiLUT.lean CodonLUT. | formal/CoreFormalism/HachimojiLUT.lean:L1 | #mathematical | [CodonLUT](#codonlut) |
| **equationPosition** | Manifold localization, equation embedding | The deterministic map EquationShape -> SpherePoint that answers where does this equation live on the manifold? | formal/CoreFormalism/HachimojiLUT.lean:L4 | #mathematical | [SpherePoint](#spherepoint) |
--- ---
@ -29,10 +38,91 @@ SilverSight invents names only when necessary. When a concept already exists und
| Term | Definition | File:Line | Tags | See Also | | 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) | | **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) | | **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: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) | | **AVM** | Adaptive Virtual Machine. The stack-machine transition semantics delta defined in the core; the universal bridge between math languages and executable traces. | Core/SilverSightCore.lean:L1 | #core #implementation | [TIC](#tic), [AvmTy](#avmty) |
| **TIC** | Temporal Index of Computation. A monotone event counter derived from AVM state transitions. | Core/SilverSightCore.lean:L1 | #core #implementation | [AVM](#avm) | | **TIC** | Temporal Index of Computation. A monotone event counter derived from AVM state transitions. | Core/SilverSightCore.lean:L1 | #core #implementation | [AVM](#avm) |
| **pathCost** | Raw integer cost metric carried on a Receipt; never a Float. | Core/SilverSightCore.lean:L1 | #core | [Receipt](#receipt) |
| **Library method** | The architecture rule: Core/ defines contracts, libraries implement them, and no library imports another library. | AGENTS.md:L1 | #protocol | [Core](#core) |
| **Core** | The invariant center of SilverSight: Core/SilverSightCore.lean and Core/SilverSight/FixedPoint.lean. Defines Receipt, AVM, TIC, and canonical Q16_16. | AGENTS.md:L1 | #core | [Library method](#library-method) |
| **Schema** | Typeclass describing fixed-size, well-formed data: byteSize and wellFormed. | Core/SilverSight/Semantics/Schema.lean:L1 | #core #implementation | [byteSize](#bytesize), [wellFormed](#wellformed) |
| **byteSize** | Number of bytes occupied by a value of a Schema type; constant and statically known. | Core/SilverSight/Semantics/Schema.lean:L1 | #core #implementation | [Schema](#schema) |
| **wellFormed** | Predicate asserting that a value satisfies its Schema invariants. | Core/SilverSight/Semantics/Schema.lean:L1 | #core #implementation | [Schema](#schema) |
| **Layout** | Physical data placement: rowMajor, columnar, compact, mmapView. | Core/SilverSight/Semantics/Layout.lean:L1 | #core #implementation | [AccessProfile](#accessprofile), [rowMajor](#rowmajor) |
| **AccessProfile** | Read/write mix used by the layout cost model. | Core/SilverSight/Semantics/Layout.lean:L1 | #core #implementation | [Layout](#layout) |
| **WireFormat** | Certified encoder/decoder pair for a Schema under a Layout. | Core/SilverSight/Semantics/WireFormat.lean:L1 | #core #implementation | [roundTrip](#roundtrip) |
| **roundTrip** | WireFormat axiom: decode (encode a) = some a for every value. | Core/SilverSight/Semantics/WireFormat.lean:L1 | #core #protocol | [WireFormat](#wireformat) |
| **View** | Zero-copy, address-bounded window into a ByteArray. | Core/SilverSight/Semantics/View.lean:L1 | #core #implementation | [LayoutBridge](#layoutbridge) |
| **LayoutBridge** | Certified conversion between two Layouts with a round-trip guarantee. | Core/SilverSight/Semantics/LayoutBridge.lean:L1 | #core #implementation | [Layout](#layout), [View](#view) |
| **CanalRegime** | Storage regime (cold, warm, hot, flash) used by layout selection. | Core/SilverSight/Semantics/CanalLayout.lean:L1 | #core #implementation | [CanalLayout](#canallayout) |
| **CanalLayout** | Module that maps CanalRegime to a preferred Layout and profile. | Core/SilverSight/Semantics/CanalLayout.lean:L1 | #core #implementation | [CanalRegime](#canalregime) |
| **rowMajor** | Default Layout: fields stored contiguously in declaration order. | Core/SilverSight/Semantics/Layout.lean:L1 | #core #implementation | [Layout](#layout) |
| **mmapView** | Layout optimized for memory-mapped, read-only access. | Core/SilverSight/Semantics/Layout.lean:L1 | #core #implementation | [Layout](#layout) |
| **BraidState** | Aggregated braid carrier state used by the eigensolid compressor. | formal/CoreFormalism/BraidState.lean:L1 | #mathematical #core | [BraidStorm](#braidstorm) |
---
## RRC / AVM ISA
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **RRC** | Receipt Routing Classifier. Aligns PIST structural labels with RRC semantic routing shapes and emits gate receipts. | formal/SilverSight/RRC/Emit.lean:L1 | #core #protocol | [RRCShape](#rrcshape), [FixtureRow](#fixturerow) |
| **CoreFormalism** | The SilverSight foundational library containing canonical Q16_16, Sidon sets, braid dynamics, and related lemmas. | formal/CoreFormalism/:L1 | #core #mathematical | [SidonSets](#sidonsets) |
| **RRCShape** | One of six lawful routing shapes: cognitiveLoadField, signalShapedRouteCompiler, logogramProjection, projectableGeometryTopology, cadForceProbeReceipt, holdForUnlawfulOrUnderspecifiedShape. | formal/SilverSight/RRCLogogramProjection.lean:L1 | #core #protocol | [WitnessStatus](#witnessstatus) |
| **WitnessStatus** | candidate (admits next-stage checks) or hold (blocked pending more evidence). | formal/SilverSight/RRCLogogramProjection.lean:L1 | #protocol | [RRCShape](#rrcshape) |
| **LogogramReceipt** | Receipt core for one compiled logogram projection, carrying shape, status, regime, and tear evidence. | formal/SilverSight/RRCLogogramProjection.lean:L1 | #core #protocol | [RRCShape](#rrcshape) |
| **FixtureRow** | One compiled equation record with raw features and optional PIST labels; input to the RRC alignment gate. | formal/SilverSight/RRC/Emit.lean:L1 | #core | [AlignmentStatus](#alignmentstatus) |
| **AlignmentStatus** | Result of determineAlignment: alignedExact, alignedProxy, compatibleStructuralProjection, alignmentWarning, or missingPrediction. | formal/SilverSight/RRC/Emit.lean:L1 | #protocol | [FixtureRow](#fixturerow) |
| **determineAlignment** | RRC alignment gate that maps a FixtureRow and optional PIST labels to an AlignmentStatus. | formal/SilverSight/RRC/Emit.lean:L1 | #protocol | [FixtureRow](#fixturerow) |
| **AvmTy** | Closed-world AVM type universe: q0_16, q16_16, bool. | formal/SilverSight/AVMIsa/Types.lean:L1 | #core #implementation | [AvmVal](#avmval) |
| **AvmVal** | Typed AVM value payload indexed by AvmTy. | formal/SilverSight/AVMIsa/Value.lean:L1 | #core #implementation | [AvmTy](#avmty) |
| **Instr** | AVM instruction set: push, pop, dup, swap, load, store, jump, jumpIf, prim, halt. | formal/SilverSight/AVMIsa/Instr.lean:L1 | #core #implementation | [Prim](#prim) |
| **Prim** | Finite AVM primitive set: boolean ops and saturating Q0_16/Q16_16 add/sub. | formal/SilverSight/AVMIsa/Instr.lean:L1 | #core #implementation | [Instr](#instr) |
| **AVMIsa.Emit** | Top-level JSON output boundary. Stamps AVM canary receipts and RRC corpus bundles. | formal/SilverSight/AVMIsa/Emit.lean:L1 | #core #protocol | [RRC](#rrc) |
| **TDoku16D** | Projected gradient descent constraint propagation on the 16D subspace. | formal/SilverSight/PIST/Tdoku16D.lean:L1 | #mathematical | [Q16_16](#q16_16) |
| **CrossDomainSynthesis** | Enclosure and defect proof boundaries validating critical ratios. | formal/SilverSight/PIST/CrossDomainSynthesis.lean:L1 | #mathematical | [MultiSurfacePacker](#multisurfacepacker) |
| **MultiSurfacePacker** | Multi-surface Lagrangian optimization decision logic. | formal/SilverSight/PIST/MultiSurfacePacker.lean:L1 | #mathematical | [CrossDomainSynthesis](#crossdomainsynthesis) |
---
## Fixed-point and Numerics
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **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:L1 | #core #implementation | [Q0_16](#q0_16), [ofFloat](#offloat) |
| **Q0_16** | 16.16-style fixed-point interpretation used for bounded unit-interval quantities. | Core/SilverSight/FixedPoint.lean:L1 | #core #implementation | [Q16_16](#q16_16) |
| **ofFloat** | Conversion from Float to Q16_16. Permitted only at external boundaries (JSON parsing, sensor input); must be immediately bracketed. | AGENTS.md:L1 | #protocol #implementation | [Q16_16](#q16_16), [Float](#float) |
| **ofNat / ofRatio / ofRawInt** | Canonical constructors for Q16_16 values in compute paths. | Core/SilverSight/FixedPoint.lean:L1 | #core #implementation | [Q16_16](#q16_16) |
| **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:L1 | #protocol #deprecated | [ofFloat](#offloat) |
---
## Braid / Eigensolid Compression
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **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:L1 | #mathematical #core | [eigensolid](#eigensolid), [crossStep](#crossstep) |
| **eigensolid** | The converged, stable state of a braid crossing loop; detected when crossStep(s) = s. | formal/CoreFormalism/BraidEigensolid.lean:L42 | #mathematical #core | [crossStep](#crossstep), [BraidStorm](#braidstorm) |
| **crossStep** | One braid-crossing iteration that merges phase and emits a residual. | formal/CoreFormalism/BraidCross.lean:L1 | #mathematical #core | [eigensolid](#eigensolid), [BraidStorm](#braidstorm) |
| **strand** | A single braided carrier with phase accumulator, parity, slot, residue, jitter, and admissibility bracket. | formal/CoreFormalism/BraidStrand.lean:L1 | #mathematical #core | [BraidStorm](#braidstorm) |
| **Yang-Baxter** | The braid relation that defines braid-order invariance. | formal/CoreFormalism/BraidEigensolid.lean:L1 | #mathematical | [BraidStorm](#braidstorm) |
---
## Sidon / Number Theory
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **Sidon set** | A set where all pairwise sums a + b are unique up to reordering. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical #core | [Sidon label](#sidon-label) |
| **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:L1 | #mathematical #core | [Sidon set](#sidon-set) |
| **Sidon slack** | Address budget minus the maximum label used; encodes capacity headroom. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical | [Sidon set](#sidon-set) |
| **IsIntervalSidon** | Predicate stating that a finite set is a Sidon subset of {1,...,N}. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical | [Sidon set](#sidon-set) |
| **IsSidonMod** | Predicate stating that a set is Sidon modulo M: sums are unique up to congruence. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical | [Sidon set](#sidon-set) |
| **sidonMaximum** | Extremal function h(N) returning the maximum size of an interval Sidon set. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical | [Sidon set](#sidon-set) |
| **Singer theorem** | Existence of a Sidon set of size q+1 modulo q^2+q+1 for prime powers q. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical | [Sidon set](#sidon-set) |
| **Lindstrom bound** | Upper bound for interval Sidon sets. | formal/CoreFormalism/SidonSets.lean:L1 | #mathematical | [Sidon set](#sidon-set) |
| **interaction graph** | Typed directed graph whose adjacency matrix is tested for the Sidon witness property. | formal/CoreFormalism/InteractionGraphSidon.lean:L1 | #mathematical | [Sidon label](#sidon-label) |
| **weak-axis CRT** | Chinese Remainder Theorem reconstruction used for RRC weak-axis classification. | formal/CoreFormalism/SieveLemmas.lean:L1 | #mathematical | [SieveLemmas](#sievelemmas) |
--- ---
@ -42,10 +132,55 @@ SilverSight invents names only when necessary. When a concept already exists und
2. Make the File:Line column point at the exact file and line number 2. Make the File:Line column point at the exact file and line number
3. Add relevant Tags for categorization 3. Add relevant Tags for categorization
4. Add See Also links to related terms using #anchor format 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 5. If the term has a standard name, add it to the Standard Terminology Crosswalk
6. If the term is used in a receipt or gate, ensure the source module proves the property
7. Run python3 -m py_compile on any touched Python and lake build on any touched Lean
--- ---
## Deep Wiki Integration ## Deep Wiki Integration
All terms are indexed by term name, file path, tags, and cross-references for deep wiki compatibility. All terms are indexed by term name, file path, tags, and cross-references for deep wiki compatibility.
---
## Spiral Packing & Layout
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **Integer Spiral Packing** | Corpus-wide packing of signed coefficients using base 328,469 with offset 164,234. Unpack inverts exactly, round-trip verified over all 250 matrices. | python/spectral_codebook.py:L1 | #implementation #mathematical | [phi_corkscrew_index](#phi_corkscrew_index) |
| **phi_corkscrew_index** | Index function for corkscrew packing. Previously not injective ((-1,1) and (1,0) both gave 1 in base 2). Fixed upstream. | python/phi_corkscrew.py:L1 | #mathematical | [Integer Spiral Packing](#integer-spiral-packing) |
---
## f(n) Layout (Decorative)
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **f(n) layout** | Decorative layout where each entry gets radius_sq and angle_frac. Computed in decimal because indices reach ~10^44 where float64 keeps zero fractional bits. | python/f_layout.py:L1 | #implementation #mathematical | [radius_sq](#radius_sq), [angle_frac](#angle_frac) |
| **radius_sq** | Spiral index value in f(n) layout, representing squared radius. | python/f_layout.py:L1 | #mathematical | [f(n) layout](#fn-layout) |
| **angle_frac** | Angular fraction in f(n) layout, computed in decimal for precision. Min angular separation ≈ 4.6×10^-6 of a turn. | python/f_layout.py:L1 | #mathematical | [f(n) layout](#fn-layout) |
---
## Cartan Floor & Fingerprints
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **Cartan Δ-floor** | Floor parameter Δ = 17/1792 exact (CartanConnection.lean:70). Used for Fisher version on Δ_7. | formal/SilverSight/PIST/CartanConnection.lean:L70 | #mathematical #core | [Fisher version](#fisher-version), [Δ_7](#δ_7) |
| **Fisher version** | Fisher version on Δ_7 with Cartan Δ-floor. 13 fingerprint pairs fall below Δ, merging 196 fingerprints into 187 Δ-resolution codewords. | python/spectral_codebook.py:L1 | #implementation #mathematical | [Cartan Δ-floor](#cartan-Δ-floor) |
| **Δ_7** | 7-dimensional simplex with Fisher-Rao metric. Cartan connection defined on J¹(Δ_7). | formal/SilverSight/PIST/CartanConnection.lean:L1 | #mathematical | [Cartan Δ-floor](#cartan-Δ-floor) |
| **fingerprint** | Characteristic polynomial coefficients as unique identifier. 196 unique fingerprints across 250 matrices. | python/charpoly_codebook.py:L1 | #mathematical | [codeword](#codeword), [Cartan Δ-floor](#cartan-Δ-floor) |
| **codeword** | Δ-resolution codeword after applying Cartan floor. 187 codewords from 196 fingerprints. | python/spectral_codebook.py:L1 | #mathematical | [fingerprint](#fingerprint) |
---
## Torus Winding
| Term | Definition | File:Line | Tags | See Also |
|------|------------|-----------|------|----------|
| **TorusWinding** | Winding data structure carrying a_exact/b_exact (plain ). Supersedes _safe variant which only detected saturation. | python/torus_winding.py:L1 | #implementation #mathematical | [a_exact](#a_exact), [torus_to_spiral_index](#torus_to_spiral_index) |
| **a_exact** | Exact integer parameter in TorusWinding, enables lossless round trips. | python/torus_winding.py:L1 | #implementation | [TorusWinding](#toruswinding) |
| **b_exact** | Exact integer parameter in TorusWinding, enables lossless round trips. | python/torus_winding.py:L1 | #implementation | [TorusWinding](#toruswinding) |
| **torus_to_spiral_index** | Function mapping torus winding to spiral index. Prefers a_exact/b_exact for lossless round trips. Regression-tested at n = 10^9. | python/torus_winding.py:L1 | #implementation #mathematical | [TorusWinding](#toruswinding) |