# Build Log: 2026-06-21 — SidonSets Restoration & SilverSight Porting Graph

## Session Summary

Restored `CoreFormalism.SidonSets.lean` to the active SilverSight build, hardened the
SilverSight core surface, and generated a searchable Research Stack porting graph to guide
the long-term migration of provably useful math/concepts from Research Stack.

## Build Baselines

All builds run against SilverSight `main` at `8f1d30d` with toolchain
`leanprover/lean4:v4.32.0-rc1`.

| Command | Jobs | Errors | Notes |
|---|---|---|---|
| `lake build` | 2978 | 0 | Default build target |
| `lake build SilverSightFormal` | 3118 | 0 | Full formal library |
| `lake build CoreFormalism.SidonSets` | 2601 | 0 | Narrow target after restore |
| `lake build CoreFormalism.SieveLemmas` | 2402 | 0 | Ported sieve foundation |
| `lake build CoreFormalism.InteractionGraphSidon` | 2530 | 0 | Ported interaction-graph module |
| `lake build CoreFormalism.BraidEigensolid` | 2680 | 0 | Ported braid eigensolid |
| `lake build CoreFormalism.BraidSpherionBridge` | 2745 | 0 | Ported spherion bridge |

## What Was Ported / Restored

### Core formalism modules

- `CoreFormalism.FixedPoint` — canonical `Q16_16` fixed-point surface
- `CoreFormalism.Tactics` — common tactics for the project
- `CoreFormalism.Q16_16Numerics` — numeric helpers over `Q16_16`
- `CoreFormalism.DynamicCanal` — dynamic canal infrastructure
- `CoreFormalism.Bind` — binding layer
- `CoreFormalism.BraidBracket` — braid bracket primitives
- `CoreFormalism.BraidStrand` — strand model
- `CoreFormalism.BraidCross` — crossing model
- `CoreFormalism.BraidField` — braid field operations
- `CoreFormalism.SidonSets` — Sidon sets, extremal function, bounds, Singer theorem
- `CoreFormalism.SieveLemmas` — sieving lemmas for Sidon constructions
- `CoreFormalism.InteractionGraphSidon` — interaction graph + Sidon labeling
- `CoreFormalism.BraidEigensolid` — eigensolid fixed-point theory
- `CoreFormalism.BraidSpherionBridge` — braid/spherion bridge

### Python tooling / tests

- `tests/test_q16_canonical.py` — 10 green tests asserting canonical `Q16_16` semantics
- `tests/quarantine/q16_roundtrip_test.legacy.py` — archived; waits on C bridge restoration
- `.github/scripts/glossary_lint.py` — warns when docs introduce undefined terms

### Documentation / contracts

- `docs/GLOSSARY.md` — living dictionary with standard-terminology crosswalk
- `docs/GLOSSARY_ALLOWLIST.md` — allowlist for glossary lint
- `docs/TESTING.md` — unit/integration/CI testing contract
- `docs/research_stack_usage_graph.{json,md,dot,svg,png}` — searchable 13k-entity graph of Research Stack usage
- `docs/research_stack_porting_candidates.md` — prioritized porting shortlist
- `CITATION.cff` — updated with module-specific reference notes

## SidonSets Restoration Details

The module was quarantined because a chaos-game appendix used invalid Lean syntax and
out-of-scope identifiers. Restoration steps:

1. Removed the broken chaos-game appendix entirely.
2. Replaced LaTeX-style escapes (`\Z`, `\N`) with `Int` / `Nat` in comments.
3. Introduced local `abbrev Z := Int` and `abbrev N := Nat` to avoid auto-implicit shadowing.
4. Fixed finset decidability issues and omega/linarith failures by normalizing to `Nat` where appropriate.
5. Verified with narrow and full library builds.

## Research Stack Usage Graph

Generated a cross-reference graph from the Research Stack checkout at
`/home/allaun/Research Stack`:

- **Nodes:** 13 000+ files, modules, and concepts
- **Edges:** 13 000+ import / usage / reference relationships
- **Outputs:** JSON, Markdown, GraphViz DOT, SVG, PNG
- **Purpose:** convert the legacy Research Stack into a searchable point graph so useful
  math, code, and goals can be located and ported deterministically.

