|
|
7c303624be
|
refactor(core): typed Invariant/TensorType migration, CartanConnection cleanup
Bind.lean:
- Add Invariant structure (Nat-backed identifier) with DecidableEq
- Add Invariant.ofNat / Invariant.fromString (boundary-only string->Nat hash)
- Add TensorType inductive enum (identity, riemannian, thermodynamic, etc.)
- Migrate Metric.tensor from String to TensorType (AGENTS.md S1.5 compliance)
- Migrate Witness.left_invariant/right_invariant from String to Invariant
- Update all bind theorems and #eval call sites
BraidField.lean:
- Update computePIST call sites to use Invariant.fromString
BraidEigensolid.lean:
- Simplify eigensolid_trivial proof (drop unnecessary calc block)
CartanConnection.lean:
- Extract C_int_cross_block_zero lemma
- Extract factor_sum lemma (eliminates inline factor helper)
- Extract mu_double_lift lemma (factors out triplicated pattern in
Jacobiator_basis_zero_int, reducing it from ~30 lines to ~12)
- Simplify Jacobiator_basis_all using refine+rw pattern
nr_bracket_validation.py:
- Fix stale file path (Research Stack -> research-stack)
|
2026-06-28 00:11:28 -05:00 |
|
|
|
4490dc28a7
|
feat(rrc): bare-minimum RRC refactor into SilverSight
- Move canonical FixedPoint to Core/SilverSight/FixedPoint.lean
- Add SilverSightRRC library: RRC logogram gates, receipt bridge, AVM ISA
- Add AVMIsa.Emit as the sole top-level JSON output boundary
- Add rrc-emit-fixture executable and Python I/O shims
- Update AGENTS.md, glossary, project map, and build baseline
Build: 2981 jobs, 0 errors (lake build)
|
2026-06-21 09:08:48 -05:00 |
|
