mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00

allaun 670e7617c3 refactor(rrc): rename corpus250→allFixtures/emitManifold, generic n-dimensional modules, Authentik deploy

- Rename python/build_corpus250.py → python/build_manifold.py
- Rename emitCorpus250 → emitManifold, corpus250 → allFixtures
- Schema: avm_rrc_corpus250_v1 → avm_rrc_manifold_v1
- Classify.lean now delegates to ClassifyN (generic n-dim module)
- ClassifyN.hashTable8: extracted 119-entry hash table from old Classify
- build_manifold.py now emits ClassifyN.classifyProxy hashTable8 + classifyExact 8
- build_pist_matrices_250.py: added pistMatrixDim constant
- SilverSight docs/AGENTS.md updated for renames
- Research Stack AGENTS.md updated for toolchain references
- Authentik deployed on neon-64gb (port 30001, working)
- cross_domain_significance.py: statistical significance test (all phases <6σ with n=3)
- setup_authentik.sh: fixed image, password, port, key sharing

Build: 3307 jobs, 0 errors (lake build)

2026-06-30 04:54:40 -05:00

22 KiB

Raw Permalink Blame History

SilverSight Porting Map

Source: Research-Stack (/home/allaun/Research Stack)
Target: SilverSight (https://github.com/allaunthefox/SilverSight)
Goal: Move only what is proven, active, and compatible with the library-method architecture.

Searchable inventory: docs/research_stack_usage_graph.json / .md / .dot — a point graph of all 849 Semantics modules, 3,175 theorems, 7,784 defs, 215 scripts, 1,235 docs, services, databases, nodes, skills, and goals.
Porting shortlist: docs/research_stack_porting_candidates.md — ranked by theorem count, in-degree, definitions, and sorry count.

1. Current SilverSight State

SilverSight already has a clean skeleton built around the 5-layer conceptual map:

Core/
  SilverSightCore.lean          ← 200-line invariant core
formal/
  CoreFormalism/                ← Chentsov, Hachimoji, Q16_16
  PVGS_DQ_Bridge/               ← 7 sections + master bridge
  UniversalEncoding/            ← 50-token math address space
  BindingSite/                  ← amino-acid / protein binding sketches
python/
  chaos_game.py
  sidon_address.py
  spectral_profile.py
  q16_canonical.py
qubo/
  finsler_metric.py
  qubo_builder.py
  qaoa_circuit.py
  classical_solver.py
tests/
  q16_roundtrip_test.py
docs/
  ARCHITECTURE.md
  LIBRARY_MANIFEST.md
  RRC_PLACEMENT.md
REBASE_RULES.md                 ← seed ruleset from Research-Stack

2. Research-Stack Source Inventory

The source tree is large (~9,600 objects, ~1,300 Lean files). Most of it is exploratory or extracted to other repos. The durable, proven subset lives in:

Area	What matters
`0-Core-Formalism/lean/Semantics/Semantics/`	Proven Lean modules: FixedPoint, SidonSets, SieveLemmas, InteractionGraphSidon, BraidEigensolid, BraidSpherionBridge, AVMIsa.*, RRC.Emit/Q16_16Manifold, TransportQUBOBridge, ChentsovBridge.
`4-Infrastructure/shim/`	Python shims: qaoa_adapter.py, qubo_highs.py, benchmark_finsler_qap.py, chaos_game_16d.py, sidon_generation_kernel.py, geometric_entropy_explorer.py, candidate_certification_bridge.py, stack_solidification_audit.py.
`6-Documentation/docs/`	AGENTS.md strict rules, architecture specs, distilled notes, specs (DP-RRC, Virtio-Net compute, etc.).
`5-Applications/text-to-cad/`	CAD/URDF harness and skills.
`scripts/qc-flag/`	Lean QC flagger protocol.
`.devin/skills/lean-proof/SKILL.md`	Mandatory proof-quality skill.
`.github/skills/contextstream-workflow/SKILL.md`	Persistent memory workflow.
`.github/skills/research-stack-workflow/SKILL.md`	Token-efficient proof workflow.
`.cursorrules`, `.devin/`, `.claude/`, `.roo/`, `.kilo/`, `.windsurf/`	Editor/agent hook configs that enforce ContextStream-first rules.

3. Porting Matrix

Legend

Status	Meaning
✅ PORTED	Already exists in SilverSight in compatible form.
🟡 PORT	Proven/active in Research-Stack; should move to SilverSight as-is or with minimal renaming.
🟠 ADAPT	Concept survives, but implementation must be refactored for the library-method architecture.
🔴 DROP	Quarantined, hairy, extracted to other repos, or superseded by SilverSight design.

Core Layer

Research-Stack	SilverSight Target	Status	Notes
`Semantics.FixedPoint.lean`	`formal/CoreFormalism/FixedPoint.lean`	✅ PORTED	Full FixedPoint module with Q0_16/Q16_16 inverse trig, clamping, and determinism theorems. Replaced the thin `Q16_16_Spec.lean`.
`Semantics.Q16InverseProof.lean`	`formal/CoreFormalism/FixedPoint.lean`	✅ PORTED	Absorbed into `FixedPoint.lean`; inverse-proof machinery for bounded KKT systems and no-Float Q16_16 boundaries.
`Semantics.SidonSets.lean`	`formal/CoreFormalism/SidonSets.lean`	✅ PORTED	Builds (`lake build CoreFormalism.SidonSets`). Core Sidon definitions, extremal bounds, and Singer construction. Chaos-game appendix dropped.
`Semantics.InteractionGraphSidon.lean`	`formal/CoreFormalism/InteractionGraphSidon.lean`	✅ PORTED	Typed interaction graphs, bounded Sidon witness, RRC weak-axis CRT reconstruction. No Float.
`Semantics.SieveLemmas.lean`	`formal/CoreFormalism/SieveLemmas.lean`	✅ PORTED	Coprime-sieve observers, CRT reconstruction, executable human/dolphin witness. No Float.
`Semantics.ChentsovBridge.lean`	`formal/CoreFormalism/ChentsovFinite.lean`	✅ PORTED	Already present; keep the finite n=8 proof as the core theorem.
`Semantics.TransportQUBOBridge.lean`	`QUBOLib/` or `MetricLib/`	🟡 PORT	Finsler → QUBO bridge; 0 sorries, 2 axioms with TODO(lean-port). Clean fit.

LexLib / MathLib Layer

Research-Stack	SilverSight Target	Status	Notes
`UniversalMathEncoding.lean`	`formal/UniversalEncoding/UniversalMathEncoding.lean`	✅ PORTED	Already exists. Needs LaTeX parser (`expressionToReceipt`) completed.
`ChiralitySpace.lean`	`formal/UniversalEncoding/ChiralitySpace.lean`	✅ PORTED	Already exists.
`math_symbols.py`, `build_math_symbols_db.py`	`python/`	🟡 PORT	Token vocabulary builder for the 50-token address space.
`equation_shape_parser.py`	`python/`	🟡 PORT	Parses equation strings into structural features.

SearchLib Layer

Research-Stack	SilverSight Target	Status	Notes
`python/chaos_game_16d.py`	`python/chaos_game.py`	🟠 ADAPT	16D chaos game engine. Port logic but strip Research-Stack hair (VCN refs, etc.).
`python/sidon_generation_kernel.py`	`python/sidon_address.py`	🟠 ADAPT	Sidon label generation. Merge into existing `sidon_address.py`.
`python/geometric_entropy_explorer.py`	`python/spectral_profile.py`	🟠 ADAPT	Entropy-exploration candidate generator. Use as basis for `SearchLib` basin exploration.
`python/candidate_certification_bridge.py`	`python/`	🟠 ADAPT	Generates `Candidates.lean` from entropy exploration. Refactor to produce SilverSight receipts.
`Semantics.BraidEigensolid.lean`	`formal/CoreFormalism/BraidEigensolid.lean`	✅ PORTED	Namespace `SilverSight.BraidEigensolid`. Builds: `lake build CoreFormalism.BraidEigensolid` (2986 jobs, 0 errors). Minor proof adaptations for `Q16_16.toInt`/coercion and `PhaseVec.add` zero-fast-path.
`Semantics.BraidSpherionBridge.lean`	`formal/CoreFormalism/BraidSpherionBridge.lean`	✅ PORTED	Namespace `SilverSight.BraidSpherionBridge`. Dependency chain (Tactics, Q16_16Numerics, DynamicCanal, Bind, BraidBracket, BraidStrand, BraidCross, BraidField) added to `lakefile.lean` roots. Builds: `lake build CoreFormalism.BraidSpherionBridge` (2989 jobs, 0 errors).
`Semantics.AntiBraidStorm.lean`	`SearchLib/`	🟡 PORT	Adversarial verification for receipt aliasing.
`Semantics.BaselineComparison.lean`	`SearchLib/`	🟡 PORT	Comparative baseline fixtures for eigensolid/meta-solid packing-bound claims.

StructureLib Layer

Research-Stack	SilverSight Target	Status	Notes
`formal/UniversalEncoding/ChiralitySpace.lean`	`StructureLib/`	✅ PORTED	Already present.
`formal/BindingSite/BindingSiteTypes.lean`	`formal/BindingSite/BindingSiteTypes.lean`	✅ PORTED	All compute fields Q16_16 (no Float). Registered in SilverSightFormal. 2026-06-25.
`formal/BindingSite/BindingSiteHachimoji.lean`	`formal/BindingSite/BindingSiteHachimoji.lean`	✅ PORTED	ChentsovFinite dep removed; `buildProfile` in Q16_16; no sorry. Registered. 2026-06-25.
`formal/BindingSite/BindingSiteCodec.lean`	`formal/BindingSite/BindingSiteCodec.lean`	✅ PORTED	Rewrote: dropped PVGS Bridge dep (Core/Bridge Q16_16 type collision resolved); `dqEnergy`/`stellarRank` computed from entropy profile; `stellarRank_le_8` + `dqEnergy_empty` theorems proved. Registered. 2026-06-25.
`formal/BindingSite/BindingSiteEntropy.lean`	`formal/BindingSite/BindingSiteEntropy.lean`	🟠 ADAPT	§1-§4 Q16_16 (registered via BindingSiteHachimoji dep-chain). §5 `fisher_implies_similar_druggability` has sorry — blocked on `entropy_lipschitz` axiom (research-level Pinsker inequality). Not registered directly until §5 resolved. 2026-06-25.

MetricLib Layer

Research-Stack	SilverSight Target	Status	Notes
`4-Infrastructure/shim/qaoa_adapter.py`	`qubo/finsler_metric.py` / `qubo/qubo_builder.py`	🟠 ADAPT	2,421-line QUBO ↔ Ising ↔ Pauli bridge. Split into MetricLib + QUBOLib pieces.
`4-Infrastructure/shim/benchmark_finsler_qap.py`	`qubo/test_optimize.py`	🟠 ADAPT	Finsler-Randers QAP benchmark. Use as validation suite.
`4-Infrastructure/shim/benchmark_finsler_qaoa.py`	`qubo/test_optimize.py`	🟠 ADAPT	Finsler-QAOA benchmark. Use as validation suite.
`Semantics.TransportTheory` / `Semantics.ChentsovBridge`	`MetricLib/`	🟡 PORT	Finsler metric + Chentsov theorem formalisms.

QUBOLib Layer

Research-Stack	SilverSight Target	Status	Notes
`4-Infrastructure/shim/qaoa_adapter.py`	`qubo/qaoa_circuit.py` / `qubo/qubo_builder.py`	🟠 ADAPT	Split: QUBO builder stays in QUBOLib; Finsler metric moves to MetricLib.
`4-Infrastructure/shim/qubo_highs.py`	`qubo/classical_solver.py`	🟠 ADAPT	HiGHS MIP bridge and TSP assignment relaxation. Merge into `classical_solver.py`.
`4-Infrastructure/shim/pist_matrix_builder.py`	`python/`	🟡 PORT	250-equation PIST matrix builder; produces deterministic 8×8 strand adjacency.
`4-Infrastructure/shim/build_corpus250.py`	`python/build_manifold.py`	🟠 ADAPT	Generates RRC manifold rows. Refactored from `build_corpus250.py`; emits `allFixtures`.

PVGSLib Layer

Research-Stack	SilverSight Target	Status	Notes
`formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean` + sections	`formal/PVGS_DQ_Bridge/`	✅ PORTED	Already present. Still has `sorry`s to close.
`Semantics.EffectiveBoundDQ.lean`	`PVGSLib/`	🟡 PORT	DualQuaternion effective bounds; dependency for bridge.
`Semantics.DualQuaternion.lean` (if exists)	`PVGSLib/`	🟡 PORT	Required by EffectiveBoundDQ.

EventLib Layer

Research-Stack	SilverSight Target	Status	Notes
`SilverSightCore.lean` TIC axiom	`Core/SilverSightCore.lean`	✅ PORTED	Already present conceptually.
`python/chaos_game.py` iteration counter	`python/chaos_game.py`	🟠 ADAPT	Make TIC derivation explicit: each chaos-game step emits an event receipt.
`4-Infrastructure/shim/run_trace_v2_canary.py`	`EventLib/`	🔴 DROP	Trace-canary runner tied to Research-Stack ENE schema. Reimplement against SilverSight core.

AuditLib Layer

Research-Stack	SilverSight Target	Status	Notes
`5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py`	`AuditLib/`	🟠 ADAPT	Receipt verification + SHA256 answer check. Refactor to verify SilverSight receipts.
`4-Infrastructure/shim/pvgs_receipt_hash.py`	`formal/PVGS_DQ_Bridge/` / `AuditLib/`	✅ PORTED	Already present in SilverSight.
`shared-data/data/stack_solidification/` receipts	`AuditLib/`	🔴 DROP	Research-Stack runtime receipts; archive only. Regenerate in SilverSight.

RRCLib Layer

Research-Stack	SilverSight Target	Status	Notes
`Semantics.RRC.Emit.lean` (ncDerived)	`formal/SilverSight/RRC/Emit.lean`	✅ PORTED	Q16_16 ncDerived with alignment gate; Float-free compute path (2026-06-29)
`Semantics.RRC.Q16_16Manifold.lean` (Q16_16)	`formal/SilverSight/RRC/Q16_16Manifold.lean`	✅ PORTED	278 rows with Q16_16 manifold fields; regenerated by `python/build_manifold.py`
`Semantics.AVMIsa.Emit.lean`	`RRCLib/`	🟡 PORT	Sole output boundary for top-level receipt JSON.
`Semantics.RRC.ReceiptDensity.lean`	`formal/SilverSight/RRC/ReceiptDensity.lean`	✅ PORTED	Receipt density scoring (already existed)
`Semantics.RRCLogogramProjection.lean`	`formal/SilverSight/RRCLogogramProjection.lean`	✅ PORTED	Logogram receipt types + admission gates
`4-Infrastructure/shim/validate_rrc_predictions.py`	`python/`	🟠 ADAPT	Validation harness; refactor to SilverSight receipt format
—	`formal/SilverSight/FFS/Validation.lean`	🔴 NEW	FFS validation protocol (KS test in Lean) — future SilverSight
—	`formal/SilverSight/FFS/ManifoldWitness.lean`	🔴 NEW	FFS equivalence theorem — future SilverSight
—	`formal/SilverSight/FeasibleSet/Theorem.lean`	🔴 NEW	Feasible-Set Relaxation Theorem (Set.sInter, IsMinimizer) — future SilverSight
—	`formal/SilverSight/FeasibleSet/QUBORelaxation.lean`	🔴 NEW	k-hot QUBO instantiation — future SilverSight

Infrastructure Layer

Research-Stack	SilverSight Target	Status	Notes
`AGENTS.md` hierarchy	`docs/` + root `AGENTS.md`	🟡 PORT	Bring root + core subtree AGENTS.md rules. Drop stale project-state blocks.
`REBASE_RULES.md`	root `REBASE_RULES.md`	✅ PORTED	Already pushed.
`.github/workflows/lean-check.yml`	`.github/workflows/`	🟠 ADAPT	Adapt CI to SilverSight `lake build` paths.
`.github/workflows/python-check.yml`	`.github/workflows/`	🟠 ADAPT	Adapt Python test paths.
`.github/workflows/q16-roundtrip.yml`	`.github/workflows/`	✅ PORTED	Already present.
`.devin/skills/lean-proof/SKILL.md`	`.devin/skills/`	🟡 PORT	Mandatory for all Lean work.
`.github/skills/contextstream-workflow/SKILL.md`	`.github/skills/`	🟡 PORT	Persistent memory workflow.
`.github/skills/research-stack-workflow/SKILL.md`	`.github/skills/`	🟠 ADAPT	Rename to `silversight-workflow`; update paths.
`.cursorrules`, `.devin/config.json`, `.claude/settings.json`	root / `.devin/`	🟡 PORT	Editor hook configs enforcing ContextStream-first rules.
`scripts/qc-flag/`	`scripts/qc-flag/`	🟡 PORT	7-check Lean QC protocol.

4. Gaps

Things SilverSight's architecture calls for but Research-Stack does not cleanly provide:

Gap	Where it belongs	What to build
`SilverSightCore.lean` completeness	`Core/`	Finish HachimojiState, Receipt, Instruction, δ, TIC axiom, loop invariant. Current file is a sketch.
LexLib / MathLib	`Library/LexLib.lean`	No complete LaTeX/ASCII tokenizer exists in Research-Stack. Build from `equation_shape_parser.py` + `math_symbols.py`.
EventLib	`Library/EventLib.lean`	TIC counter is conceptual only. Implement event receipts from chaos-game steps.
RRCLib	`Library/RRCLib/`	RRC is in `PVGS_DQ_Bridge_fixed.lean` §4. Extract into standalone library per `docs/RRC_PLACEMENT.md`.
Orchestrator	`Orchestrator/SilverSight.lean`	No equivalent in Research-Stack. Build new composition layer.
CBridge / PythonBridge	`CBridge/`, `PythonBridge/`	Mentioned in `docs/ARCHITECTURE.md` but not present. Build Q16_16 C lib + ctypes bindings.
Doc-sync CI	`.github/workflows/doc-sync.yml`	Exists but needs to verify porting map + architecture docs stay consistent.

5. Conflicts

Conflict	Resolution
Research-Stack `Q16_16.lean` / `FixedPoint.lean` vs SilverSight `Q16_16_Spec.lean`	✅ PORTED — `Q16_16_Spec.lean` deleted; `formal/CoreFormalism/FixedPoint.lean` is now the canonical source of truth.
Duplicate `Schema` class in `formal/SilverSight/Schema.lean` vs `Core/SilverSight/Semantics/Schema.lean`	✅ RESOLVED 2026-06-25 — `formal/SilverSight/Schema.lean` is now a shim that re-exports Core Schema. Core Schema extended with Q16_16, Q0_16, UInt64 instances. `ProductSchema.lean`, `ProductWireFormat.lean`, `Receipt.lean` registered and building clean.
PVGS Bridge `Q16_16` (`.raw : Int` / `toInt = raw/65536`) vs Core `Q16_16` (`.val : Int` / `toInt = .val`)	✅ RESOLVED 2026-06-25 — `BindingSiteCodec.lean` no longer imports PVGS Bridge; `dqEnergy`/`stellarRank` computed directly from entropy profile. Bridge Q16_16 type remains in `PVGS_DQ_Bridge_fixed.lean` only.
Research-Stack `qaoa_adapter.py` (2,421 lines) vs SilverSight split `qubo/*.py`	Split adapter: Finsler/QUBO builder → MetricLib/QUBOLib; circuit generation → QUBOLib; bitstring bridge → PVGSLib.
Research-Stack `AGENTS.md` references many dead paths	Port rules, not state. Update path references to SilverSight equivalents.
SilverSight `ARCHITECTURE.md` uses 6 layers; conceptual map uses 5	Reconcile: 5-layer conceptual map is authoritative; 6-layer doc is an older draft. Update `ARCHITECTURE.md` to match 5-layer model + library method.

6. Recommended Porting Order

Core first — ✅ Replace Q16_16_Spec.lean with full FixedPoint.lean. Lock down SilverSightCore.lean. SilverSightCore.lean now builds with no sorries and no Float.
SearchLib — Port SidonSets.lean, SieveLemmas.lean, InteractionGraphSidon.lean.
RRCLib — Extract RRC gates from PVGS_DQ_Bridge_fixed.lean §4 into standalone library.
QUBOLib + MetricLib — Split qaoa_adapter.py and qubo_highs.py cleanly.
LexLib — Build tokenizer from math_symbols.py + equation_shape_parser.py.
AuditLib + EventLib — Implement receipt validation and TIC counting.
Orchestrator — Compose all libraries through Core.
Skills + editor configs — Port agent rules last, once directory structure is stable.

7. Drop List

Do not port these Research-Stack artifacts:

legacy/ and ExtensionScaffold/ modules with pre-existing errors.
Quarantined PIST.HybridTSMPISTTorus.
VCN/LUPINE infrastructure (extracted to distributed-compute-fabric).
Kubernetes/k3s manifests, Ray actors, Garage/restic storage scripts (extracted to distributed-compute-fabric).
Stale assignment boards (windsurf/ASSIGNMENTS.md) and old sorry audits (windsurf/SORRY_AUDIT.md).
Runtime DBs, consolidation manifests, and generated receipts under shared-data/ and .headroom/.
.agents/plugins/marketplace.json and dormant substack-connector.
Biological/genetics extensions unless the BindingSite direction is pursued.

This map is a living document. Update it as components are ported or reclassified.

CFF-to-Module Mapping

Cross-reference between CITATION.cff reference notes and SilverSight modules. Entries marked 🟡 are planned or partially ported; ✅ means a corresponding SilverSight file currently exists on disk.

CFF reference	Research-Stack module(s)	SilverSight target	Exists?
Giani, Win, Conti (2025) — Photon-Varied Gaussian States	`Semantics.PVGS_DQ_Bridge`	`formal/PVGS_DQ_Bridge/`	✅
Chabaud, Mehraban (2022) — Stellar representation	`Semantics.PVGS_DQ_Bridge`	`formal/PVGS_DQ_Bridge/`	✅
Pizzimenti et al. (2024) — Wigner negativity	`Semantics.BindingSite`, `Semantics.PVGS_DQ_Bridge`	`formal/BindingSite/`, `formal/PVGS_DQ_Bridge/`	✅
Wassner et al. (2025) — Single quadrature noise tomography	`Semantics.PVGS_DQ_Bridge`	`formal/PVGS_DQ_Bridge/`	✅
Saucedo (2019) — Pascal's Triangle / Sidon constructions	`Semantics.SidonSets`	`formal/CoreFormalism/SidonSets.lean`	✅ (`CoreFormalism.SidonSets` builds; chaos-game appendix dropped)
Farr, Groot (2009) — Close packing density	`Semantics.BraidEigensolid`, `Semantics.BraidSpherionBridge`, `Semantics.BaselineComparison`	`formal/CoreFormalism/BraidEigensolid.lean`, `formal/CoreFormalism/BraidSpherionBridge.lean`	✅ (BaselineComparison not yet ported)
Fasolo, Sollich (2004) — Fractionation effects	`Semantics.BraidEigensolid` (meta-solid concept)	`formal/CoreFormalism/BraidEigensolid.lean`	✅
Baranau, Tallarek (2014) — Random-close packing limits	`Semantics.BraidEigensolid`	`formal/CoreFormalism/BraidEigensolid.lean`	✅
Kofke, Bolhuis (1999) — Freezing of polydisperse hard spheres	`Semantics.BraidEigensolid`, `Semantics.BaselineComparison`	`formal/CoreFormalism/BraidEigensolid.lean`	✅ (BaselineComparison not yet ported)
Arrizabalaga, Tracy, Manchester (2026) — Differentiable IPM	`Semantics.FixedPoint`, `Semantics.Q16InverseProof`	`formal/CoreFormalism/FixedPoint.lean` (absorbed)	✅
Yang et al. (2026) — STARS recurrent dynamics	`Semantics.AVMIsa.*`, `Semantics.Run`	`Core/SilverSightCore.lean` (AVM transition function)	✅

Unresolved references

Semantics.MetaSolid is cited in CITATION.cff as a Research-Stack module, but no Semantics.MetaSolid.lean file exists in Research-Stack. It is treated here as the meta-solid concept documented in the ContextStream node e967f515-3af9-46c9-9fc8-e5c766a6c4fc and bound to Semantics.BraidEigensolid.
Semantics.BaselineComparison and the meta-solid concept (Semantics.MetaSolid) are cited in CITATION.cff but have no corresponding SilverSight module on disk yet. They are tracked as 🟡 PORT targets in the SearchLib layer above.
The original CITATION.cff cited formal/BraidEigensolid.lean and formal/BraidSpherionBridge.lean at the repository root; those files now live at formal/CoreFormalism/BraidEigensolid.lean and formal/CoreFormalism/BraidSpherionBridge.lean.

22 KiB Raw Permalink Blame History Unescape Escape