Enter Calculus - A Reproducible Computational Artefact: Companion artefact for Enter Calculus
Le résumé fourni par la source
This document specifies a reproducible computational artefact accompanying the Enter calculus. The implementation provides an executable model of strictly linear typing, configurations, operational reduction, abstract measurement strategies, decohered fine-graining, the operational Born-rule derivation, generalized measurements, single-level reflection, sharp measurement contexts, and the record-free Walsh-slack problem. The artefact combines deterministic regression tests, executable claim checkers, property-based generation of well-typed terms, and a standalone random-fuzzing layer. It is a testing and falsification artefact rather than a machine-checked proof: universal statements in the paper remain mathematical theorems and would require a proof assistant such as Lean or Coq for formal verification.
Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.