SilverSight/lean-toolchain at 93c6b0a6918ab53fb820edd80ddebf5609d5ca65 - allaun/SilverSight - Forgejo: Beyond coding. We Forge.

allaun/SilverSight

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

allaun 7a973a06f6 feat(core): harden SilverSightCore and port canonical FixedPoint

- Remove Float from Core/SilverSightCore.lean (Receipt.pathCost is now Option Nat)
- Prove TIC theorems tic_never_decreases and computation_generates_time
- Add lakefile.lean, lean-toolchain, and .gitignore for .lake/
- Port Research-Stack Semantics.FixedPoint.lean to formal/CoreFormalism/FixedPoint.lean
- Delete thin Q16_16_Spec.lean; update Python/QUBO comments and docs
- Create AGENTS.md distilled from Research Stack core bindings
- Update REBASE_RULES.md to strip legacy hacks and reference AGENTS.md

Build: 2978 jobs, 0 errors (lake build)

2026-06-21 06:30:12 -05:00

1 line

No EOL

28 B

Text

Raw Blame History

leanprover/lean4:v4.32.0-rc1