1.42 MB

Ctrl+K

1 contributor

History: 9 commits

phanerozoic

Put the organism first and move serialization, sizes and the Rocq map to appendices

5ee1fb5 9 days ago

extract
Prove the paper's counts, levelization, depth bounds, recipe lengths and Section 6 in Rocq, and revise the paper 9 days ago
Abstract.v

24.9 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Adder.v

6.08 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
AmpHost.v

19.9 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Assumptions.v

6.53 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
BlockLev.v

32.9 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Choose.v

7.94 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Compile.v

5.18 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Complete.v

4.72 kB
Replace the interpreter sections with the two-head machine and translating organism proved in Rocq, prove the hosted constructor in full, compute the restoration bound in C, add independent reproductions of the paper's constructions and measurements, and cut the paper to 36 pages 11 days ago
Decoder.v

52.5 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Device.v

3.87 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Erfc.v

22.7 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
ExtrNat.v

1.73 kB
Prove the paper's counts, levelization, depth bounds, recipe lengths and Section 6 in Rocq, and revise the paper 9 days ago
Extract.v

245 Bytes
Prove the paper's counts, levelization, depth bounds, recipe lengths and Section 6 in Rocq, and revise the paper 9 days ago
ExtractHost.v

244 Bytes
Prove the paper's counts, levelization, depth bounds, recipe lengths and Section 6 in Rocq, and revise the paper 9 days ago
ExtractStored.v

240 Bytes
Prove the paper's counts, levelization, depth bounds, recipe lengths and Section 6 in Rocq, and revise the paper 9 days ago
FlipLower.v

12.8 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
FoldHost.v

29.8 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Gates.v

3.75 kB
Replace the interpreter sections with the two-head machine and translating organism proved in Rocq, prove the hosted constructor in full, compute the restoration bound in C, add independent reproductions of the paper's constructions and measurements, and cut the paper to 36 pages 11 days ago
Host.v

7.64 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
HostCount.v

24.5 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
HostIP.v

17.8 kB
Prove the stored host's construction, copies, period and network in Rocq for every word width, give each unit its own window cell, and revise Section 8 with the new records 10 days ago
HostLev.v

57.6 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
HostSem.v

27.3 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
HostWF.v

15.8 kB
Prove in Rocq that the host family computes SUBLEQ at every word width, check the stored host's startup and step records on decision diagrams, state the stored-host theorems for every stored host with their overhead, bound self-reproduction under noise, remove the neuromorphic mappings, and cut the paper to 30 pages 11 days ago
Indep.v

9.29 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Lev.v

39.8 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Lower.v

15 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Main.v

14.6 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Margin.v

47 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Net.v

13.8 kB
Replace the interpreter sections with the two-head machine and translating organism proved in Rocq, prove the hosted constructor in full, compute the restoration bound in C, add independent reproductions of the paper's constructions and measurements, and cut the paper to 36 pages 11 days ago
NetMain.v

1.41 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Noise.v

56.8 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
NoiseNum.v

6.53 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Organism.v

4.99 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
PassCheck.v

4.01 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
PassLemma.v

10.9 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Phys.v

9.52 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
PhysFacts.v

4.17 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
PhysLev.v

64.1 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
PhysMain.v

1.55 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
PhysSem.v

70.5 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
PhysWF.v

21.2 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Pstar.v

58.7 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Recipe.v

19.3 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Restore.v

90.5 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Run.v

26.7 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Schedule.v

13.4 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago
Spec.v

4.19 kB
Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper 11 days ago
Stored.v

10.1 kB
Put the organism first and move serialization, sizes and the Rocq map to appendices 9 days ago