From 9f3d6ee987f99925e2c04c895512397cb894cd79 Mon Sep 17 00:00:00 2001 From: J0bot Date: Tue, 25 Aug 2026 17:26:40 +0000 Subject: [PATCH] Initial commit --- README.md | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..d7ae06b --- /dev/null +++ b/README.md @@ -0,0 +1,3 @@ +# ploxion-rocq + +PLOXION · LA BOUCLE qui teste la MATH DU XERBOXION sans LLM (RS-7) → une to-do infinie sur 2 axes. Elle énumère ta math (nombre→forme cubion=x²/spherion=π·x/wormion/portion/bion, collapse vers le ploxion premier, géométrie du kion, les -ion) et la met à l'épreuve : ce qui se vérifie = théorème (preuve formelle Rocq = à faire) · un contre-exemple ou une loi ouverte (kmath n'est pas associatif ; la loi base-π « à dériver ») = À FAIRE côté PREUVE · les -ion pas encore définis = À FAIRE côté GÉNÉRATION. + un vrai noyau de preuve interactif (jOSProof, esprit Rocq, Curry-Howard proof=program) + le savoir Rocq. Moteurs déterministes jOSXermath (20/20) + jOSProof (17/17), lien vers le vrai Rocq. · fournit: rocq, boucle, math-xerboxion, preuve, todo, formel, savoir \ No newline at end of file