BIT-RIAC-001 R2 — Reality-Interface Admissibility Charter: Consolidated Meta-Charter and Lean 4 Core Encoding

BIT-RIAC-001 R2 introduces the Reality-Interface Admissibility Charter, a typed horizontal meta-charter governing when an internally closed representation, proof, receipt, ledger state, or claim may be promoted to a world-anchored claim, an authorized action, a grounded settlement, or a physical-source attribution. Its central separation is: InternalClosure ≠ WorldAnchoring ≠ Authorization ≠ PhysicalRealization. RIAC does not authorize natural events and does not claim that BIT operates or controls reality itself. It governs the admissibility of claims, actions, settlements, and source attributions made by agents and formal systems. R2 consolidates three historical R1 drafts as development lineage rather than three independent RIAC inventions. Exactly three independent integration cores are retained: 1. Non-vacuous Applicable-Gate Non-Laundering;2. Cross-Profile Conservative Non-Substitution;3. Conditional Typed-Handoff Preservation. The accompanying F6A package provides a no-Mathlib Lean 4.30.0 encoding of these three cores. The frozen project contains 617 Lean source lines and passes an exact clean build of 8/8 jobs. T1 and T2 disclose Lean’s standard propext axiom; T3 has an empty axiom surface. No local RIAC, domain, source, oracle, world, or empirical axiom is declared. Three semantic negative controls are rejected as intended. Status: precanonical and scoped. F7 external replication, F8 empirical/canonical validation, world-soundness, arbitrary adapter correctness, all-runtime mediation, and any claim that BIT is an operating system of nature remain open or explicitly excluded. RIAC là một meta-charter có kiểu, quy định khi nào một kết quả nội bộ được phép bước qua giao diện với thực tại dưới dạng claim neo vào thế giới, hành động được cấp quyền, settlement có chứng cứ hoặc attribution nguồn vật lý. RIAC không phải “hệ điều hành của tự nhiên” và không cấp phép cho các định luật tự nhiên xảy ra.