## CI / Contract Updates

- `.github/workflows/lean-check.yml` — Lean build gate
- `.github/workflows/python-check.yml` — Python test + glossary lint gate
- `.github/workflows/doc-sync.yml` — documentation sync gate
- `docs/generate_project_map.py` — regenerable project map generator

## Generated Artifacts

- `docs/PROJECT_MAP.md` — human-readable SilverSight project map (77 files, 10 layers)
- `docs/PROJECT_MAP.json` — machine-readable project map (schema `silversight_project_map_v1`)

## Invariants Upheld

- No `Float` in any Lean compute path.
- `ofFloat` only permitted at JSON/sensor boundaries.
- Library-method architecture preserved: `Core/` imports nothing; libraries import only `Core/`
  or Mathlib; no library imports another library.
- `Q16_16` unified to `CoreFormalism.FixedPoint`.

## Next Recommended Work

- Restore C bridge for `Q16_16` roundtrip tests.
- Port additional Research Stack modules identified in `docs/research_stack_porting_candidates.md`.
- Add `#eval` witnesses / roundtrip proofs for remaining core modules per `docs/TESTING.md`.


## RRCLib Port (this session)

Ported Research-Stack RRC decision surface into SilverSight as a new library.

### Files added

- `formal/SilverSight/RRCLogogramProjection.lean` — RRC shape/logogram admission gates
- `formal/SilverSight/ReceiptCore.lean` — receipt kinds, ledger, and `toSilverSightReceipt` bridge
- `formal/SilverSight/RRC/Emit.lean` — 6 canonical fixture rows, alignment gate, JSON emitter
- `formal/SilverSight/AVMIsa/{Types,Value,Instr,State,Step,Run,Emit}.lean` — AVM ISA + canary bundle
- `formal/RRCLib/` — user-facing symlinks to the SilverSight modules
- `exe/RrcEmitFixture.lean` — executable that emits the fixture corpus JSON
- `python/pist_matrix_builder.py` — PIST 8×8 matrix builder (I/O only)
- `python/validate_rrc_predictions.py` — emitted JSON validator (I/O only)

### Build verification

| Command | Jobs | Errors | Notes |
|---|---|---|---|
| `lake build` | 2981 | 0 | Default target |
| `lake build SilverSightRRC` | 2992 | 0 | New RRC library |
| `lake build SilverSightCore` | 3132 | 0 | No regression; FixedPoint now in Core |
| `lake build SilverSightFormal` | 3132 | 0 | No regression |
| `lake build rrc-emit-fixture` | — | 0 | Executable JSON emitter |

### Deviations from source

