SNAPKITTYWEST commited on
Commit
4bc8ea5
Β·
verified Β·
1 Parent(s): 80d7559

Sync with GitHub, license metadata from LICENSE files, commercial license notice

Browse files

sync from SNAPKITTYWEST/carry-agent: 2 files
metadata license: None -> agpl-3.0
README: License section kept (already accurate) + commercial notice
README: GitHub source link added

Files changed (2) hide show
  1. .gitattributes +5 -7
  2. README.md +442 -428
.gitattributes CHANGED
@@ -1,7 +1,5 @@
1
- *.curry linguist-language=Curry
2
- *.pl linguist-language=Prolog
3
- *.rs linguist-language=Rust
4
- Cargo.toml linguist-detectable=false
5
- Cargo.lock linguist-detectable=false
6
- docs/carry_brand_banner.png filter=lfs diff=lfs merge=lfs -text
7
- docs/firecarry.png filter=lfs diff=lfs merge=lfs -text
 
1
+ *.curry linguist-language=Curry
2
+ *.pl linguist-language=Prolog
3
+ *.rs linguist-language=Rust
4
+ Cargo.toml linguist-detectable=false
5
+ Cargo.lock linguist-detectable=false
 
 
README.md CHANGED
@@ -1,428 +1,442 @@
1
- <p align="center">
2
- <img src="docs/firecarry.png" alt="CARRY β€” CARTO's Evil Twin Made of Curry" width="360px" />
3
- </p>
4
-
5
- <h1 align="center">CARRY</h1>
6
- <h3 align="center">Adversarial Twin of CARTO</h3>
7
-
8
- <p align="center">
9
- <strong>CURRY_CRYSTAL_C3 Triad + Braid Topology + Sovereign Quantum Simulator</strong><br />
10
- 7-state DAG-locked pipeline Β· Entropy-gated transitions Β· Tau-Prolog logic kernel<br />
11
- Fibonacci anyons Β· ICP governance Β· BLAKE3 WORM audit chain<br />
12
- <em>The FSM tells you WHERE you are. The braid tells you WHETHER you got there honestly.</em>
13
- </p>
14
-
15
- <p align="center">
16
- <img src="https://img.shields.io/badge/lang-Rust-orange?style=flat-square" />
17
- <img src="https://img.shields.io/badge/logic-Tau--Prolog-blue?style=flat-square" />
18
- <img src="https://img.shields.io/badge/proof-Braid_B₃-purple?style=flat-square" />
19
- <img src="https://img.shields.io/badge/quantum-Fibonacci_Anyons-cyan?style=flat-square" />
20
- <img src="https://img.shields.io/badge/formal-Lean_4_%2B_Agda-blueviolet?style=flat-square" />
21
- <img src="https://img.shields.io/badge/tests-14%2F14_PASS-brightgreen?style=flat-square" />
22
- <img src="https://img.shields.io/badge/sorry-0-brightgreen?style=flat-square" />
23
- <img src="https://img.shields.io/badge/license-AGPL--3.0-green?style=flat-square" />
24
- </p>
25
-
26
- ---
27
-
28
- <p align="center">
29
- <img src="docs/carry_brand_banner.png" alt="CARRY FSM β€” Adversarial Twin System + Deterministic Compiler Engine" width="100%" />
30
- </p>
31
-
32
- ---
33
-
34
- ```
35
- β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•— β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•— β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•— β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•— β–ˆβ–ˆβ•— β–ˆβ–ˆβ•—
36
- β–ˆβ–ˆβ•”β•β•β•β•β•β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•—β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•—β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•—β•šβ–ˆβ–ˆβ•— β–ˆβ–ˆβ•”β•
37
- β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•‘β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•”β•β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•”β• β•šβ–ˆβ–ˆβ–ˆβ–ˆβ•”β•
38
- β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•‘β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•—β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•— β•šβ–ˆβ–ˆβ•”β•
39
- β•šβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•—β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•‘β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•‘β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•‘
40
- β•šβ•β•β•β•β•β•β•šβ•β• β•šβ•β•β•šβ•β• β•šβ•β•β•šβ•β• β•šβ•β• β•šβ•β•
41
-
42
- ╔═══════════════════════════════════════════════╗
43
- β•‘ B R A I D T O P O L O G Y R U N T I M E β•‘
44
- β•‘ σ₁ Β· Οƒβ‚‚ Β· σ₁ = Οƒβ‚‚ Β· σ₁ Β· Οƒβ‚‚ β•‘
45
- β•‘ Yang-Baxter holds. The chain is honest. β•‘
46
- β•šβ•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•
47
-
48
- strand 0 ──╲ ╱── Οƒβ‚‚ crossing
49
- strand 1 β•²β•±
50
- β•±β•²
51
- strand 2 ──╱ ╲── σ₁ crossing
52
- β”‚
53
- β–Ό
54
- [C3 at pos 0]
55
- writhe = +2
56
- INVARIANT HOLDS
57
- ```
58
-
59
- ---
60
-
61
- ## What Is CARRY?
62
-
63
- CARRY is the **adversarial twin** of [CARTO](https://github.com/SNAPKITTYWEST/cartographer-agent).
64
-
65
- **CARTO** is the sovereign mapping agent β€” it models terrain, constructs pipelines, and produces outputs it claims are valid.
66
-
67
- **CARRY** attacks those outputs. If CARRY cannot break CARTO's pipeline, the pipeline is honest. CARRY is the red team that never sleeps β€” a formal adversary baked into the architecture itself rather than run as a separate audit process.
68
-
69
- The relationship:
70
-
71
- ```
72
- CARTO CARRY
73
- ───── ─────
74
- Maps terrain ←→ Attacks the map
75
- Claims pipeline is valid ←→ Tries to falsify the claim
76
- Produces WORM output ←→ Verifies the WORM seal
77
- GOTO (push semantics) ←→ COME-FROM (pull semantics)
78
- Forward evolution (U) ←→ Reversed evolution (U†)
79
- ```
80
-
81
- The braid topology encodes this duality formally: every GOTO crossing has a matching COME-FROM crossing. The writhe invariant proves that authority was transferred through the correct sequence of crossings β€” not just that it arrived at the right place, but that it took the right path.
82
-
83
- If the path is wrong, the braid is wrong. If the braid is wrong, the proof is rejected. No exceptions.
84
-
85
- ---
86
-
87
- ## Braid Authority Transfer
88
-
89
- ```
90
- INITIAL: Curry ──── Crystal ──── C3
91
- [0] [1] [2] (authority = pos 0)
92
-
93
- After Οƒβ‚‚: Curry ──── C3 ──── Crystal
94
- [0] [1] [2] (C3 crosses OVER Crystal)
95
-
96
- After σ₁: C3 ──── Curry ──── Crystal
97
- [0] [1] [2] (C3 crosses OVER Curry)
98
-
99
- Writhe W(Ξ²) = (+1) + (+1) = +2
100
- C3 at position 0 β†’ AUTHORITY TRANSFERRED
101
- INVARIANT HOLDS βœ“
102
- ```
103
-
104
- ```
105
- BRAID WORD: Οƒβ‚‚ Β· σ₁
106
- ─────────────────────
107
- Curry ────\────────────────
108
- \
109
- Crystal ────X──\────────── Οƒβ‚‚: C3 over Crystal
110
- / \
111
- C3 ─────── /────X──────── σ₁: C3 over Curry
112
- \
113
- β–Ό
114
- C3 at pos 0
115
- W = +2 βœ“
116
- ```
117
-
118
- ---
119
-
120
- ## Architecture
121
-
122
- ```
123
- ╔══════════════════════════════════════════════════════════════╗
124
- β•‘ CARRY STACK β•‘
125
- ╠══════════════════════════════════════════════════════════════╣
126
- β•‘ FORMAL LAYER Lean 4 + Agda β•‘
127
- β•‘ 13 invariants Β· 0 sorry β•‘
128
- β•‘ state_preservation proved β•‘
129
- β•‘ duality_involution proved β•‘
130
- ╠══════════════════════════════════════════════════════════════╣
131
- β•‘ QUANTUM LAYER Fibonacci Anyon Simulator β•‘
132
- β•‘ B₃ braid group Β· Ο† = 1.6180 β•‘
133
- β•‘ StateVector + DensityMatrix engines β•‘
134
- β•‘ ICP 6-stage governance pipeline β•‘
135
- β•‘ ASP declarative constraint solver β•‘
136
- β•‘ 6052 cycle-accurate emulator β•‘
137
- ╠══════════════════════════════════════════════════════════════╣
138
- β•‘ GOVERNANCE LAYER Conditional Dual DAG β•‘
139
- β•‘ GOTO ↔ COME-FROM duality β•‘
140
- β•‘ state preserved across ALL transitions β•‘
141
- β•‘ BLAKE3 WORM audit chain β•‘
142
- ╠══════════════════════════════════════════════════════════════╣
143
- β•‘ RUNTIME LAYER Rust (carry-fsm crate) β•‘
144
- β•‘ 7-state DAG-locked FSM β•‘
145
- β•‘ Entropy ≀ 0.20 gate β•‘
146
- β•‘ Tau-Prolog logic kernel β•‘
147
- β•šβ•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•
148
- ```
149
-
150
- ---
151
-
152
- ## 7-State Quantum FSM
153
-
154
- ```
155
- β”Œβ”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”
156
- β”‚ INIT │───▢│ PREPARE │───▢│ ENTANGLE │───▢│ COMPUTE β”‚
157
- β””β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”¬β”€β”€β”€β”€β”˜
158
- β”‚
159
- β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β” β”‚
160
- β”‚ COMMIT │◀───│ VERIFY │◀───│MEASURE β”‚β—€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜
161
- β””β”€β”€β”€β”¬β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”˜
162
- β”‚
163
- └──▢ PREPARE (loop) ─── or ─── COMMIT (terminal)
164
-
165
- Any state ──▢ HALTED (emergency)
166
- Any state ──▢ CYCLE_LIMIT (budget exhausted, absorbing)
167
-
168
- Theorem (Lean 4, zero sorry):
169
- Halted and CYCLE_LIMIT are ABSORBING STATES.
170
- No transition exits them. Ever.
171
- ```
172
-
173
- ---
174
-
175
- ## The Quantum Module
176
-
177
- CARRY ships a full first-principles quantum simulator:
178
-
179
- ```
180
- runtime/quantum/
181
- β”œβ”€β”€ core.rs StateVector |ψ⟩ + DensityMatrix ρ engines
182
- β”‚ Born rule measurement Β· noise models
183
- β”‚ H X Y Z S T Rx Ry Rz CNOT CZ SWAP
184
- β”œβ”€β”€ fsm.rs 7-state governance FSM (proved absorbing terminals)
185
- β”œβ”€β”€ agents.rs Primary + Partner agent pairs
186
- β”‚ Qubit ownership: pairwise disjoint (proved INV-7)
187
- β”œβ”€β”€ dag.rs Execution DAG + provenance hash chain
188
- β”œβ”€β”€ icp.rs Integrity Constraint Protocol
189
- │ 6 stages: Setup→Observe→Validate→Check→Execute→Verify
190
- β”‚ HALT on any constraint breach
191
- β”œβ”€β”€ asp.rs Answer Set Programming constraint solver
192
- β”‚ QubitControl Β· Entangled Β· AgentControls rules
193
- β”œβ”€β”€ topological.rs Fibonacci anyon simulator
194
- β”‚ B₃: σ₁ Οƒβ‚‚ σ₁���¹ σ₂⁻¹ Β· Ο† β‰ˆ 1.6180 (golden ratio)
195
- β”‚ Fusion rules: tauβŠ—tau β†’ {vacuum, tau}
196
- β”œβ”€β”€ ftb.rs Fibonacci-Taylor Braid synthesis [RESEARCH_HYPOTHESIS]
197
- β”œβ”€β”€ gitc.rs Governance Invariant Topological Cycle
198
- β”œβ”€β”€ emulator_6052.rs Cycle-accurate 6052 emulator Β· MAX_CYCLE hard budget
199
- └── benchmarks.rs Bell Β· GHZ Β· Teleportation Β· Deutsch Β· Grover Β· QFT
200
- ```
201
-
202
- Reference circuits:
203
-
204
- ```
205
- Circuit Qubits Gates Expected state
206
- ──────────── ────── ───── ──────────────────────────
207
- Bell 2 2 (|00⟩ + |11⟩) / √2
208
- GHZ-3 3 3 (|000⟩ + |111⟩) / √2
209
- Teleportation 3 7 State transfer protocol
210
- Deutsch-Jozsa 2 5 Constant/balanced oracle
211
- Grover-2Q 2 12 Amplitude amplification
212
- QFT-3Q 3 10 Quantum Fourier Transform
213
- ────────────────────────────────────────────────────────
214
- 14/14 tests PASS Β· all circuits SUCCESS
215
- ```
216
-
217
- ---
218
-
219
- ## Formal Verification Layer
220
-
221
- ```
222
- runtime/quantum/
223
- β”œβ”€β”€ QuantumSpec.agda Dependent-type specification
224
- β”‚ Transition s s' encoded in the TYPE
225
- β”‚ Illegal transitions: unrepresentable
226
- β”‚
227
- β”œβ”€β”€ QuantumInvariants.lean 13 machine-checked invariants
228
- β”‚ INV-1: norm preserved by unitary gates
229
- β”‚ INV-3: cycle counter strictly monotone
230
- β”‚ INV-4: FSM confined to DAG edges
231
- β”‚ INV-5: Halted/CycleLimit absorbing βœ“
232
- β”‚ INV-7: agent qubit ownership disjoint
233
- β”‚ INV-9: Fibonacci fusion rules correct
234
- β”‚ INV-12: GITC invariant_holds iff all checks pass
235
- β”‚ ... 13 total Β· 0 sorry
236
- β”‚
237
- └── QuantumReference.fs F# executable reference backend
238
- 7 conformance tests
239
- Bell state Β· FSM terminal Β· ownership
240
- ```
241
-
242
- The key post-quantum security property (ADR-002):
243
-
244
- ```
245
- theorem state_preservation :
246
- Step P (l₁, s₁) (lβ‚‚, sβ‚‚) β†’ s₁ = sβ‚‚
247
-
248
- The governance layer is FORMALLY INERT with respect to state.
249
- A quantum adversary with full control of the navigator
250
- CANNOT touch the cryptographic state.
251
- Not policy. TYPE.
252
- ```
253
-
254
- ---
255
-
256
- ## Trust Gate Invariants
257
-
258
- ```
259
- ╔═══════════════════════════════════════════════════════════╗
260
- β•‘ GATE RULE BLOCKS β•‘
261
- ╠═══════════════════════════════════════════════════════════╣
262
- β•‘ Entropy entropy ≀ 0.20 Acting on noise β•‘
263
- β•‘ Writhe W(Ξ²) β‰₯ 2 Incomplete transfer β•‘
264
- β•‘ Reidemeister σ·σ⁻¹ rejected Fake crossings β•‘
265
- β•‘ V1 Trust active ≑ trusted Untrusted execution β•‘
266
- β•‘ Absorbing Halted stays Halted Re-entry after HALT β•‘
267
- β•‘ Cycle cycle ≀ max_cycle Infinite loops β•‘
268
- β•šβ•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•
269
- ```
270
-
271
- ---
272
-
273
- ## Repository Structure
274
-
275
- ```
276
- carry-agent/
277
- β”‚
278
- β”œβ”€β”€ Cargo.toml carry-fsm crate (AGPL-3.0)
279
- β”‚
280
- β”œβ”€β”€ runtime/
281
- β”‚ β”œβ”€β”€ carry-fsm.rs Core FSM library (7-state DAG)
282
- β”‚ β”œβ”€β”€ braid.rs B₃ braid topology module
283
- β”‚ β”œβ”€β”€ main.rs carry-cli binary
284
- β”‚ β”‚
285
- β”‚ └── quantum/ β—€ SOVEREIGN QUANTUM SIMULATOR
286
- β”‚ β”œβ”€β”€ core.rs StateVector + DensityMatrix + gates
287
- β”‚ β”œβ”€β”€ fsm.rs Quantum governance FSM
288
- β”‚ β”œβ”€β”€ agents.rs Primary/partner agent pairs
289
- β”‚ β”œβ”€β”€ dag.rs Execution DAG + provenance
290
- β”‚ β”œβ”€β”€ icp.rs Integrity Constraint Protocol
291
- β”‚ β”œβ”€β”€ asp.rs ASP constraint solver
292
- β”‚ β”œβ”€β”€ topological.rs Fibonacci anyon simulator
293
- β”‚ β”œβ”€β”€ ftb.rs Fibonacci-Taylor Braids [HYPOTHESIS]
294
- β”‚ β”œβ”€β”€ gitc.rs Governance Invariant Topological Cycle
295
- β”‚ β”œβ”€β”€ emulator_6052.rs Cycle-accurate 6052 emulator
296
- β”‚ β”œβ”€β”€ benchmarks.rs Reference circuit suite
297
- β”‚ β”œβ”€β”€ mod.rs Module root
298
- β”‚ β”‚
299
- β”‚ β”œβ”€β”€ QuantumSpec.agda β—€ Dependent-type spec (Agda)
300
- β”‚ β”œβ”€β”€ QuantumInvariants.lean β—€ 13 invariants, 0 sorry (Lean 4)
301
- β”‚ └── QuantumReference.fs β—€ F# conformance backend
302
- β”‚
303
- β”œβ”€β”€ kernels/
304
- β”‚ β”œβ”€β”€ carry-kernel.pl Original Prolog transition table
305
- β”‚ └── tau-prolog/
306
- β”‚ β”œβ”€β”€ braid_kernel.pl Braid logic engine (ISO Prolog)
307
- β”‚ └── crossing_table.pl Crossing-to-DAG lookup
308
- β”‚
309
- β”œβ”€β”€ logic/
310
- β”‚ └── constraint-graph.xml Constraint graph specification
311
- β”‚
312
- β”œβ”€β”€ modules/
313
- β”‚ └── carry-manifest.json Full manifest (layers, DAG, rules)
314
- β”‚
315
- └── docs/
316
- β”œβ”€β”€ firecarry.png Avatar
317
- β”œβ”€β”€ carry_brand_banner.png Architecture diagram
318
- β”œβ”€β”€ braid_animation.svg Animated braid crossing proof
319
- └── CARRY_ARCHITECTURE.md Architecture specification
320
- ```
321
-
322
- ---
323
-
324
- ## Run It
325
-
326
- ```bash
327
- # Full pipeline (FSM + braid proof)
328
- cargo run --bin carry-cli
329
-
330
- # Quantum benchmark suite
331
- cargo run --bin carry-cli -- quantum benchmark
332
-
333
- # Quantum governance verification (ICP + ASP)
334
- cargo run --bin carry-cli -- quantum verify
335
-
336
- # Fibonacci anyon topological simulation
337
- cargo run --bin carry-cli -- quantum topology
338
-
339
- # All 14 tests
340
- cargo test
341
-
342
- # Inspect FSM state
343
- cargo run --bin carry-cli -- quantum inspect
344
- ```
345
-
346
- Expected output:
347
-
348
- ```
349
- ═══════════════════════════════════════════════════════════════
350
- CARRY PIPELINE: BOTH PROOFS DISCHARGE
351
- FSM: DETERMINISTIC_COMPILATION_COMPLETE
352
- BRAID: INVARIANT_HOLDS (writhe=2, C3 at pos 0)
353
- ═══════════════════════════════════════════════════════════════
354
-
355
- β”Œβ”€ QUANTUM BENCHMARK SUITE ──────────────────────────────────┐
356
- Circuit: Bell Qubits: 2 | Gates: 2 | Status: SUCCESS
357
- Circuit: GHZ-3 Qubits: 3 | Gates: 3 | Status: SUCCESS
358
- Circuit: Teleportation Qubits: 3 | Gates: 7 | Status: SUCCESS
359
- Circuit: Deutsch Qubits: 2 | Gates: 5 | Status: SUCCESS
360
- Circuit: Grover-2Q Qubits: 2 | Gates: 12 | Status: SUCCESS
361
- Circuit: QFT-3Q Qubits: 3 | Gates: 10 | Status: SUCCESS
362
- ═══════════════════════════════════════════════════════════════
363
- ```
364
-
365
- ---
366
-
367
- ## The Math
368
-
369
- **B₃ braid group** β€” generators σ₁, Οƒβ‚‚, Yang-Baxter:
370
-
371
- ```
372
- σ₁ Β· Οƒβ‚‚ Β· σ₁ = Οƒβ‚‚ Β· σ₁ Β· Οƒβ‚‚
373
- ```
374
-
375
- **Writhe invariant** for canonical pipeline Ξ² = Οƒβ‚‚ Β· σ₁:
376
-
377
- ```
378
- W(Ξ²) = (+1) + (+1) = +2
379
- Ο€(Ξ²): C3 β†’ position 0
380
- Invariant: W(Ξ²) β‰₯ 2 ∧ Ο€(Ξ²)(C3) = 0
381
- ```
382
-
383
- **Fibonacci anyons** β€” golden ratio quantum dimension:
384
-
385
- ```
386
- Ο† = (1 + √5) / 2 β‰ˆ 1.6180
387
- tau βŠ— tau β†’ vacuum w.p. 1/φ² β‰ˆ 0.382
388
- tau βŠ— tau β†’ tau w.p. 1 - 1/φ² β‰ˆ 0.618
389
- ```
390
-
391
- **Zβ‚‚ duality** (proved in Lean 4 + Agda, from order-of-symmetry):
392
-
393
- ```
394
- D ∘ D = id (duality is an involution)
395
- D(P) β‰  P (no fixed points β€” orbit size exactly 2)
396
- GOTO ↔ COME-FROM (structural mirrors, Zβ‚‚ group of order 2)
397
- ```
398
-
399
- **State preservation** (proved, 0 sorry):
400
-
401
- ```
402
- Step P (l₁, s₁) (lβ‚‚, sβ‚‚) β†’ s₁ = sβ‚‚
403
- The navigator cannot touch the payload. By type. Not by policy.
404
- ```
405
-
406
- ---
407
-
408
- ```
409
- ╔═════════════════════════════════════════════╗
410
- β•‘ CARRY: The adversarial twin that proves β•‘
411
- β•‘ your pipeline is honest. β•‘
412
- β•‘ β•‘
413
- β•‘ The compiler says it runs. β•‘
414
- β•‘ The braid says it's real. β•‘
415
- β•‘ The Lean proof says it stays real. β•‘
416
- β•šβ•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•
417
- ```
418
-
419
- ---
420
-
421
- ## License
422
-
423
- AGPL-3.0-only
424
- Copyright (C) 2026 Ahmad Ali Parr, Jessica L. Williams / SNAPKITTYWEST
425
-
426
- <p align="center">
427
- <img src="docs/firecarry.png" alt="Firecarry" width="80px" />
428
- </p>
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ ---
2
+ license: agpl-3.0
3
+ tags:
4
+ - snapkitty
5
+ ---
6
+
7
+ > Source: [github.com/SNAPKITTYWEST/carry-agent](https://github.com/SNAPKITTYWEST/carry-agent)
8
+
9
+ <p align="center">
10
+ <img src="docs/firecarry.png" alt="CARRY β€” CARTO's Evil Twin Made of Curry" width="360px" />
11
+ </p>
12
+
13
+ <h1 align="center">CARRY</h1>
14
+ <h3 align="center">Adversarial Twin of CARTO</h3>
15
+
16
+ <p align="center">
17
+ <strong>CURRY_CRYSTAL_C3 Triad + Braid Topology + Sovereign Quantum Simulator</strong><br />
18
+ 7-state DAG-locked pipeline Β· Entropy-gated transitions Β· Tau-Prolog logic kernel<br />
19
+ Fibonacci anyons Β· ICP governance Β· BLAKE3 WORM audit chain<br />
20
+ <em>The FSM tells you WHERE you are. The braid tells you WHETHER you got there honestly.</em>
21
+ </p>
22
+
23
+ <p align="center">
24
+ <img src="https://img.shields.io/badge/lang-Rust-orange?style=flat-square" />
25
+ <img src="https://img.shields.io/badge/logic-Tau--Prolog-blue?style=flat-square" />
26
+ <img src="https://img.shields.io/badge/proof-Braid_B₃-purple?style=flat-square" />
27
+ <img src="https://img.shields.io/badge/quantum-Fibonacci_Anyons-cyan?style=flat-square" />
28
+ <img src="https://img.shields.io/badge/formal-Lean_4_%2B_Agda-blueviolet?style=flat-square" />
29
+ <img src="https://img.shields.io/badge/tests-14%2F14_PASS-brightgreen?style=flat-square" />
30
+ <img src="https://img.shields.io/badge/sorry-0-brightgreen?style=flat-square" />
31
+ <img src="https://img.shields.io/badge/license-AGPL--3.0-green?style=flat-square" />
32
+ </p>
33
+
34
+ ---
35
+
36
+ <p align="center">
37
+ <img src="docs/carry_brand_banner.png" alt="CARRY FSM β€” Adversarial Twin System + Deterministic Compiler Engine" width="100%" />
38
+ </p>
39
+
40
+ ---
41
+
42
+ ```
43
+ β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•— β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•— β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•— β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•— β–ˆβ–ˆβ•— β–ˆβ–ˆβ•—
44
+ β–ˆβ–ˆβ•”β•β•β•β•β•β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•—β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•—β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•—β•šβ–ˆβ–ˆβ•— β–ˆβ–ˆβ•”β•
45
+ β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•‘β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•”β•β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•”β• β•šβ–ˆβ–ˆβ–ˆβ–ˆβ•”β•
46
+ β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•‘β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•—β–ˆβ–ˆβ•”β•β•β–ˆβ–ˆβ•— β•šβ–ˆβ–ˆβ•”β•
47
+ β•šβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ•—β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•‘β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•‘β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•‘ β–ˆβ–ˆβ•‘
48
+ β•šβ•β•β•β•β•β•β•šβ•β• β•šβ•β•β•šβ•β• β•šβ•β•β•šβ•β• β•šβ•β• β•šβ•β•
49
+
50
+ ╔═══════════════════════════════════════════════╗
51
+ β•‘ B R A I D T O P O L O G Y R U N T I M E β•‘
52
+ β•‘ σ₁ Β· Οƒβ‚‚ Β· σ₁ = Οƒβ‚‚ Β· σ₁ Β· Οƒβ‚‚ β•‘
53
+ β•‘ Yang-Baxter holds. The chain is honest. β•‘
54
+ β•šβ•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•
55
+
56
+ strand 0 ──╲ ╱── Οƒβ‚‚ crossing
57
+ strand 1 β•²β•±
58
+ β•±β•²
59
+ strand 2 ──╱ ╲── σ₁ crossing
60
+ β”‚
61
+ β–Ό
62
+ [C3 at pos 0]
63
+ writhe = +2
64
+ INVARIANT HOLDS
65
+ ```
66
+
67
+ ---
68
+
69
+ ## What Is CARRY?
70
+
71
+ CARRY is the **adversarial twin** of [CARTO](https://github.com/SNAPKITTYWEST/cartographer-agent).
72
+
73
+ **CARTO** is the sovereign mapping agent β€” it models terrain, constructs pipelines, and produces outputs it claims are valid.
74
+
75
+ **CARRY** attacks those outputs. If CARRY cannot break CARTO's pipeline, the pipeline is honest. CARRY is the red team that never sleeps β€” a formal adversary baked into the architecture itself rather than run as a separate audit process.
76
+
77
+ The relationship:
78
+
79
+ ```
80
+ CARTO CARRY
81
+ ───── ─────
82
+ Maps terrain ←→ Attacks the map
83
+ Claims pipeline is valid ←→ Tries to falsify the claim
84
+ Produces WORM output ←→ Verifies the WORM seal
85
+ GOTO (push semantics) ←→ COME-FROM (pull semantics)
86
+ Forward evolution (U) ←→ Reversed evolution (U†)
87
+ ```
88
+
89
+ The braid topology encodes this duality formally: every GOTO crossing has a matching COME-FROM crossing. The writhe invariant proves that authority was transferred through the correct sequence of crossings β€” not just that it arrived at the right place, but that it took the right path.
90
+
91
+ If the path is wrong, the braid is wrong. If the braid is wrong, the proof is rejected. No exceptions.
92
+
93
+ ---
94
+
95
+ ## Braid Authority Transfer
96
+
97
+ ```
98
+ INITIAL: Curry ──── Crystal ──── C3
99
+ [0] [1] [2] (authority = pos 0)
100
+
101
+ After Οƒβ‚‚: Curry ──── C3 ──── Crystal
102
+ [0] [1] [2] (C3 crosses OVER Crystal)
103
+
104
+ After σ₁: C3 ──── Curry ──── Crystal
105
+ [0] [1] [2] (C3 crosses OVER Curry)
106
+
107
+ Writhe W(Ξ²) = (+1) + (+1) = +2
108
+ C3 at position 0 β†’ AUTHORITY TRANSFERRED
109
+ INVARIANT HOLDS βœ“
110
+ ```
111
+
112
+ ```
113
+ BRAID WORD: Οƒβ‚‚ Β· σ₁
114
+ ─────────────────────
115
+ Curry ────\────────────────
116
+ \
117
+ Crystal ────X──\────────── Οƒβ‚‚: C3 over Crystal
118
+ / \
119
+ C3 ─────── /────X──────── σ₁: C3 over Curry
120
+ \
121
+ β–Ό
122
+ C3 at pos 0
123
+ W = +2 βœ“
124
+ ```
125
+
126
+ ---
127
+
128
+ ## Architecture
129
+
130
+ ```
131
+ ╔══════════════════════════════════════════════════════════════╗
132
+ β•‘ CARRY STACK β•‘
133
+ ╠══════════════════════════════════════════════════════════════╣
134
+ β•‘ FORMAL LAYER Lean 4 + Agda β•‘
135
+ β•‘ 13 invariants Β· 0 sorry β•‘
136
+ β•‘ state_preservation proved β•‘
137
+ β•‘ duality_involution proved β•‘
138
+ ╠══════════════════════════════════════════════════════════════╣
139
+ β•‘ QUANTUM LAYER Fibonacci Anyon Simulator β•‘
140
+ β•‘ B₃ braid group Β· Ο† = 1.6180 β•‘
141
+ β•‘ StateVector + DensityMatrix engines β•‘
142
+ β•‘ ICP 6-stage governance pipeline β•‘
143
+ β•‘ ASP declarative constraint solver β•‘
144
+ β•‘ 6052 cycle-accurate emulator β•‘
145
+ ╠══════════════════════════════════════════════════════════════╣
146
+ β•‘ GOVERNANCE LAYER Conditional Dual DAG β•‘
147
+ β•‘ GOTO ↔ COME-FROM duality β•‘
148
+ β•‘ state preserved across ALL transitions β•‘
149
+ β•‘ BLAKE3 WORM audit chain β•‘
150
+ ╠══════════════════════════════════════════════════════════════╣
151
+ β•‘ RUNTIME LAYER Rust (carry-fsm crate) β•‘
152
+ β•‘ 7-state DAG-locked FSM β•‘
153
+ β•‘ Entropy ≀ 0.20 gate β•‘
154
+ β•‘ Tau-Prolog logic kernel β•‘
155
+ β•šβ•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•
156
+ ```
157
+
158
+ ---
159
+
160
+ ## 7-State Quantum FSM
161
+
162
+ ```
163
+ β”Œβ”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”
164
+ β”‚ INIT │───▢│ PREPARE │───▢│ ENTANGLE │───▢│ COMPUTE β”‚
165
+ β””β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”¬β”€β”€β”€β”€β”˜
166
+ β”‚
167
+ β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β” β”‚
168
+ β”‚ COMMIT │◀───│ VERIFY │◀───│MEASURE β”‚β—€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜
169
+ β””β”€β”€β”€β”¬β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”˜
170
+ β”‚
171
+ └──▢ PREPARE (loop) ─── or ─── COMMIT (terminal)
172
+
173
+ Any state ──▢ HALTED (emergency)
174
+ Any state ──▢ CYCLE_LIMIT (budget exhausted, absorbing)
175
+
176
+ Theorem (Lean 4, zero sorry):
177
+ Halted and CYCLE_LIMIT are ABSORBING STATES.
178
+ No transition exits them. Ever.
179
+ ```
180
+
181
+ ---
182
+
183
+ ## The Quantum Module
184
+
185
+ CARRY ships a full first-principles quantum simulator:
186
+
187
+ ```
188
+ runtime/quantum/
189
+ β”œβ”€β”€ core.rs StateVector |ψ⟩ + DensityMatrix ρ engines
190
+ β”‚ Born rule measurement Β· noise models
191
+ β”‚ H X Y Z S T Rx Ry Rz CNOT CZ SWAP
192
+ β”œβ”€β”€ fsm.rs 7-state governance FSM (proved absorbing terminals)
193
+ β”œβ”€β”€ agents.rs Primary + Partner agent pairs
194
+ β”‚ Qubit ownership: pairwise disjoint (proved INV-7)
195
+ β”œβ”€β”€ dag.rs Execution DAG + provenance hash chain
196
+ β”œβ”€β”€ icp.rs Integrity Constraint Protocol
197
+ │ 6 stages: Setup→Observe→Validate→Check→Execute→Verify
198
+ β”‚ HALT on any constraint breach
199
+ β”œβ”€β”€ asp.rs Answer Set Programming constraint solver
200
+ β”‚ QubitControl Β· Entangled Β· AgentControls rules
201
+ β”œβ”€β”€ topological.rs Fibonacci anyon simulator
202
+ β”‚ B₃: σ₁ Οƒβ‚‚ σ₁⁻¹ σ₂⁻¹ Β· Ο† β‰ˆ 1.6180 (golden ratio)
203
+ β”‚ Fusion rules: tauβŠ—tau β†’ {vacuum, tau}
204
+ β”œβ”€β”€ ftb.rs Fibonacci-Taylor Braid synthesis [RESEARCH_HYPOTHESIS]
205
+ β”œβ”€β”€ gitc.rs Governance Invariant Topological Cycle
206
+ β”œβ”€β”€ emulator_6052.rs Cycle-accurate 6052 emulator Β· MAX_CYCLE hard budget
207
+ └── benchmarks.rs Bell Β· GHZ Β· Teleportation Β· Deutsch Β· Grover Β· QFT
208
+ ```
209
+
210
+ Reference circuits:
211
+
212
+ ```
213
+ Circuit Qubits Gates Expected state
214
+ ──────────── ────── ───── ──────────────────────────
215
+ Bell 2 2 (|00⟩ + |11⟩) / √2
216
+ GHZ-3 3 3 (|000⟩ + |111⟩) / √2
217
+ Teleportation 3 7 State transfer protocol
218
+ Deutsch-Jozsa 2 5 Constant/balanced oracle
219
+ Grover-2Q 2 12 Amplitude amplification
220
+ QFT-3Q 3 10 Quantum Fourier Transform
221
+ ────────────────────────────────────────────────────────
222
+ 14/14 tests PASS Β· all circuits SUCCESS
223
+ ```
224
+
225
+ ---
226
+
227
+ ## Formal Verification Layer
228
+
229
+ ```
230
+ runtime/quantum/
231
+ β”œβ”€β”€ QuantumSpec.agda Dependent-type specification
232
+ β”‚ Transition s s' encoded in the TYPE
233
+ β”‚ Illegal transitions: unrepresentable
234
+ β”‚
235
+ β”œβ”€β”€ QuantumInvariants.lean 13 machine-checked invariants
236
+ β”‚ INV-1: norm preserved by unitary gates
237
+ β”‚ INV-3: cycle counter strictly monotone
238
+ β”‚ INV-4: FSM confined to DAG edges
239
+ β”‚ INV-5: Halted/CycleLimit absorbing βœ“
240
+ β”‚ INV-7: agent qubit ownership disjoint
241
+ β”‚ INV-9: Fibonacci fusion rules correct
242
+ β”‚ INV-12: GITC invariant_holds iff all checks pass
243
+ β”‚ ... 13 total Β· 0 sorry
244
+ β”‚
245
+ └── QuantumReference.fs F# executable reference backend
246
+ 7 conformance tests
247
+ Bell state Β· FSM terminal Β· ownership
248
+ ```
249
+
250
+ The key post-quantum security property (ADR-002):
251
+
252
+ ```
253
+ theorem state_preservation :
254
+ Step P (l₁, s₁) (lβ‚‚, sβ‚‚) β†’ s₁ = sβ‚‚
255
+
256
+ The governance layer is FORMALLY INERT with respect to state.
257
+ A quantum adversary with full control of the navigator
258
+ CANNOT touch the cryptographic state.
259
+ Not policy. TYPE.
260
+ ```
261
+
262
+ ---
263
+
264
+ ## Trust Gate Invariants
265
+
266
+ ```
267
+ ╔═══════════════════════════════════════════════════════════╗
268
+ β•‘ GATE RULE BLOCKS β•‘
269
+ ╠═══════════════════════════════════════════════════════════╣
270
+ β•‘ Entropy entropy ≀ 0.20 Acting on noise β•‘
271
+ β•‘ Writhe W(Ξ²) β‰₯ 2 Incomplete transfer β•‘
272
+ β•‘ Reidemeister σ·σ⁻¹ rejected Fake crossings β•‘
273
+ β•‘ V1 Trust active ≑ trusted Untrusted execution β•‘
274
+ β•‘ Absorbing Halted stays Halted Re-entry after HALT β•‘
275
+ β•‘ Cycle cycle ≀ max_cycle Infinite loops β•‘
276
+ β•šβ•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•
277
+ ```
278
+
279
+ ---
280
+
281
+ ## Repository Structure
282
+
283
+ ```
284
+ carry-agent/
285
+ β”‚
286
+ β”œβ”€β”€ Cargo.toml carry-fsm crate (AGPL-3.0)
287
+ β”‚
288
+ β”œβ”€β”€ runtime/
289
+ β”‚ β”œβ”€β”€ carry-fsm.rs Core FSM library (7-state DAG)
290
+ β”‚ β”œβ”€β”€ braid.rs B₃ braid topology module
291
+ β”‚ β”œβ”€β”€ main.rs carry-cli binary
292
+ β”‚ β”‚
293
+ β”‚ └── quantum/ β—€ SOVEREIGN QUANTUM SIMULATOR
294
+ β”‚ β”œβ”€β”€ core.rs StateVector + DensityMatrix + gates
295
+ β”‚ β”œβ”€β”€ fsm.rs Quantum governance FSM
296
+ β”‚ β”œβ”€β”€ agents.rs Primary/partner agent pairs
297
+ β”‚ β”œβ”€β”€ dag.rs Execution DAG + provenance
298
+ β”‚ β”œβ”€β”€ icp.rs Integrity Constraint Protocol
299
+ β”‚ β”œβ”€β”€ asp.rs ASP constraint solver
300
+ β”‚ β”œβ”€β”€ topological.rs Fibonacci anyon simulator
301
+ β”‚ β”œβ”€β”€ ftb.rs Fibonacci-Taylor Braids [HYPOTHESIS]
302
+ β”‚ β”œβ”€β”€ gitc.rs Governance Invariant Topological Cycle
303
+ β”‚ β”œβ”€β”€ emulator_6052.rs Cycle-accurate 6052 emulator
304
+ β”‚ β”œβ”€β”€ benchmarks.rs Reference circuit suite
305
+ β”‚ β”œβ”€β”€ mod.rs Module root
306
+ β”‚ β”‚
307
+ β”‚ β”œβ”€β”€ QuantumSpec.agda β—€ Dependent-type spec (Agda)
308
+ β”‚ β”œβ”€β”€ QuantumInvariants.lean β—€ 13 invariants, 0 sorry (Lean 4)
309
+ β”‚ └── QuantumReference.fs β—€ F# conformance backend
310
+ β”‚
311
+ β”œβ”€β”€ kernels/
312
+ β”‚ β”œβ”€β”€ carry-kernel.pl Original Prolog transition table
313
+ β”‚ └── tau-prolog/
314
+ β”‚ β”œβ”€β”€ braid_kernel.pl Braid logic engine (ISO Prolog)
315
+ β”‚ └── crossing_table.pl Crossing-to-DAG lookup
316
+ β”‚
317
+ β”œβ”€β”€ logic/
318
+ β”‚ └── constraint-graph.xml Constraint graph specification
319
+ β”‚
320
+ β”œβ”€β”€ modules/
321
+ β”‚ └── carry-manifest.json Full manifest (layers, DAG, rules)
322
+ β”‚
323
+ └── docs/
324
+ β”œβ”€β”€ firecarry.png Avatar
325
+ β”œβ”€β”€ carry_brand_banner.png Architecture diagram
326
+ β”œβ”€β”€ braid_animation.svg Animated braid crossing proof
327
+ └── CARRY_ARCHITECTURE.md Architecture specification
328
+ ```
329
+
330
+ ---
331
+
332
+ ## Run It
333
+
334
+ ```bash
335
+ # Full pipeline (FSM + braid proof)
336
+ cargo run --bin carry-cli
337
+
338
+ # Quantum benchmark suite
339
+ cargo run --bin carry-cli -- quantum benchmark
340
+
341
+ # Quantum governance verification (ICP + ASP)
342
+ cargo run --bin carry-cli -- quantum verify
343
+
344
+ # Fibonacci anyon topological simulation
345
+ cargo run --bin carry-cli -- quantum topology
346
+
347
+ # All 14 tests
348
+ cargo test
349
+
350
+ # Inspect FSM state
351
+ cargo run --bin carry-cli -- quantum inspect
352
+ ```
353
+
354
+ Expected output:
355
+
356
+ ```
357
+ ═══════════════════════════════════════════════════════════════
358
+ CARRY PIPELINE: BOTH PROOFS DISCHARGE
359
+ FSM: DETERMINISTIC_COMPILATION_COMPLETE
360
+ BRAID: INVARIANT_HOLDS (writhe=2, C3 at pos 0)
361
+ ═══════════════════════════════════════════════════════════════
362
+
363
+ β”Œβ”€ QUANTUM BENCHMARK SUITE ──────────────────────────────────┐
364
+ Circuit: Bell Qubits: 2 | Gates: 2 | Status: SUCCESS
365
+ Circuit: GHZ-3 Qubits: 3 | Gates: 3 | Status: SUCCESS
366
+ Circuit: Teleportation Qubits: 3 | Gates: 7 | Status: SUCCESS
367
+ Circuit: Deutsch Qubits: 2 | Gates: 5 | Status: SUCCESS
368
+ Circuit: Grover-2Q Qubits: 2 | Gates: 12 | Status: SUCCESS
369
+ Circuit: QFT-3Q Qubits: 3 | Gates: 10 | Status: SUCCESS
370
+ ═══════════════════════════════════════════════════════════════
371
+ ```
372
+
373
+ ---
374
+
375
+ ## The Math
376
+
377
+ **B₃ braid group** β€” generators σ₁, Οƒβ‚‚, Yang-Baxter:
378
+
379
+ ```
380
+ σ₁ Β· Οƒβ‚‚ Β· σ₁ = Οƒβ‚‚ Β· σ₁ Β· Οƒβ‚‚
381
+ ```
382
+
383
+ **Writhe invariant** for canonical pipeline Ξ² = Οƒβ‚‚ Β· σ₁:
384
+
385
+ ```
386
+ W(Ξ²) = (+1) + (+1) = +2
387
+ Ο€(Ξ²): C3 β†’ position 0
388
+ Invariant: W(Ξ²) β‰₯ 2 ∧ Ο€(Ξ²)(C3) = 0
389
+ ```
390
+
391
+ **Fibonacci anyons** β€” golden ratio quantum dimension:
392
+
393
+ ```
394
+ Ο† = (1 + √5) / 2 β‰ˆ 1.6180
395
+ tau βŠ— tau β†’ vacuum w.p. 1/φ² β‰ˆ 0.382
396
+ tau βŠ— tau β†’ tau w.p. 1 - 1/φ² β‰ˆ 0.618
397
+ ```
398
+
399
+ **Zβ‚‚ duality** (proved in Lean 4 + Agda, from order-of-symmetry):
400
+
401
+ ```
402
+ D ∘ D = id (duality is an involution)
403
+ D(P) β‰  P (no fixed points β€” orbit size exactly 2)
404
+ GOTO ↔ COME-FROM (structural mirrors, Zβ‚‚ group of order 2)
405
+ ```
406
+
407
+ **State preservation** (proved, 0 sorry):
408
+
409
+ ```
410
+ Step P (l₁, s₁) (lβ‚‚, sβ‚‚) β†’ s₁ = sβ‚‚
411
+ The navigator cannot touch the payload. By type. Not by policy.
412
+ ```
413
+
414
+ ---
415
+
416
+ ```
417
+ ╔═════════════════════════════════════════════╗
418
+ β•‘ CARRY: The adversarial twin that proves β•‘
419
+ β•‘ your pipeline is honest. β•‘
420
+ β•‘ β•‘
421
+ β•‘ The compiler says it runs. β•‘
422
+ β•‘ The braid says it's real. β•‘
423
+ β•‘ The Lean proof says it stays real. β•‘
424
+ β•šβ•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•β•
425
+ ```
426
+
427
+ ---
428
+
429
+ ## License
430
+
431
+ AGPL-3.0-only
432
+ Copyright (C) 2026 Ahmad Ali Parr, Jessica L. Williams / SNAPKITTYWEST
433
+
434
+ <p align="center">
435
+ <img src="docs/firecarry.png" alt="Firecarry" width="80px" />
436
+ </p>
437
+
438
+ ### πŸ’Ό Commercial License
439
+
440
+ Snapkitty code is free and open under **AGPL-3.0** for open-source use. Building a commercial product or service? A **proprietary commercial license** from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.
441
+
442
+ **[β†’ Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20carry-agent)** Β· A.parr@belespritdaccord.uk