commit 9f3d6ee987f99925e2c04c895512397cb894cd79 Author: J0bot Date: Tue Aug 25 17:26:40 2026 +0000 Initial commit 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