- Skipped the 250-equation corpus; added `emitFixtureCorpus` for the 6-row fixture corpus.
- Moved canonical `FixedPoint` to `Core/SilverSight/FixedPoint.lean`; `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim.
- Actual Lean modules live under `formal/SilverSight/`; `formal/RRCLib/` holds symlinks so the requested paths exist.

### Final verification run

| Gate | Result |
|---|---|
| `lake build` | ✅ 2981 jobs, 0 errors |
| `lake build SilverSightCore` | ✅ 3132 jobs, 0 errors |
| `lake build SilverSightFormal` | ✅ 3132 jobs, 0 errors |
| `lake build SilverSightRRC` | ✅ 2992 jobs, 0 errors |
| `lake build rrc-emit-fixture` | ✅ green |
| `python3 -m py_compile python/pist_matrix_builder.py python/validate_rrc_predictions.py tests/test_q16_canonical.py .github/scripts/check_doc_sync.py .github/scripts/glossary_lint.py` | ✅ green |
| `python3 .github/scripts/glossary_lint.py` | ✅ no warnings |
| `python3 .github/scripts/check_doc_sync.py` | ✅ OK |
| `rrc-emit-fixture \| validate_rrc_predictions.py` | ✅ OK: 6 rows |
| `pytest tests/test_q16_canonical.py` | ⚠️ skipped — pytest not installed |

---

## Later same day: RRC module ports and Q16_16 cross-language roundtrip

### What changed

- Ported three Research Stack RRC gates into `formal/SilverSight/RRC/`:
  - `ReceiptDensity.lean` — Q16_16 receipt-density scoring
  - `PolyFactorIdentity.lean` — divisor-sum signature gate (E8Sidon surface stubbed)
  - `EntropyCandidates.lean` — 10 braid-state fixtures using
    `CoreFormalism.BraidEigensolid` types
- Added a Lean ↔ C ↔ Python Q16_16 roundtrip test:
  - `c/q16_canonical.c` — canonical saturating Q16_16 C library
  - `exe/Q16_16Roundtrip.lean` — Lean executable linked via Lake `extern_lib`
  - `tests/test_q16_roundtrip.py` — Python ↔ C roundtrip harness (revived from
    `tests/quarantine/q16_roundtrip_test.legacy.py`)
- Updated `lakefile.lean` with the `q16-roundtrip` executable and the
  `extern_lib q16_canonical` build target.

### Build baselines

| Command | Jobs | Errors | Notes |
|---|---|---|---|
| `lake build` | 2981 | 0 | Default target |
| `lake build SilverSightRRC` | 3006 | 0 | RRC decision surface incl. new gates |
| `lake build q16-roundtrip` | 5949 | 0 | Lean ↔ C executable |

### Test results

| Test | Result |
|---|---|
| `python3 tests/test_q16_roundtrip.py` | ✅ 21 tests passed |
| `.lake/build/bin/q16-roundtrip` | ✅ 35 Lean ↔ C tests passed |

---

## Later same day: Phase 1 core — schema / layout / wireformat modules

### What changed

Implemented the YaFF-inspired Phase 1 Core modules in
`Core/SilverSight/Semantics/`:

- `Schema.lean` — fixed-size schema contract (`byteSize`, `wellFormed`).
- `Layout.lean` — `Layout` enum, `AccessProfile`, Q0_16 `Layout.cost`,
  `chooseLayoutByCost`, and an ε-suboptimality theorem.
- `WireFormat.lean` — certified encoder/decoder structure
  (`encode`, `decode`, `encode_size`, `roundTrip`) with row-major instances
  for `Unit`, `Bool`, and `UInt8`.
- `View.lean` — zero-copy view contract (`base`, `offset`, `valid`) and a
  `readUInt8` accessor backed by address-arithmetic.
- `LayoutBridge.lean` — certified layout conversion structure and identity
  bridges.
- `CanalLayout.lean` — `CanalRegime` enum and `chooseLayout` override on
  top of the pure cost model.

Updated `lakefile.lean` to add all new `SilverSight.Semantics.*` modules to
`SilverSightCore`. Updated `docs/ARCHITECTURE.md`, `AGENTS.md`,
`docs/RRC_REFACTOR_READINESS.md`, and `SilverSight_Spec.md` to reflect the
new Core surface.

### Build baselines

| Command | Jobs | Errors | Notes |
|---|---|---|---|
| `lake build` | 2987 | 0 | Default target now includes Semantics core |
| `lake build SilverSightCore` | 2987 | 0 | Core + Semantics modules |
| `lake build SilverSightRRC` | 3006 | 0 | RRC decision surface |
| `lake build q16-roundtrip` | 5949 | 0 | Lean ↔ C executable |

### Verification results

| Test | Result |
|---|---|
| `python3 tests/test_q16_roundtrip.py` | ✅ 21 tests passed |
| `.lake/build/bin/q16-roundtrip` | ✅ 35 Lean ↔ C tests passed |
| `python3 .github/scripts/glossary_lint.py` | ✅ no warnings |
| `python3 .github/scripts/check_doc_sync.py` | ✅ OK |

### Notes

- `Semantics` modules import only `SilverSight.FixedPoint` and Mathlib,
  preserving the library-method rule that Core may not depend on libraries.
- The full `DynamicCanal` physics remains in `CoreFormalism.DynamicCanal`;
  `CanalLayout` is the Core-side abstraction that will be driven by it.
- Concrete `WireFormat`/`LayoutBridge` instances for product types such as
  `BraidState` are left as library extensions.