BIT-MEI-A2-FORMAL-REL-001: Physics Audit, Typed Calculator A2, and Scoped Lean Refinement for Mass-Energy-Information, T > 0, and Planck-Scale Bounds

BIT-MEI-A2-FORMAL-REL-001 is an independent-research terminal public-audit release concerning a physics audit and typed calculator for mass-energy-information, the T > 0 domain of Landauer-style calculations, unit/type/provenance invariants, and Planck-scale bounds. The deposit contains the public release report in DOCX and PDF; Typed Calculator A2 and its tests; the pinned Lean 4.30.0 / Lake / Mathlib v4.30.0 Formal F1 bundle; the Formal F2 native-no-bridge BLOCKED receipt; and a canonical reproducibility capsule, manifest and SHA-256 sheet. Scoped results: A2 98/98 tests PASS; 12/12 declared countermodels eliminated; Formal F1 966-job Lean build PASS; 7/7 expected compile-fail fixtures PASS; exact hash-bound finite-trace refinement preserved. Native no-bridge reproduction was NOT ACHIEVED because the sealed F2 environment failed before kernel execution and no external native runner was available at release time. Formal semantics for API A2 was NOT_OPENED. Planck-pixel, c-bandwidth and black-hole-overflow remain HOLD with zero accepted causal edges. This release does not establish full Python semantics, independent replication, a new physical law, security certification, authority or world effects. Status: OPEN_APPEND_ONLY; TERMINAL PUBLIC-AUDIT HANDOFF.