Jeremy Avigad, Anat Ganor, Lior Goldberg, David Levit · 7 authors
StarkWare's S-two prover provides an efficient means for establishing, on blockchain, that a program written in the Cairo virtual machine language runs to completion. The latter claim is encoded by an algebraic intermediate representation (AIR) that captures the semantics of the Cairo language. The AIR asserts the existence of tables of values from a finite field satisfying certain algebraic constraints. A cryptographic interactive proof system, circle STARK, provides an efficiently-checked certificate that the AIR is satisfied. We describe our verification, using the Lean 4 proof assistant, that the AIR encoding is sound, which is to say, the satisfiability of the AIR implies the computational claim.
Abstract AI-generated forgeries of financial documents—such as invoices, audit reports, ledgers, and balance sheets—expose a critical fault line in legal proof. These hybrid visual–textual artefacts derive evidentiary authority from their jurisvisual form: logos, seals, signatures, and tabular architecture, whose visual grammar indexes authenticity and institutional power. Drawing on Charles Sanders Peirce’s triadic semiotics (representamen–object–interpretant), this study demonstrates that deepfake technologies dissolve the sign-relation underwriting documentary proof by engineering synthetic representamina that mimic the indexical and symbolic features of authentic documents. At the same time, the underlying financial event may be absent. The evidentiary economy is thereby reconfigured within a videosphere where image-like documents perform the truth. This article advances a layered remediation architecture: (i) provenance anchoring through cryptographic signatures, content hashing, and distributed ledgers; (ii) content forensics integrating AI-assisted detection with forensic semiotics—indexical stress tests and symbolic authenticity challenges; and (iii) procedural safeguards including calibrated evidentiary thresholds, adversarial authenticity hearings, and robust chain-of-custody protocols. It argues that restoring evidentiary confidence requires cultivating semiotic literacy among judges, auditors, and legal practitioners as core professional competence, enabling legal systems to navigate the post-textual landscape with epistemic rigour.
The Internet of Vehicles (IoV) is changing the contemporary mobility, as it allows real-time communication between vehicles, infrastructure, and cloud services. Nevertheless, such growing connectivity brings on serious privacy, regulatory, and trust issues especially because sensitive behavioral and location information is exposed. The current IoV-security systems tend to be based on identity-based checks, or centralized trust authorities, which can lead to infringement of user privacy and cause surveillance and profiling threats. The paper is inspired by privacy-preserving architectures in the Metaverse to suggest a decentralized trust system of IoV systems on the basis of zero-knowledge proofs, namely zk-SNARKs. The suggested solution allows vehicles to cryptographically verify that they meet regulatory or operational regulations- i.e. valid insurance, safety test, or emissions- without revealing personal identifiers or raw information. The framework enables building scalable, low-latency and audible trusts and following data minimization principles through combining zk-SNARK verification and Layer 2 blockchain solutions.
This study examines whether retail social media sentiment and community attention explain daily net capital flows into U.S. spot Bitcoin exchange-traded funds (ETFs), and whether issuer brand visibility conditions that relationship. We construct a balanced panel of N=10 ETFs over T=514 trading days (January 2024 to January 2026) and combine it with 162,819 cleaned Reddit posts to derive three AI-driven discourse variables: engagement-weighted sentiment, community attention, and a novel issuer-specific BrandScore. Entity fixed-effects regressions show that neither aggregate sentiment nor BrandScore level alone significantly predicts fund-level flows; however, the Sentiment × BrandScore interaction is significant (β^=2.930, p=0.038), indicating that sentiment becomes economically meaningful only when attached to a visible issuer. This interaction survives two-way (entity + date) fixed effects (p=0.012) and winsorization (p=0.004). Panel quantile regressions reveal distributional heterogeneity in the brand-sentiment channel. Rolling 90-day window estimation confirms the mechanism is episodic, with the interaction achieving significance in 62.8% of subsample windows. These results provide suggestive evidence for a brand-filtered sentiment transmission mechanism in digital asset markets.
Salience-Queue Occupation Theory (SQOT) is a protocol-relative mathematical framework for analyzing when finite-budget operational processes lose effective control over their priority queues under persistent or adversarial salience sources. The manuscript formalizes salience occupation using observable histories, budget ledgers, diagnostic reserves, queue morphisms, finite certificate grammars, checkable ledgers, typed risk composition, self-auditing kernels, and route-sound checker semantics. The theory is designed for artificial, distributed, or post-biological operational systems, but it does not rely on subjective psychology or normative claims about what a process should attend to. Instead, it studies finite, auditable conditions under which a process can preserve diagnostic capacity, response or no-action availability, rollback or quarantine options, semantic-egress safety, mechanism-compatible incentives, and bounded verification cost. The results include finite checker semantics soundness, checked non-circular sovereignty certificates, typed risk composition, adaptive succinct-session soundness, egress abstraction refinement, and payoff-reflected mechanism robustness. SQOT explicitly limits its claims to declared validity domains and does not assert absolute physical, cryptographic, economic, or base-reality guarantees.
C. Rupa, K. Vijaya Bhaskar Reddy, Srinivas Jagirdar, Srinivas Rao Pulluri · 6 authors
Land registration and record management systems worldwide continue to face significant challenges, including document fraud, long processing times, and inefficient maintenance procedures. Traditional methods involve several technical limitations that reduce reliability and transparency. To address these issues, the proposed system leverages blockchain technology to improve process efficiency, data integrity, and security in land registration workflows. In the proposed framework, users upload property details and supporting land documents while initiating a sale. However, fraudulent document uploads remain a common issue, enabling sellers to receive payments using forged records without the buyer’s knowledge. To mitigate such risks, a Convolutional Neural Network (CNN) is integrated to authenticate and validate uploaded land documents before further processing. Only documents verified as authentic are stored on the blockchain. The government authority converts these validated documents into Non-Fungible Tokens (NFTs) and mints them on the Ethereum blockchain. A unique hash is generated for each document, enabling secure verification and traceability through platforms such as Etherscan. Once the documents are confirmed to be valid, the property is approved for sale, and the ownership transfer between the seller and buyer is securely executed through the blockchain enabled system. We evaluated the performance of proposed framework by considering both blockchain performance metrics and CNN evaluation metrics.
Frontier AI governance frameworks increasingly use cumulative training compute as the primary criterion for designating high-impact models, but enforcement rests on self-reporting because no technical verification primitive for training exists. Any future international agreement on frontier AI faces the same problem at higher stakes: coordinated regulation of technologies with significant externalities has historically rested on technical verification, without which agreements are declaratory. Recent governance analyses judge zero-knowledge proofs a promising candidate but currently impractical at frontier scale [26, 4]. We argue the impracticality is paradigm-bound rather than fundamental, and propose a verification architecture for frontier dense pre-training combining a pre-committed training specification, inter-node network observations, and on-the-fly Merkle commitments of intermediate computation, verified through a zero-knowledge Virtual Machine (zkVM) with native BF16/FP32 precompiles. The proof checks the actual floating-point computation the GPU performed rather than a fixed-point approximation, and preserves model-architecture confidentiality through a private training specification. The protocol produces three proof types: a genesis proof at initialisation, in-training step proofs across the run, and ex-ante attestations enforcing policy-relevant claims as running invariants, turning the training record into a governance-enforceable artefact. We estimate a deployable proof of concept within approximately 36 months at single-digit-percent training-side overhead, against a six-to-ten-year cycle for verification-grade custom silicon. Thirteen open research and engineering problems are catalogued as a research agenda for external contribution
Decentralized Finance (DeFi) services are usually constructed by composing a variety of smart contracts. While composability is a key driver of the success of DeFi, it also creates security risks: adversaries may exploit interactions between newly deployed contracts and the pre-existing ones to inflict economic losses. We introduce MEV non-interference, a formal security notion for DeFi composability requiring that the maximal extractable value from a set of newly deployed contracts is not increased by interactions with the existing blockchain state. To support this notion, we define local MEV, a novel measure of economic attacks that focusses on the loss of a given set of victim contracts. We study two adversarial models, with bounded and unbounded wealth, and establish sufficient conditions and locality principles that enable modular reasoning about secure composability. We apply the framework to representative DeFi compositions, including exchanges, AMMs, options, lending pools, routers, and arbitrage contracts, showing how it distinguishes secure compositions from vulnerable ones. Our results provide a formal foundation for reasoning about the economic security of DeFi compositions.
Few forces have reshaped organizational life as quickly as digital transformation. The way firms create value, manage risk, and hold their competitive ground now depends on systems that grow more entangled with one another every year. A typical enterprise sits at the center of a constant flow of data drawn from its operations, its cloud platforms, the sensors embedded in its products, its planning systems, and the many places where it meets its customers. Artificial intelligence (AI), machine learning, big data analytics, blockchain, and cybersecurity have each made it easier to turn that flow into useful judgment. Yet most organizations still adopt these tools one at a time, and the habit quietly erodes the strategic payoff that integration could deliver. This paper sets out an Autonomous Decision Intelligence (ADI) framework that gathers AI, cybersecurity, big data analytics, blockchain, and management information systems (MIS) into one coherent architecture built for resilient digital enterprises. The argument rests on a synthesis of recent work in decision intelligence, predictive analytics, business intelligence, federated learning, cloud computing, blockchain governance, cyber threat intelligence, and enterprise risk management. From that body of evidence, we construct a conceptual model for organizational decision-making that is trustworthy and capable of improving itself over time. The framework gives weight to secure data governance, explainable AI, privacy-preserving analytics, blockchain-based trust, cyber-resilience, and intelligent automation. It then asks how such a design might reinforce critical infrastructure protection, supply chain resilience, economic sustainability, IT project governance, and day-to-day agility. The contribution is at once theoretical and practical, because it shows how converging technologies can turn conventional decision-support systems into adaptive ecosystems that learn. Organizations that pair AI-driven analytics with strong security and decentralized trust look best placed to absorb uncertainty, keep operating under stress, and pursue digital transformation that lasts.
Trusted Execution Environments (TEEs) have emerged as a critical technology for safeguarding sensitive data and ensuring code integrity in modern computing systems. However, relying on a single TEE implementation makes systems vulnerable to a central point of attack. Building distributed-trust systems leveraging heterogeneous TEEs helps disperse trust but still faces threats from centralized management and adaptive mobile adversaries. To address these challenges, this paper introduces TeeDAO, a novel three-layer framework that automatically organizes multiple heterogeneous TEE instances and provides unified interfaces to support diverse applications, while ensuring long-term guarantees of availability, integrity, and confidentiality. TeeDAO couples BFT-ordered governance with heterogeneity-aware Distributed Proactive Secret Sharing (DPSS) and Secure Multi-Party Computation (MPC) so that attestation-driven committee changes are consistently reflected in secret recovery, resharing, and computation across a dynamic committee of heterogeneous TEEs. We implement a prototype of TeeDAO, integrating COBRA's DPSS scheme with the HotStuff BFT consensus protocol, and adapt it for Intel SGX, TDX, and Hygon CSV. Evaluations demonstrate that TeeDAO achieves up to 1.8x higher key-value store throughput in a large cluster with 61 nodes compared to state-of-the-art systems, efficient autonomous management, and minimal computation overhead (<18%) for multi-party computation tasks.
Abstract : This article investigates the efficacy of implementing an AI-powered automated trading system on the blockchain using advanced machine learning algorithms and smart contract technology. The work addresses the challenges of cryptocurrency market volatility, the need for real-time decision making and the limitations of traditional trading approaches that often result in suboptimal returns and exposure to increased risk. This work develops a comprehensive trading platform that combines Long Short-Term Memory (LSTM) neural networks, Q-Learning reinforcement learning algorithms and blockchain-based smart contracts to create an autonomous, intelligent trading system. The methodology follows a multi-layered approach that integrates real-time market data collection from CoinGecko and Snowtrace APIs, advanced AI model training using TensorFlow.js, and smart contract deployment on the Avalanche C-Chain using Hardhat and OpenZeppelin libraries. LSTM model is used for price prediction and Q-Learning agent is used for trading strategy optimization, while comprehensive risk management is implemented using Value at Risk (VaR) calculations, portfolio rebalancing algorithms and automated stop-loss mechanisms. The trading execution is facilitated through direct integration with Pangolin DEX smart contracts to ensure decentralized and trustless trade execution. The performance of the system is evaluated using a sophisticated backtesting engine with Monte Carlo simulations, comparing the AI-driven strategy against traditional buy-and-hold approaches. The performance metrics used were Sharpe ratio, maximum drawdown, win rate, and total return. The AI-powered token prediction system demonstrates a superior performance due to its ability to process complex, non-linear market patterns and adapt to changing market conditions through reinforcement learning, and execute trades with minimal latency through blockchain integration. The findings are expected to provide cryptocurrency traders and institutional investors with a robust and automated trading solution that leverages the benefits of both artificial intelligence and blockchain technology for improved investment outcomes and risk management.
We introduce the Polymarket-v1 Database: the complete on-chain trade archive of Polymarket's first-generation CTF Exchange on Polygon, spanning 2022-11-21 to 2026-04-28 and covering the full contract lifecycle from first settlement to natural termination. The dataset comprises 1.20 billion trade records across 1.30 million markets with $61 billion in nominal volume. Its defining feature is 100% ground-truth aggressor direction derived from the blockchain settlement layer, a property unavailable in existing prediction market archives, which rely on heuristic inference. We use this truth-aligned archive to benchmark standard microstructure tools and document three findings. First, the tick rule and bulk volume classification achieve near-random aggregate accuracy (49.83% and 50.51%), but this masks a systematic, correctable price-level gradient driven by positive trade direction autocorrelation and concentrated market-making -- two structural features of prediction markets that violate the mean-reversion assumption embedded in classical classifiers. Second, these classification errors propagate into downstream metrics: inferred VPIN diverges substantially from ground-truth VPIN, and OFI estimates are directionally biased, with material consequences for Transaction Cost Analysis. Third, ground-truth microstructure quality predicts forecasting performance in ways that classification-based proxies cannot recover: True VPIN positively predicts Brier scores, while Gibbs spread negatively predicts them -- a selection effect reflecting that high-spread niche markets attract informed specialists rather than noise traders. Replacing ground-truth metrics with classified proxies attenuates both relationships, illustrating that measurement accuracy at the transaction level is a prerequisite for reliable inference about prediction market design and probability calibration.
Antonio J. Fernández-Pinto, Manuel Bravo, Gregory Chockler, Alexey Gotsman
Unauthenticated Byzantine consensus protocols achieve optimal failure resilience while relying only on authenticated point-to-point channels, not authenticated messages. They are an attractive building block for blockchains that do not mandate symmetric trust assumptions as well as for future post-quantum settings. We consider unauthenticated Byzantine consensus in partially synchronous networks and focus on optimizing its good-case latency - the worst-case time for correct processes to reach a decision under favorable conditions. A recently proposed ForgetIT protocol achieves an optimal good-case latency of 3 message delays but employs a highly complex design. We show that this complexity is unnecessary. To this end, we present Fast TetraBFT - an unauthenticated Byzantine consensus protocol that achieves optimal good-case latency by augmenting an existing TetraBFT protocol with a simple fast-path wrapper. Our solution lowers the good-case latency of TetraBFT from 5 to 3 message delays while preserving its bounded space requirements and low communication complexity.
Sixth-generation (6G) wireless networks will underpin ultra-dense Industrial IoT (IIoT) ecosystems in which resource-constrained Far-Edge devices -- autonomous mobile robots, industrial actuators, connected vehicles -- must simultaneously satisfy sub-millisecond latency, $10^{-7}$-class reliability, and decades-long cryptographic security. Current architectures delegate Digital Twin (DT) computation to centralised cloud or Mobile Edge Computing (MEC) servers, incurring prohibitive round-trip latency, and rely on classical public-key cryptography vulnerable to quantum attacks under the harvest-now, decrypt-later (HNDL) threat model. We propose Q-FE, a Quantum-Native 6G Far-Edge architecture integrating three co-designed components: (i) Micro-Digital Twins ($μ$DTs) co-located with 6G base stations and high-capability endpoints; (ii) a Cross-Layer Post-Quantum Key Exchange module embedding CSIDH-512 isogeny key material directly within MAC-layer control frames, exploiting the scheme's uniquely compact keys ($\le 64$ bytes) to avoid packet fragmentation; and (iii) an Asynchronous Federated Learning (AFL) protocol governed by lightweight DAG smart contracts at MEC nodes, eliminating straggler bottlenecks and preventing model-poisoning and Sybil attacks without exposing raw data. End-to-end simulations (NS-3 + PySyft) demonstrate that Q-FE reduces MAC-layer overhead by 62% versus ML-KEM/Kyber-1024, maintains P99.9 URLLC latency at 0.78 ms, and accelerates global-model convergence by 31% over synchronous Federated Learning. Protocol complexity analysis confirms $O(N \log R)$ per aggregation round, and $μ$DT handover migration completes in $1.9 \pm 0.3$ ms across $10^4$ simulated events. A formal threat model confirms resilience against quantum eavesdropping, model-poisoning, and Sybil attacks.
We present a hybrid news sentiment engine that continuously learns market sentiment from paired news headlines and concurrent asset-price snapshots without requiring any neural network training or GPU compute. The system uses a three-way ensemble combining (1) a financial-domain lexicon (FinBERT-style keyword scoring), (2) an adaptive statistical TF-IDF cluster learner that organizes headlines into semantic neighborhoods and tracks their average realized price reactions, and (3) an auto-calibrating weighting mechanism that adjusts ensemble contributions based on each signal's historical correlation with actual price movements. The engine runs on a 3-hour polling cycle from the Tradeflags NewsFeed API, which provides 22 price-snapshot fields per news item spanning equity indices (ES, NQ, SPY, DJIA, NDX, IWM), commodities (CL), and cryptocurrencies (BTC, ETH). All processing occurs at sub-second latency on a CPU-only server at effectively zero marginal cost per analytic cycle. We compare our approach against established methods -- FinBERT, GPT-based scoring, VADER, and commercial sentiment APIs -- across dimensions of cost, latency, accuracy, and adaptability. Our statistical cluster learner, which adapts to changing market regimes without retraining, represents a novel contribution not found in existing sentiment systems.
A new form of Maximal Extractable Value (MEV), termed speculative MEV, has emerged across Layer-2 blockchains. Unlike Ethereum mainnet, many Layer-2 systems lack a public mempool, forcing extraction strategies to become probabilistic: searchers emit multiple identical transactions hoping to capture an opportunity first. This generates substantial transaction spam, increasing fees and wasting block space. We investigate speculative Oracle Extractable Value (OEV), a form of MEV associated with liquidating undercollateralized loans via speculative backrunning of oracle price updates. We propose a methodology for detecting speculative liquidations in the wild and apply it across Arbitrum, Base, and Optimism. On October 10, 2025, we identify 64 speculative liquidators on Aave (57% of all detected liquidators) and 831 successful speculative liquidations (39% of all successful liquidations across the three chains). We further examine whether latency differences in oracle price feed updates across blockchains can be exploited for cross-chain OEV. Specifically, we ask whether a searcher can observe oracle updates on one chain and frontrun liquidation opportunities on another. We systematically analyze Chainlink Decentralized Oracle Network (DON) configurations (deviation thresholds, heartbeat intervals, and submitted price observations) across Arbitrum, Base, Ethereum, and Optimism. Our dataset comprises 63 Chainlink feeds, 12,009 price updates, and over 100,000 oracle observations linked to 2,986 Aave liquidations. We show that independent DONs consume largely identical off-chain price data nearly simultaneously yet publish updates at different times, creating statistically predictable cross-chain exploitation windows. We demonstrate that Chainlink updates on Optimism can predict subsequent updates on Arbitrum and Base, enabling speculative cross-chain OEV extraction.
We analyze intentional block delays (mining gaps) in Proof-of-Work blockchain systems, where miners strategically balance mining rewards against operational costs. Using a game-theoretic model, we derive a Nash equilibrium with optimal mining strategies and establish necessary and sufficient conditions for mining gap existence. We demonstrate that mining gaps, when combined with difficulty adjustment algorithms, can destabilize the system. We propose conditions to address sustainability concerns as block rewards decrease and reliance on transaction fees increases. Our findings are illustrated through a two-player game simulation and an analysis of the Bitcoin network, providing insights for blockchain design and policy. This work contributes to understanding strategic mining behavior and its impact on blockchain stability and efficiency.
Incorporating news into time series forecasting is appealing because news can reveal abrupt exogenous events that historical values alone cannot recover. However, existing LLM-based news-forecasting pipelines face two practical limitations: relevant news articles often exceed the model's context window, and iterative retrieval of supplementary news is typically unguided, leading to redundant updates and slow convergence. We address these issues with a novel framework that combines importance-aware news compression and process-level retrieval supervision. First, we train an importance reward model that estimates the forecasting utility of each article and uses this signal to allocate compression budgets during sequential pairwise fusion, preserving informative content within a fixed context limit. Second, we introduce a process reward model (PRM) that ranks multiple supplementary-news candidates conditioned on the current error profile and the history of previously selected articles, replacing one-shot blind retrieval with quality-controlled selection. Both components are trained offline using historical data with ground truth; inference uses the frozen filtering logic and compression modules without any reflection loop. Experiments on finance, energy, traffic, and bitcoin forecasting benchmarks show that our method improves prediction accuracy over strong baselines, significantly reduces the number of refinement iterations compared to the iterative baseline, and remains effective when relevant articles span thousands of tokens.
This preprint is available in two versions: French (main_fr.pdf / main_fr.tex) and English (main_en.pdf / main_en.tex). The English abstract follows. For over one hundred and fifty years, all railway signalling architectures have rested on a single assumption: safety authority resides in the ground infrastructure. The network authorises; the train obeys. We question its necessity. The physical safety condition is a local property of the train and its environment, verifiable without external authorisation. We propose an architecture — AEGIS (Autonomous Embedded Ground-Independent Signalling) — in which neither primary safety nor installation coordination depends on a centralised ground authority: the ground provides certified data, the train reasons, and installation coordination is handled by a topologically partitioned distributed ledger. We examine the architectural properties arising from this inversion, the emergent properties of the resulting system, and the open questions this new paradigm generates.
Context: The growing adoption of distributed and industrial-grade applications built on blockchain infrastructures has intensified the need for systematic approaches to manage the lifecycle of long-running systems, where governance, auditability, and performance constraints must coexist. Objectives: This paper presents TRUST , a lifecycle-oriented system architecture for the governed evolution and integration of smart contract based components. Methods: The architecture incorporates on-chain governance, version traceability, rollback support, and code provenance to enable accountability and observability across successive deployments in multi-stakeholder systems. A full 2 4 factorial evaluation was conducted by treating governance, versioning, provenance, and ABI handling as independent system factors and measuring their effects on latency, throughput, and gas consumption. Results: The results show that governance and provenance introduce controlled and predictable overheads, while compact ABI handling improves throughput and reduces gas consumption by more than 20%. Conclusion: These findings indicate that a lifecycle-oriented architecture can balance accountability and efficiency in governed smart contract applications.
Vulnerability disclosure volumes now far exceed organizational assessment capacity, yet three adjacent research communities (proof-of-concept generation, vulnerability prioritization, and detection rule engineering) operate largely in isolation. Existing automated exploit generation systems report binary pass/fail outcomes, discarding partial progress and producing no signal for the other two communities. This paper presents FORGE, a multi-agent system that bridges these three silos through graduated exploitation depth. Five specialized agents (Intel, Generator, Planner, Exploit, and Detector) execute in a fixed pipeline that (1) generates targeted vulnerable applications from CVE metadata, (2) conducts coached, multi-turn exploitation assessed by an LLM-primary oracle on a four-level taxonomy (L0: no evidence through L3: full compromise), and (3) produces Sigma and Snort detection rules grounded in OpenTelemetry exploitation traces. Graduated depth is the bridging mechanism: deeper exploitation yields richer behavioral traces for detection engineering, while depth data across scoring bands provides ground truth for prioritization validation. A tiered knowledge architecture accumulates intelligence across assessments, transferring build and exploitation experience to subsequent CVEs. Evaluation on 603 CVEs from the CVE-GENIE dataset achieves 67.8% end-to-end L1+ exploitation at USD 1.50 per CVE across eight languages and 187 CWE types. Exploitation rates remain near 68% regardless of EPSS or CVSS band, indicating that pattern-level reachability is orthogonal to metadata-based prioritization. Detection rules from L2+ exploitation achieve significantly higher span-normalized grounding than L1-derived rules (p=0.035), and 93.4% of generated Snort rules produce zero false positives against a synthetic benign corpus.
We propose ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Lof Dependent Type Theory (MLTT) integrating trace-indexed types, presheaf non-monotone semantics, and constructive AGM belief revision. A Coq mechanisation accompanies the paper (34 complete proofs; zero admits for the two central results). (I) Trace types. FinTrace(s0,sn) is an inductive family of typed execution traces. FinTrace and Star(Step) are isomorphic as path types but not judgementally equal; TraceElim exposes the event label e:Event explicitly, giving a more ergonomic interface for event-driven induction. We prove the Trace-Reachability Correspondence, Deterministic Replay, and a canonicity framework via reducibility candidates with a Transport Lemma (RC-elim deferred; all other Core results are Coq-verified). (II) Sheaf semantics. Trace-indexed propositions are contravariant sheaves over the free trace partial-order category Tf. A Separation Theorem (explicit countermodel) distinguishes proof-theoretic monotonicity from semantic non-monotonicity. The term model is an initial CwF (syntactic universal property, not classical completeness). (III) AGM belief revision. We give an explicit constructive partial meet contraction algorithm verified against (C1)-(C4). All eight AGM postulates (R1)-(R8) are theorems. Proofs of R7 and R8 use the Disjunctive Entrenchment Lemma, given a self-contained constructive derivation. (IV) Integration. B^AGM fails the sheaf composition law BP-comp for sequential revision (explicit countermodel, Coq-verified). We introduce Single-Step Revision Systems (SSRS), prove B^AGM is a valid SSRS (Coq-verified), and show this suffices for trace morphisms, retraction characterisation, and revision witnesses. The BP-comp failure reveals a fundamental tension between path-dependent belief revision and functor consistency, not previously identified.
This preprint develops a unified thermodynamic and game-theoretic framework for the analysis of monetary systems, with particular focus on Bitcoin as a proof-of-work-based digital monetary architecture. The work combines concepts from thermodynamics, information theory, game theory, monetary economics, and econophysics to investigate how monetary systems may be understood as coordination systems operating under informational, institutional, and physical constraints. The manuscript introduces a distinction between monetary entropy, associated with uncertainty in monetary issuance, layered claims, and purchasing-power instability, and physical entropy generated through irreversible energy dissipation in proof-of-work systems. Building on this distinction, the concept of monetary temperature is proposed and operationalized through purchasing-power volatility and related coordination variables. Within this framework, Bitcoin is interpreted as a thermodynamically enforced Nash-equilibrium system in which strategic stability is constrained through irreversible physical cost. Comparative analysis of Bitcoin, gold, and fiat monetary systems suggests that monetary architectures can be understood as evolving entropy-management architectures adapted to different technological and civilizational conditions. Finally, the paper proposes an evolutionary interpretation of monetary history in which monetary systems function as mechanisms for stabilizing large-scale human cooperation under increasing informational complexity. Monetary evolution is interpreted as a cooling process in which declining volatility corresponds to increasing coordination maturity and stabilization across expanding economic networks. Keywords: Bitcoin, thermodynamics, Nash equilibrium, monetary entropy, entropy-management architectures, proof-of-work, econophysics, monetary systems, monetary temperature, game theory.