diff --git a/CITATION.cff b/CITATION.cff index 7aa9bd21..5f6dc52c 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -1,15 +1,30 @@ 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 -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: - family-names: "Schneider" given-names: "Brandon" 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" url: "https://github.com/allaunthefox/SilverSight" date-released: "2026-06-21" -license: MIT +license: Apache-2.0 +commit: "4abd17ffeba2593767ecfc7ca82711de2a2eb921" + references: - type: article @@ -18,6 +33,7 @@ references: - family-names: "Imaginary" given-names: "ICERM" 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." - type: software @@ -29,20 +45,21 @@ references: repository-code: "https://github.com/allaunthefox/Research-Stack" url: "https://github.com/allaunthefox/Research-Stack" date-released: "2026-05-08" - 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" + license: Apache-2.0 + notes: "Parent research repository. SilverSight ports proven Lean modules (Semantics.FixedPoint, Semantics.SidonSets, Semantics.SieveLemmas, Semantics.InteractionGraphSidon, Semantics.BraidEigensolid, Semantics.BraidSpherionBridge)." - type: software - title: "GP_ELITE: Régression symbolique par programmation génétique" + title: "GP_ELITE: Regression symbolique par programmation genetique" authors: - name: "Sabri Hakou" version: "0.1.0" date-released: "2026-06-13" - license: "MIT" + license: MIT 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 + title: "Photon-Varied Gaussian States" authors: - family-names: "Giani" given-names: "A." @@ -50,39 +67,38 @@ references: given-names: "S." - family-names: "Conti" given-names: "C." - title: "Photon-Varied Gaussian States" - year: "2025" - notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; preprint identifier pending confirmation." + year: 2025 + notes: "Binds to Research Stack Semantics.PVGS_DQ_Bridge -> SilverSight formal/PVGS_DQ_Bridge/; preprint identifier pending confirmation." - type: unpublished + title: "Stellar representation of non-Gaussian quantum states" authors: - family-names: "Chabaud" given-names: "U." - family-names: "Mehraban" given-names: "S." - title: "Stellar representation of non-Gaussian quantum states" - year: "2022" - notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; full citation details pending DOI or arXiv ID." + year: 2022 + notes: "Binds to Research Stack Semantics.PVGS_DQ_Bridge -> SilverSight formal/PVGS_DQ_Bridge/; full citation details pending DOI or arXiv ID." - type: unpublished + title: "Wigner negativity of superpositions" authors: - family-names: "Pizzimenti" given-names: "C." - - family-names: "et al." - title: "Wigner negativity of superpositions" - year: "2024" - notes: "Binds to Research Stack `Semantics.BindingSite` / `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/BindingSite/`; full citation details pending DOI or arXiv ID." + - literal: "et al." + year: 2024 + notes: "Binds to Research Stack Semantics.BindingSite / Semantics.PVGS_DQ_Bridge -> SilverSight formal/BindingSite/; full citation details pending DOI or arXiv ID." - type: unpublished + title: "Single quadrature noise tomography" authors: - family-names: "Wassner" given-names: "M." - - family-names: "et al." - title: "Single quadrature noise tomography" - year: "2025" - notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; full citation details pending DOI or arXiv ID." + - literal: "et al." + year: 2025 + 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" authors: - family-names: "Saucedo" @@ -92,7 +108,7 @@ references: name: "California State University, San Bernardino" collection-title: "Electronic Theses, Projects, and Dissertations" 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 title: "Close packing density of polydisperse hard spheres" @@ -104,7 +120,7 @@ references: date-published: "2009-12" doi: "10.1063/1.3276799" 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 title: "Fractionation effects in phase equilibria of polydisperse hard-sphere colloids" @@ -116,7 +132,7 @@ references: date-published: "2004-10" doi: "10.1103/physreve.70.041410" 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 title: "Random-close packing limits for monodisperse and polydisperse hard spheres" @@ -128,7 +144,7 @@ references: date-published: "2014" doi: "10.1039/c3sm52959b" 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 title: "Freezing of polydisperse hard spheres" @@ -140,7 +156,7 @@ references: date-published: "1999" doi: "10.1103/physreve.59.618" 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 title: "A Differentiable Interior-Point Method in Single Precision" @@ -153,7 +169,7 @@ references: given-names: "Zachary" date-published: "2026-05" 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 title: "Everything Is Logarithms" @@ -162,7 +178,7 @@ references: given-names: "Alex" date-published: "2026-05-25" 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 title: "Stabilizing Recurrent Dynamics for Test-Time Scalable Latent Reasoning in Looped Language Models" @@ -183,17 +199,15 @@ references: given-names: "Yu-Feng" date-published: "2026-05" 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 title: "Tangent lines to parabola at ends of focal chord are perpendicular (calculus proof)" authors: - - family-names: "Unknown" + - literal: "Unknown" date-published: "2025" 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." - -# ── Implemented references ported from Research Stack ────────────── + notes: "Demonstrates focal chord perpendicularity. Maps to Hachimoji eigensolid conjugate pairs with 1/n scaling." - type: article title: "Brownian dynamics of polydisperse colloidal hard spheres: Equilibrium structures and random close packings" @@ -224,7 +238,7 @@ references: authors: - family-names: "Santiso" given-names: "E." - - family-names: "Müller" + - family-names: "Muller" given-names: "E. A." date-published: "2002" doi: "10.1080/00268970210125313" @@ -234,7 +248,7 @@ references: - type: article title: "Freezing line of polydisperse hard spheres via direct-coexistence simulations" authors: - - family-names: "Castagnède" + - family-names: "Castagnede" given-names: "A." - family-names: "Filion" given-names: "L." @@ -257,7 +271,6 @@ references: - family-names: "Zia" given-names: "R." date-published: "2025" - doi: "10.1017/jfm.2026.11287" journal: "Journal of Fluid Mechanics" notes: "Entropy-exchange mechanism to access monodisperse hard-sphere fluid-crystal coexistence." @@ -282,7 +295,7 @@ references: authors: - family-names: "De Jager" given-names: "M." - - family-names: "Castagnède" + - family-names: "Castagnede" given-names: "A." - family-names: "Smallenburg" given-names: "F." @@ -297,8 +310,8 @@ references: authors: - family-names: "Cantor" given-names: "D." - - family-names: "Azéma" - given-names: "É." + - family-names: "Azema" + given-names: "E." - family-names: "Sornay" given-names: "P." - family-names: "Radjai" @@ -346,553 +359,3 @@ references: institution: name: "University of Twente" 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(As1−xPx)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." diff --git a/WORK_LOG.md b/WORK_LOG.md index ff9941d3..8fef853b 100644 --- a/WORK_LOG.md +++ b/WORK_LOG.md @@ -61,3 +61,52 @@ Standalone formula for the hardest Layer 3 conjecture: a Cartan connection of ty --- ## 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 diff --git a/docs/GLOSSARY.md b/docs/GLOSSARY.md index dd366f2d..e1327d0b 100644 --- a/docs/GLOSSARY.md +++ b/docs/GLOSSARY.md @@ -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 | |------------------|----------------------|--------------|-----------|------|----------| -| **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 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), [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) | -| **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) | +| **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), [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), [BraidStorm](#braidstorm) | +| **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) | +| **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 | |------|------------|-----------|------|----------| -| **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) | +| **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. 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 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) | +| **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 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 +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 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) |