Merge pull request #48 from hyperpolymath/claude/refresh-system-et-row

chore(census): refresh the row of system-et (the Agda track is now on its main branch)

Author: hyperpolymath

docs/atlas/generated/az.adoc

@@ -274,7 +274,7 @@
 * `hyperpolymath/stateful-artefacts` — engineering; 4 own proof files, 23 detected declarations; provers: idris2 2, tla 2
 * `hyperpolymath/statistikles` — theory; 4 own proof files, 22 detected declarations; provers: agda 4
 * `catachresis-colloquium/stealth-glider-ecosystem` — engineering; 1 own proof files, 13 detected declarations; provers: idris2 1
-* `hyperpolymath/system-et` — theory; 21 own proof files, 164 detected declarations; provers: lean 21
+* `hyperpolymath/system-et` — theory; 86 own proof files, 612 detected declarations; provers: agda 65, lean 21
 
 == T
 

docs/atlas/generated/classes.adoc

@@ -43,7 +43,7 @@
 * `hyperpolymath/secret-types` — theory; 21 own proof files, 91 detected declarations; provers: agda 21
 * `hyperpolymath/snifs` — theory; 3 own proof files, 43 detected declarations; provers: agda 2, idris2 1
 * `hyperpolymath/statistikles` — theory; 4 own proof files, 22 detected declarations; provers: agda 4
-* `hyperpolymath/system-et` — theory; 21 own proof files, 164 detected declarations; provers: lean 21
+* `hyperpolymath/system-et` — theory; 86 own proof files, 612 detected declarations; provers: agda 65, lean 21
 * `hyperpolymath/tangle` — theory; 3 own proof files, 61 detected declarations; provers: lean 3
 * `hyperpolymath/trope-checker` — theory; 38 own proof files, 514 detected declarations; provers: agda 10, lean 12, idris2 16
 * `hyperpolymath/tropical-types` — theory; 28 own proof files, 540 detected declarations; provers: lean 19, isabelle 9

docs/atlas/generated/index.json

@@ -199,7 +199,7 @@
 * `hyperpolymath/ssg-collection` — engineering; 23 own proof files, 108 detected declarations; provers: lean 1, idris2 6, spark 13, other 3
 * `hyperpolymath/stateful-artefacts` — engineering; 4 own proof files, 23 detected declarations; provers: idris2 2, tla 2
 * `hyperpolymath/statistikles` — theory; 4 own proof files, 22 detected declarations; provers: agda 4
-* `hyperpolymath/system-et` — theory; 21 own proof files, 164 detected declarations; provers: lean 21
+* `hyperpolymath/system-et` — theory; 86 own proof files, 612 detected declarations; provers: agda 65, lean 21
 * `hyperpolymath/tangle` — theory; 3 own proof files, 61 detected declarations; provers: lean 3
 * `hyperpolymath/thunderbird-template-reloaded` — engineering; 10 own proof files, 74 detected declarations; provers: idris2 10
 * `hyperpolymath/tlaiser` — engineering; 9 own proof files, 181 detected declarations; provers: idris2 9

docs/atlas/generated/organisations.adoc

@@ -22,6 +22,8 @@ verdicts.
 
 |https://github.com/hyperpolymath/echo-types[hyperpolymath/echo-types] |161 |0 |agda 161 |1676 |0 |1 |0 |1 |`PROOF-STATUS.adoc`
 
+|https://github.com/hyperpolymath/system-et[hyperpolymath/system-et] |86 |0 |agda 65, lean 21 |612 |0 |0 |0 |0 |`docs/status/PROOF-STATUS.adoc`
+
 |https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation] |78 |0 |agda 78 |618 |0 |2 |0 |1 |`docs/status/PROOF-NEEDS.adoc`
 
 |https://github.com/hyperpolymath/valence-shell[hyperpolymath/valence-shell] |64 |0 |agda 10, lean 16, rocq 12, isabelle 9, idris2 12, smt-atp 5 |996 |5 |1 |0 |9 |`PROOF-NEEDS.adoc`
@@ -54,8 +56,6 @@ verdicts.
 
 |https://github.com/hyperpolymath/secret-types[hyperpolymath/secret-types] |21 |5 |agda 21 |91 |0 |0 |0 |0 |`PROOF-STATUS.adoc`
 
-|https://github.com/hyperpolymath/system-et[hyperpolymath/system-et] |21 |0 |lean 21 |164 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
-
 |https://github.com/hyperpolymath/occupancy-types[hyperpolymath/occupancy-types] |20 |2 |agda 8, lean 6, idris2 6 |90 |0 |0 |0 |0 |`PROOF-STATUS.adoc`
 
 |https://github.com/hyperpolymath/wokelang[hyperpolymath/wokelang] |18 |0 |lean 7, rocq 3, idris2 8 |418 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
@@ -72,8 +72,6 @@ verdicts.
 
 |https://github.com/hyperpolymath/CompositionalDA.jl[hyperpolymath/CompositionalDA.jl] |15 |0 |agda 15 |63 |0 |1 |0 |0 |`proofs/PROOF-STATUS.md`
 
-|https://github.com/metadatastician/hvn-dehallucinator[metadatastician/hvn-dehallucinator] |16 |7 |agda 10, idris2 1, tla 5 |203 |0 |0 |0 |0 |`docs/status/PROOF-STATUS.adoc`
-
 |https://github.com/hyperpolymath/ExactCounts.jl[hyperpolymath/ExactCounts.jl] |15 |0 |agda 15 |236 |0 |1 |0 |6 |`proofs/PROOF-STATUS.md`
 
 |https://github.com/hyperpolymath/jtv-lang[hyperpolymath/jtv-lang] |15 |0 |agda 5, lean 9, idris2 1 |287 |0 |0 |0 |0 |`verification/PROOF-STATUS.adoc`