SilverSight/docs/build_logs/2026-06-21_session_build_baseline.md

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