Brandon Schneider 6047beec4f feat(lean): BraidSpherionBridge — SpherionState ↔ BraidState equivalence ... Bridge module connecting: - SpherionState (Mountain/MMR/betaStep/rgFlow) - BraidState (8 strands/crossStep/BraidReceipt/encodeReceipt) Key content: - SpherionSpike inductive (Mountain + crossPair Fin 4) - IntNodeToPhaseVec bridge function - spikeToStrandUpdate, strandFlow operations - crossPair lemmas (0→(0,1), 1→(2,3), 2→(4,5), 3→(6,7)) - braidCross_phase_linear, Mountain_merge_apex_add lemmas - braidCross_merge_correspondence (admit — TODO(lean-port): complete) - k_spike_step_count (admit) - receipt_correspondence, receipt_encode_stable (admit) Build: 3572 jobs, 0 errors (lake build)		2026-05-30 13:29:13 -05:00
..
conversions/hardware	WIP: accumulated changes	2026-05-25 16:24:21 -05:00
external/OTOM	WIP: accumulated changes	2026-05-25 16:24:21 -05:00
LeanGPT	Remove legacy Python prototypes superseded by Lean formalization	2026-05-19 15:34:17 +00:00
Semantics	feat(lean): BraidSpherionBridge — SpherionState ↔ BraidState equivalence	2026-05-30 13:29:13 -05:00
CHAIN_ALL_REVIEW_REPORT.md	initial: sovereign research stack (consolidated, weightless, and lfs-optimized)	2026-05-04 18:11:36 -05:00