Abstract This orientation presents the architecture, results, boundaries, and reading paths of the Identity-Persistence Program, a research program on the structural conditions under which bounded evaluators can make reproducible judgments of identity, persistence, admissibility, and verification under declared regimes. The program’s foundational layer establishes three forcing results: structural floors for coherent identity claims, admissible transformation, and sufficient regime specification. These are bracketed below by the requirement that cumulative inquiry possess a stable same/not-same criterion and above by an identification ceiling: within the finite declared class, admissible evidence identifies only up to the declared quotient. The guide then maps the program’s post-floor structural theory. For a declared question family, maximal structure-compatible safe congruences yield canonical demand-relative normal forms and a theory of regime equivalence and refinement. Recurrence is classified in the one-degree homogeneous case; symmetry reduction is separated from operable quotient structure through an independent-redescription compatibility criterion; nested regimes compose through backward demand propagation and forward certificate compression; and reconstructibility, blocking cuts, and verification complexity are characterized at the mechanization layer. Condensation Dynamics adds a finite dynamical theory in which safe quotienting has an exact potential and path-independent total budget, interaction defects measure noncanonical allocation, serial nesting obeys a no-free-acceleration law, and structural conditions for zero defect are identified. The orientation also distinguishes these theorem-bearing results from the program’s finite-interior analyses of interaction, omission, representation, and declaration dependence; from interpretive accounts of endogenous regime formation; and from downstream runtime engineering. The resulting architecture is not a claim about final ontology or unrestricted knowledge. It is a class-relative theory of what bounded evaluators can license, preserve, compress, compose, and independently verify once the governing regime has been sufficiently declared. Corpus-native instantiation, selected extension classes, and independent formal proof verification remain open. This document proves no new theorem. It is the program guide: it records dependency structure, claim status, scope boundaries, and reading order, while the individual papers remain authoritative for their results.
Three classical set-theoretic themes — the axiom of choice onindistinguishable pairs (Russell's socks), the comparison of infinitecardinals, and the uncountability of the continuum — are re-readoperationally: an assertion counts only as an act, performed andwitnessed, never as a completed object postulated into existence. Underthis reading each theme splits cleanly in two, and both halves becomeshort machine-checked theorems. For the socks: no selection rule exists (no swap-symmetric selectorbeyond any finite bookkeeping bound — the Fraenkel–Mostowski statementin miniature, on the empty axiom list), while selection acts form acontinuum (the selectors are exactly the branches, which are notenumerable). The deterministic half is itself a theorem — in ananonymous network of identical automata started identically theconfiguration stays constant across nodes at every round, for arbitrarywiring, so no round distinguishes a unique node (the folklore core ofAngluin 1980, machine-checked, to our knowledge for the first time). For cardinals: a comparison is an act whose witness is data — anexplicit injection from the naturals into the branches is performed; theCantor–Lawvere diagonal is proved uniformly for every floor of thepower-set ladder, on the empty axiom list; the resulting order ispartial by design, since cardinal trichotomy is equivalent to full ACand is cited as a formal-register label rather than claimed. For uncountability: the sign is flipped from prohibition toproductivity — the fugitive from any enumeration is computed by anexplicit term, so the continuum is productive in Post's sense: thecatalogue that reads itself extends itself. And dependent choice is theperformable part of choice (recursion on a history-dependent rule,choice-free); what remains of full AC above DC is the part that can onlybe written, not performed — the same remainder whose surrender dissolvesthe Banach–Tarski decomposition (Solovay's model; cited as metatheory). Nothing here is a new classical theorem; the mathematical content ofeach proof is elementary and classical. The contribution is theoperational re-reading, the split of each theme into an impossible-rulehalf and a performed-act half, the axiom pricing of every step, and themachine check. The axiom of choice is not refuted — a symmetric-selectorimpossibility is a statement about rules, while AC postulates an objectexempt from symmetry. The paper is written to be verified from zero. A single self-containedLean 4 file (`Verify_Choice_standalone.lean`, no mathlib, no imports)reproves all ten empty-axiom-list theorems in under a second — anyagent, human or machine, runs `lean Verify_Choice_standalone.lean` andreads "does not depend on any axioms" ten times. The full corpusverifies with `lake build`, and `#print axioms` lines exhibit the axiomprofile of every object. An empty axiom list is precisely a verdict twoparties who share no axioms and no trust can both confirm: the strongestform of a checkable claim. The reliability of the results does notdepend on trusting the author, the AI that helped write the paper, orthis text — only the Lean 4 kernel. AI disclosure: this work was carried out with the substantialparticipation of the AI system Claude (Anthropic; this preprint —Claude Fable 5) in a dialogue setting; all design decisions, forkchoices, and final responsibility rest with the human author.
Distributed certification is a set of mechanisms that allows an all-knowing prover to convince the units of a communication network that the network's state has a desired property, such as being 3-colorable or free of a predefined subgraph. Classical mechanisms, such as proof labeling schemes (PLS), consist of a message from the prover to each unit, followed by one round of communication among neighbors. Later works consider extensions, called distributed interactive proofs, where the prover and the units can have multiple rounds of communication before the communication among the units. Recently, Bick, Kol, and Oshman (SODA '22) defined a zero-knowledge version of distributed interactive proofs, where the prover convinces the units that the network satisfies the property without revealing any additional information about the network's state or structure.
We study distributed zero-knowledge proofs, introduced by Bick, Kol, and Oshman (SODA 2022). While distributed interactive proofs have advanced rapidly in recent years, general-purpose techniques for distributed zero-knowledge remain scarce and mostly problem-specific. We address this gap by introducing distributed statistical zero-knowledge, requiring that each node's view be simulatable up to negligible statistical distance, and by lifting the robust Sumcheck protocol (Lund, Fortnow, Karloff, and Nisan; FOCS 1990) into a modular primitive for distributed zero-knowledge proofs.
Formal software verification systems aim to provide rigorous mathematical proofs that programs adhere to their specifications. In particular, proof assistants like Agda, Rocq and Lean can express programs, specifications and proofs within a single unifying language called Dependent Type Theory (DTT). This thesis makes contributions to parametricity within the setting of DTT and proof assistants. As a first approximation, parametricity is a uniformity property regarding polymorphic, i.e. generic programs. A generic program behaves identically regardless of the type it is instantiated with, because it cannot inspect its type argument. This simple observation leads to useful knowledge when performing proofs about the program (Wadler calls such knowledge ``theorems for free''). More generally, Reynolds mathematically defined the notion of parametricity as relational parametricity, the statement that every type can be turned into a certain reflexive graph. An edge in the graph between two values is a proof that the values have a similar structure. For instance an edge between polymorphic programs is a proof that they map related types to related outputs, and this formalizes what it means to be uniform. The parametricity translation, mapping types to reflexive graphs, is defined externally as a meta-operation on DTT expressions and is not an operation that is available inside, or internal to DTT. For example, given a type of polymorphic functions, one cannot prove inside DTT the formal statement expressing that every such function is uniform (we call such statements global free theorems). Internally parametric type theories (PTTs) achieve this by equipping DTT with a so-called Bridge type former, whose role is to represent the parametricity translation inside the theory. A landmark example is the interval-based theory of Cavallo and Harper (the CH theory), in which bridges are functions from a postulated bridge interval, in analogy with the path types of cubical type theory. Within the CH theory, global free theorems become provable. However, a practical limitation persists: contrary to the Reynolds translation of a type, the Bridge translation of a type does not directly provide an actionable parametricity result. Indeed tedious case-by-case rote work is required of the user to establish that the Bridge type former commutes with each type former appearing in the type under consideration. The first main contribution of this thesis is to improve the practical usability of internally parametric type theories. Firstly, we address the lack of a full-fledged proof-assistant implementation of binary internal parametricity and contribute the Agda-bridges proof assistant. Agda-bridges is an extension of the Agda proof assistant and implements an interactive typechecker for the CH parametric type theory. More precisely, Agda-bridges extends Agda-cubical, itself an implementation of cubical type theory. In fact, Agda-bridges typechecks the standard library of Agda-cubical, hence important theorems provided by Agda-cubical, like univalence, remain available to the user of Agda-bridges. Moreover, Agda-bridges validates key theorems for internal parametricity, in particular the relativity equivalence. This makes it possible to provide formal proofs of free theorems, including global ones. Yet the rote work challenge described above persists. Hence, secondly, we contribute Relational Observational Type Theory (ROTT), a library, or domain-specific language, written in Agda-bridges that eliminates the rote work in a principled way. ROTT lets the user obtain concise and modular proofs of actionable parametricity statements. Once a type is written using the ROTT DSL, a corresponding proof can be extracted as a one-liner. Using this methodology we are able to formalize global free theorems of practical and theoretical relevance. Notably, we expand on a proof communicated to us by Andrea Vezzosi and can show that higher-order abstract syntax is an adequate representation of the untyped lambda calculus (previously known proofs relied on the strictly stronger notion of Kripke parametricity). The second main contribution of this thesis concerns nullary internal parametricity and its relationship to the formal study of languages with variable binding. When studying a language on paper it is common to think of variables as strings, and to adopt the convention that alpha-equivalent terms are equal. However, when working formally it is preferable to represent the syntax of the object language in such a way that alpha-equivalent terms are equal by construction. Nominal frameworks are type systems featuring a so-called name abstraction type former, used to give a type to the binders of the object language. This type former enables a string-like but alpha-equivalence-respecting representation of syntax with binders. Yet existing nominal frameworks either feature typing rules hard to implement in a proof assistant environment, or lack expressivity to reason about nominal syntax. We solve these issues by contributing Parametric Nominal Type Theory, which is an extension of the nullary CH theory, a version of the CH theory where bridges have zero endpoints instead of two. Firstly, we recognize that the nullary CH theory is itself the basis of a nominal framework in which name abstraction corresponds to the nullary bridge type former. In fact the other primitives of the CH theory can be understood from a nominal point of view and existing nominal primitives can be implemented in terms of the CH ones. Secondly, we identify the missing piece that suffices to turn the nullary CH theory into an actual nominal framework, in which one can reason about object languages in a nominal fashion without the aforementioned lack of expressivity. The missing piece is a type of names Nm such that its nullary Bridge type/nullary translation is the sum type 1+Nm. We provide an induction principle for Nm that entails the property. We demonstrate that Parametric Nominal Type Theory is a suitable nominal framework. One of our examples involves emulating a restricted form of Kripke parametricity by nullary parametricity.
The Universal Form of Historical-Genetic Logic: From the Propositional Matrix to the Computable Index DOI: 10.5281/zenodo.20799967 Author: Aikaterini Xenopoulou TyrokomouIndependent ResearcherORCID: 0009 0004 9057 7432Email: katerinaxenopoulou@gmail.com Theoretical Foundation: Epameinondas Xenopoulos †Based on the Historical Genetic Logic of Epameinondas Xenopoulos, Epistemology of Logic: Logic – Dialectic or Theory of Knowledge (posthumous 2nd ed., 2024) [1, 2]Independent ResearcherORCID: 0009 0000 1736 8555† In memoriam (1920–1994) METHODOLOGICAL NOTE The present work mathematizes and extends central ideas of the formal-dialectical logic of Epameinondas Xenopoulos [1,2], with the direct aim of creating a computable and applicable tool. The mathematical expression of concepts such as dialectical intensity, historical memory, and the critical threshold constitutes a fully explicit, functional, and deliberate interpretative choice. Other consistent mathematizations are equally possible; here we choose those that ensure computational stability, transparency, and broad applicability. The work introduces original mathematical elements (such as the historical memory functions τ(t) and paradox factor Π(t), the stochastic extension, and the explicit form of the synthesis operator). These elements are presented as proposals of the author and are not attributed to Xenopoulos. The theoretical background, the fundamental categories, the logical principles, and the overall architecture belong to the work of Xenopoulos. The systematic formalization, the mathematical analysis, the proofs of the index properties, and the computational applications constitute the original contribution of the present work. ABSTRACT This work introduces the XEPTQLRI index, a computable, domain-agnostic diagnostic tool for anticipating critical transitions in complex dynamical systems. The index is grounded in the formal-dialectical logic developed by the Greek philosopher Epameinondas Xenopoulos (1920–1994), which treats contradiction not as an error but as the driving force of qualitative change. The index quantifies the "dialectical pressure" building within a system prior to a bifurcation. It combines three components: (1) dialectical intensity T(t), expressed as the harmonic mean of opposing tendencies ("Being" B(t) and "Non-Being" N(t)); (2) historical memory τ(t), capturing the direction and momentum of change; and (3) a paradox factor Π(t), which registers whether the system has historically experienced extreme opposing states. The index is defined as: Ξ(t) = [ T(t) · τ(t) · (1 + Π(t)) ] / Θ₀ where Θ₀ is a system-specific critical threshold. We prove that for systems undergoing pitchfork, transcritical, or Hopf bifurcations, the condition Ξ(t) = 1 coincides exactly with the vanishing of the maximum Lyapunov exponent — the mathematical signature of impending instability. The index is invariant under affine transformations of the coherence function, computable in linear time, and provides quantifiable early warning signals. Empirical validation across seven diverse fields — stochastic differential equations, COVID-19 epidemiology, LSTM networks under extreme noise, composting kinetics, open thermodynamics, Lindblad quantum systems, and strategic decision-making — demonstrates that the index reliably detects imminent qualitative shifts, often months before observable regime changes. The XEPTQLRI index offers a rigorous, efficient, and broadly applicable framework for early warning in nonlinear and complex systems, bridging dialectical philosophy with modern dynamical systems theory. Keywords: Historical-Genetic Logic, Formal-Dialectical Logic, Propositional Matrix of the World, XEPTQLRI Index, Dialectical Intensity, Historical Memory, Paradox Factor, Aufhebung, Critical Transitions, Phase Transitions, Bifurcations, Early Warning Signals, Maximum Lyapunov Exponent, Nonlinear Dynamics, Complex Systems, COVID-19 Epidemiology, Quantum Systems, Lindblad Equation, LSTM Neural Networks, Stochastic Differential Equations, Structural Stability, Dual Temporality. Lead Paragraph Detecting critical transitions before they happen: A dialectical index for early warning in complex dynamical systems Predicting when a complex system is about to undergo a qualitative change—whether a pandemic wave, a financial collapse, or a quantum phase transition—remains one of the most challenging problems in nonlinear science. Conventional early-warning indicators often fail to capture the slow accumulation of internal contradiction that precedes a bifurcation. Drawing on the formal-dialectical logic of the Greek philosopher Epameinondas Xenopoulos, we introduce the XEPTQLRI index, a novel pre-transitional diagnostic tool that quantifies the "dialectical pressure" building within a dynamical system. The index combines three components: dialectical intensity (the harmonic mean of opposing tendencies), historical memory (the direction and momentum of change), and a paradox factor that registers whether the system has experienced extreme opposing states in its past. We prove that, for systems undergoing pitchfork, transcritical, or Hopf bifurcations, the index crossing unity coincides exactly with the vanishing of the maximum Lyapunov exponent—the mathematical signature of impending instability. Empirical validation across seven diverse domains—from stochastic differential equations and COVID-19 epidemiology to LSTM networks under extreme noise, composting kinetics, open thermodynamics, the Lindblad equation for open quantum systems, and strategic decision-making—demonstrates that the index provides reliable early warnings, often months in advance of observable regime shifts. The XEPTQLRI index offers a mathematically rigorous, computationally efficient, and domain-agnostic framework for anticipating critical transitions in nonlinear and complex systems. INTRODUCTION The study of change runs throughout the entire history of philosophy. From Heraclitus ("πάντα ῥεῖ" – "everything flows") to Hegel, Marx, and Piaget, thought recognizes reality as an uninterrupted process of genesis, contradiction, and transcendence. Formal logic, although an indispensable tool of science, is founded on the abstraction of time and the principle of non-contradiction (p · ¬p = 0). The Greek philosopher Epameinondas Xenopoulos (1920–1994) developed a Historical-Genetic Logic (or formal-dialectical logic) that incorporates contradiction as the driving force of knowledge, bridging the gap between static formal thought and the dynamic flow of reality. In his work "Epistemology of Logic" [1,2], Xenopoulos establishes three central structures: 1. The epistemological correspondence Sπ ↔ Y(L, B, Θ): knowledge is born from the practical interaction of the subject-in-action (Sπ) with the object (Y), which is analyzed into logical structure (L), material substrate (B), and concrete position (Θ). 2. The Propositional Matrix of the World: a formal structure where each proposition carries a truth value from a discrete fractional spectrum {0, ½v, ½²v, …, 1} and passes through dialectical stages: thesis (A), development of negation (B), rupture (Γ), and new synthesis (Δ). 3. The operator N[Fi(Gj)]: the logical engine that drives propositions from one stage to another, expressing the necessary synthesis of thesis and its negation. The present article mathematizes and operationalizes these structures, giving them an explicit, computable form. For each concept we propose specific mathematical expressions. These choices are functional, not theoretically unique. The present form was chosen for its computational stability, broad applicability, and clear philosophical correspondence. The resulting XEPTQLRI index is not a simple statistical method, but the computable implementation of the dialectical operator itself in a specific, explicit mathematical framework. The empirical verification of the index in seven diverse fields (from stochastic dynamics to neural networks and epidemiology) demonstrates the practical power of this mathematization. PART I – THEORETICAL FOUNDATION 1. The Epistemological Correspondence: Sπ ↔ Y(L, B, Θ) Every cognitive process begins from the practical relation of the subject with the world. Xenopoulos [1,2] conceives this relation as an epistemological correspondence between two poles: · Sπ (Subject-Action): the subject in its active, transformative activity. Sπ is process, not state. It changes the world through action. · Y(L, B, Θ) (Object): the object of knowledge analyzed into three components: o L (Logos): the logical structure, the regularity, the form. o B (Matter): the material substrate, the content. o Θ (Thesis): the concrete spatiotemporal existence. The action Sπ modifies the object Y. This modification, assimilated by the subject, produces knowledge Sα = f(Sπ, Y). The correspondence is dialectical: action transforms the object, the transformation transforms knowledge, and new knowledge guides new action. Knowledge is not a passive image, but a historical product of interaction. This fundamental correspondence constitutes the cornerstone of every formal-dialectical analysis. 2. The Propositional Matrix of the World The knowledge born from the correspondence Sπ ↔ Y crystallizes into a dynamic formal structure: the Propositional Matrix [1,2, pp. 247-249]. Definition 1 (Proposition). A proposition P is defined as: P(x, y, z, t) = [v, τ, σ] with: · v ∈ V = {0, ½v, ½²v, …, 1}: the truth value on a fractional scale. 0 marks complete contradiction ("zero identity"), 1 marks the new integrated synthesis. · τ ∈ {T, D, TD}: the type of proposition (Formal, Dialectical, Formal-Dialectical). · σ ∈ {A, B, Γ, Δ}: the dialectical stage: o A (Thesis): stable formal knowledge. o B (Development of Negation): emergence of internal contradiction. o Γ (Rupture): critical
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.
Zero-knowledge proofs (ZKPs) play a critical role in mitigating modern digital threats by enabling verification without disclosure, a key requirement for secure computation in adversarial environments. Among existing constructions, zk-SNARKs and zk-STARKs represent two dominant paradigms with contrasting security, trust, and performance characteristics. While their theoretical foundations are well studied, practical performance under real-world conditions remains less understood. In this work, we present a systematic, implementation-level comparison of zk-SNARKs (Groth16) and zk-STARKs using publicly available reference implementations on a consumer-grade ARM platform. Our empirical evaluation covers proof generation time, verification latency, proof size, and CPU profiling. Results show that zk-SNARKs generate proofs 68x faster with 123x smaller proof size, but verify slower and require trusted setup, whereas zk-STARKs, despite larger proofs and slower generation, verify faster and remain transparent and post-quantum secure. Profiling further identifies distinct computational bottlenecks across the two systems, underscoring how execution models and implementation details significantly affect real-world performance. These findings provide actionable insights for developers, protocol designers, and researchers in selecting and optimizing proof systems for applications such as privacy-preserving transactions, verifiable computation, and scalable rollups.
Xenopoulos’ Historical Genetic Logic: A New Framework and the XEPTQLRI Theorem DOI:10.5281/zenodo.20367121Date: May 2026 Aikaterini Xenopoulou TyrokomouIndependent ResearcherORCID: 0009 0004 9057 7432Email: katerinaxenopoulou@gmail.com Theoretical Foundation: Epameinondas Xenopoulos †Based on the Historical Genetic Logic of Epameinondas Xenopoulos, Epistemology of Logic: Logic Dialectic or Theory of Knowledge (posthumous 2nd ed., 2024) [1, 2]ORCID: 0009 0000 1736 8555† In memoriam (1920–1994) Methodological NoteThe present work simplifies and mathematizes central ideas of the formal-dialectical logic of E. Xenopoulos in order to create an applicable computational tool. It does not constitute a faithful rendering of his philosophical theory in its full depth, but a focused operationalization for the purpose of computational application. Statement of AuthorshipThe present work is founded on the logical system of Epameinondas Xenopoulos (1920–1994). The XEPTQLRI index does not constitute an independent theory, nor does it introduce a new autonomous logical framework. The theoretical background, the basic categories, the logical relations, the fundamental principles, and the dialectical operators belong to the work of Epameinondas Xenopoulos. The contribution of the present work consists in the formal mathematical operationalization of specific principles of this logical system through a computable index, capable of being applied to dynamic and historically evolving systems. Consequently, the theoretical authorship belongs entirely to Epameinondas Xenopoulos, while the present work belongs to the level of systematic formalization, proof, application, and methodological development of his framework. The XEPTQLRI index expresses in quantitative form the logic of Being, Non-Being, Becoming, historical memory, and dialectical sublation, while adapting these concepts for computational use. In this sense, the present work constitutes a continuation, clarification, and applicative deepening of the Xenopoulos system, not a displacement or replacement of it. ABSTRACT We present the Xenopoulos Pre-Transitional Qualitative Leap Risk Index (XEPTQLRI), a novel mathematical index grounded in the Historical-Genetic Logic of the Greek philosopher Epameinondas Xenopoulos [1, 2]. Unlike conventional statistical summaries, XEPTQLRI captures the dialectical interplay between Being (B), Non‑Being (N), historical memory (τ), and a historical paradox factor (Π). The index is defined as Ξ = [T · τ · (1 + Π)] / Θ₀ with Θ₀ = 0.85, where T = 2BN/(B+N) is the dialectical tension expressed through the harmonic mean. Its construction respects strict causality, min‑max or logistic normalization, and a negative feedback mechanism (∂σ/∂Ξ < 0) in its dynamical extensions, though the index itself remains exogenous and purely diagnostic. We prove five theorems establishing constructive computability, scale homogeneity, non‑preservation of dynamical structure, representation dependence, and linear‑time computability. Two additional theorems (non‑self‑inversion and logical phase transition) are proved within the extended framework of the 34 Principles. Numerical experiments with the Ferrari–Xenopoulos v4.0 stochastic model show reproducible and persistent exceedance of the Aufhebung threshold, with endogenous volatility remaining low (σ ≈ 0.058). An extreme parameter run (α₅ = 1.6, σ₁ = 1.0, Θ₀ = 0.0867) reaches Ξ = 16.1, demonstrating that the critical value is not a universal constant but a local, parameter‑dependent realization. A “Dialectical War” experiment (LSTM vs. Xenopoulos system under noise = 1.0) reveals a striking dissociation: technical performance (MAE = 0.1039, 67.1% improvement) coexists with universal dialectical risk (20/20 high‑risk steps, Ξ_max = 2.99, zero paradoxality and false stability). This dissociation is mathematically consistent, as MAE and Ξ are distinct functions measuring different aspects of system behavior (MAE ⇏ Ξ). A null model comparison confirms that this risk is structurally generated (AUC 0.949 vs. 0.501, p < 0.001), with ground truth defined by the condition Ξ(t) ≥ Θ₀ for at least three consecutive time steps and binary classification threshold optimized via the Youden index. A strictly endogenous application of the canonical XEPTQLRI index to 13 distinct COVID‑19 waves in Greece (JHU CSSE) yields early warnings 48–90 days in advance (mean 84.0 days) with a mean EWS Score of 0.785, successfully detecting 10 of 13 waves (76.9%). The system substantially outperforms a simple cases‑threshold baseline (mean EWS 0.42, 23.1% success) without any reliance on AUC or external classifiers. Beyond its diagnostic function, the XEPTQLRI framework demonstrates a transformative capacity: non‑dialectical codes exposed to the Xenopoulos environment undergo systematic improvement, with documented gains ranging from 52.3% to 95.65% across multiple independent experiments. A banking crisis application correctly identified Lehman Brothers (z=3.2, p<0.001) and Bear Stearns (z=2.9, p<0.01) two years before their collapse using only pre‑2006 data. A financial early warning application achieved statistically significant predictive correlations (r=0.29–0.44, p<0.001) with lead times of 10–77 days across S&P 500, VIX, Treasury yields, and Bitcoin. Two complete experimental protocols (XENO‑EXP‑2026‑002 and XENO‑EXP‑2026‑003) provide systematic, statistically significant evidence that the Xenopoulos System, when fully embedded in machine learning architectures, functions as an improvement catalyst with measurable economic value (ROI 63:1, break‑even 6 days). Thus, XEPTQLRI bridges formal dialectics with practical early warning systems, establishing a universal law of qualitative transition while keeping its numerical expression local and context‑dependent. The present system constitutes a proto‑formalized theoretical framework — a structured mathematical–dynamical system with axiomatic foundation (34 Principles), provable theorems (7 Theorems), and computational implementation (Ferrari–Xenopoulos v4.0, COVID‑19 application), whose applicative and transformative value has been verified on real data. The system is internally consistent under its stated principles, though its full formalization in the sense of a Hilbert‑style formal system remains a subject for future work. Keywords: XEPTQLRI, Historical‑Genetic Logic, dialectical logic, qualitative leap, Aufhebung, early warning systems, stochastic differential equations, LSTM, COVID‑19, proto‑formalized framework, non‑classical negation, harmonic mean, paradox factor, historical memory, dialectical transformation, financial crisis prediction, code optimization. Lead paragraph Complex dynamical systems often undergo sudden, qualitative transformations—critical transitions that are difficult to anticipate with conventional statistical tools. This paper introduces a new mathematical framework for detecting such transformations, grounded in the Historical‑Genetic Logic of the Greek philosopher Epameinondas Xenopoulos (1920–1994). The central contribution is the Xenopoulos Pre‑Transitional Qualitative Leap Risk Index (XEPTQLRI), defined as Ξ(t) = T(t) · τ(t) · (1 + Π(t)) / Θ₀, where T is the dialectical tension between Being and Non‑Being, τ captures historical memory, and Π encodes the accumulated paradox of extreme past states. The index is fully endogenous, requires no external training or classifiers, and is accompanied by a typology of ten dialectical stages (τ₀–τ₉). We prove five constructive theorems, validate the framework through stochastic simulations, and apply it to real COVID‑19 data from Greece. Across 13 epidemic waves, XEPTQLRI issued early warnings with an average lead time of 84.0 days and a mean Early Warning Score of 0.785, substantially outperforming a simple cases‑threshold baseline. The framework thus bridges formal dialectics with operational early warning capability, offering a new lens for the study of critical phenomena. Part I — Definition and Foundation of XEPTQLRI 1. Theoretical Foundation This section presents the fundamental principles underlying the Xenopoulos Pre-Transitional Qualitative Leap Risk Index (XEPTQLRI), as formulated in the Historical-Genetic Logic of the Greek philosopher Epameinondas Xenopoulos (1920–1994) [1, 2]. These principles constitute the axiomatic framework of the index and determine both its mathematical form and its interpretive function. XEPTQLRI is neither a simple numerical magnitude nor a mere statistical summary. Instead, it is defined as a complex historical-dialectical index that captures the relationship between Being, Non-Being, their dialectical tension, historical tendency, and the probability of transcending a critical threshold of transformation. The index is embedded within the broader system of 34 Principles as the 23rd Principle, expressed through the general dialectical operator: Ξ(t) = N[F₂₃(G₂₃)]. 1.1 Principle 5: Complementarity According to the theory [1, 2], Non-Being is not an independent quantity but the complement of Being. This relationship is expressed by Principle 5: N(t)=1−B(t)N(t)=1−B(t) This equation implies that: B(t)+N(t)=1B(t)+N(t)=1 Therefore, the two quantities B(t) and N(t) are complementary aspects of the same dynamic state. If B(t) expresses the degree of presence of Being, then N(t) expresses the degree of presence of Non-Being. From the same principle it immediately follows that it is impossible for both of the following to hold simultaneously: B(t)>0.8andN(t)>0.8B(t)>0.8andN(t)>0.8 because then we would have B(t) + N(t) > 1.6, in contradiction with B(t) + N(t) = 1. Important clarification: In Theorem 2 (Paradoxical Transcendence), the condition B > 0.8 ∧ N > 0.8 refers to a special paradoxical state where the usual complementarity is suspended due to the historical accumulation of contradictions. In this state, B and N are not understood as instantaneous values at
Abstract The traditional Byzantine quorum-system model assumes a pre-existing, global agreement on the set of quorums (typically defined as the sets consisting of more than two-thirds of the participants). This assumption is problematic in permissionless systems, which strive to allow anyone to join or leave the system dynamically. While proof-of-stake permissionless systems like Ethereum require newly joining participants to register into the system, other permissionless systems like the Ripple Ledger or the Stellar network allow participants to join the system without synchronization by forgoing agreement on the set of quorums. This results in what we call a heterogeneous quorum system, where each participant has its own, personal set of quorums. An important question is to determine under what condition is it possible to solve synchronization problems like reliable broadcast or consensus in a heterogeneous quorum system. In this work, we show that the traditional quorum intersection and quorum availability conditions are not sufficient in heterogeneous quorum systems. Moreover, we propose quorum subsumption, a new condition which, together with quorum availability and quorum intersection, is sufficient to allow solving reliable broadcast and consensus. Finally, we propose protocols for reliable broadcast and consensus in heterogeneous quorum systems that satisfy quorum subsumption. In particular, we present a practical consensus protocol called Satrapy which in contrast to abstract consensus protocols uses finite state and messages.
We introduce a formal semantic Bell inequality for multi-agent validation systems and show that the MetaBell operator Ψ, deployed in the PoISV consensus protocol, functions as a rigorous Bell witness for genuine independent understanding. We derive Ψ ≈ 1 − |S̃|/(2√2), connecting Ψ to the Tsirelson bound and replacing the ad-hoc threshold with a data-driven calibrated threshold Ψ*. We further define a Bell-augmented SPVU goal state, an Immutable Incident Log satisfying EU AI Act Art. 12/17/19, a zero-knowledge proof of MetaBell compliance via Nexus zkVM, a Svetlichny-type k≥3 group extension, and the Semantic Bell Test Corpus (SBTC) for empirical validation. DOI: 10.5281/zenodo.19656679
The order-statistic gaps that underlie PPP-residualized functional identity measurement are exactly invariant to log-softmax transformation, exactly equivariant under positive scaling (including temperature), and exactly invariant to any position-independent constant shift applied to the logit vector. These are not empirical approximations — they are mathematical identities that hold for any logit vector over any vocabulary size. The result has been formally verified in Coq (GapInvariance.v: 5 theorems, 2 axioms, 0 Admitted). It retroactively strengthens the empirical API-wall finding reported in earlier work: the order-statistic gap geometry measured through API logprobs does not merely "survive" the log-softmax transformation — it is mathematically immune to it. Any deviation attributable to the API boundary must come from truncation, quantization, or coverage limitations, not from the probability-domain transformation itself. Why this matters. Earlier work showed empirically that PPP-based measurements remained stable when models were accessed through APIs that expose log-probabilities instead of raw logits. This note upgrades that result from empirical robustness to mathematical invariance. It removes the probability-domain transformation itself from the list of plausible failure modes. If an API-based PPP measurement deviates from a weights-based measurement, the cause must lie in truncation, quantization, coverage limitations, or the model — not in log-softmax. The API wall is narrower than previously understood, and the space of plausible objections to API-domain model identity measurement has shrunk by one major category. Supplementary Material. This note is accompanied by GapInvariance.v, a Coq proof file that formally verifies the five gap-invariance theorems described in §2: constant-shift invariance, positive-scale equivariance, affine scaling, log-softmax invariance, and general position-independent shift invariance. The file proves 5 theorems from 2 named axioms (OS1 and OS2), with no unresolved obligations (Admitted), and compiles cleanly under the Rocq Prover 9.1.1 (the current release of the Coq proof assistant, compiled with OCaml 5.4.0). It is available for download as a supplementary file attached to this record. The Neural Network Identity Series — Mathematical foundations, empirical validation, and governance frameworks for verifying which model is running Newest addition: Technical Note: The Disappearing Window — AI Logprob Access Withdrawal and the Structural Verifiability of Frontier Model Contracts (DOI: 10.5281/zenodo.20362098) Paper 1: The δ-Gene: Inference-Time Physical Unclonable Functions from Architecture-Invariant Output Geometry (DOI: 10.5281/zenodo.18704275) Paper 2: Template-Based Endpoint Verification via Logprob Order-Statistic Geometry (DOI: 10.5281/zenodo.18776711) Paper 3: The Geometry of Model Theft: Distillation Forensics, Adversarial Erasure, and the Illusion of Spoofing (DOI: 10.5281/zenodo.18818608) Paper 4: Provenance Generalization and Verification Scaling for Neural Network Forensics (DOI: 10.5281/zenodo.18872071) Paper 5: Beneath the Character: The Structural Identity of Neural Networks — Mathematical Evidence for a Non-Narrative Layer of AI Identity (DOI: 10.5281/zenodo.18907292) Paper 6: Which Model Is Running?: Structural Identity as a Prerequisite for Trustworthy Zero-Knowledge Machine Learning (DOI: 10.5281/zenodo.19008116) Paper 7: The Deformation Laws of Neural Identity (DOI: 10.5281/zenodo.19055966) Paper 8: What Counts as Proof? — Admissible Evidence for Neural Network Identity Claims (DOI: 10.5281/zenodo.19058540) Paper 9: Composable Model Identity — Formal Hardening of Structural Attestations in the Enterprise Identity Stack (DOI: 10.5281/zenodo.19099911) Paper 10:Where Identity Comes From: Path Sensitivity and Endpoint Underdetermination in Neural Network Training (DOI: 10.5281/zenodo.19118807) Paper 11: Post-Hoc Disclosure Is Not Runtime Proof: Model Identity at Frontier Scale (DOI: 10.5281/zenodo.19216634) Paper 12: Family-Dependent Response to Reasoning Distillation Across Structural and Functional Identity Layers (DOI: 10.5281/zenodo.19298857) Paper 13: Safety-Alignment Removal as a Model-Identity Failure — Structural Evidence from Published Weight-Level Mutation Checkpoints (DOI: 10.5281/zenodo.19383019) Technical Note: Agent Identity Is Not Model Identity (DOI: 10.5281/zenodo.19240883) Technical Note: Gap Invariance: Why PPP Measurements Are Domain-Independent by Construction (DOI: 10.5281/zenodo.19275524) Technical Note: Measured Model Substitution Under Valid Agent Credentials (DOI: 10.5281/zenodo.19342848) Technical Note: Artifact Identity Is Not Runtime Identity — Trustfall Lite and the Boundary of File-Level Model Verification (DOI: 10.5281/zenodo.20019127) Formal Verification Stack for Neural Network Structural Identity (IT-PUF Coq Proofs) (DOI: 10.5281/zenodo.18930621) Copyright (c) 2026 Anthony Ray Coslett / Fall Risk AI, LLC. All Rights Reserved. Confidential and Proprietary. Patent Pending (Applications 63/982,893, 63/990,487, 63/996,680, 64/003,244).
Historical Genetic Logic as a Dynamical Coherence Judge for Large Language Models A Rigorous Formalization of Xenopoulos’ Dialectical Operators and Experimental Validation on LLM Self‑Contradiction Katerina XenopoulouIndependent Researcher, Kefalonia, GreeceORCID: 0009-0004-9057-7432Correspondence: katerinaxenopoulou@gmail.com Theoretical Foundation: Epameinondas Xenopoulos †Epistemology of Logic: Logic–Dialectic or Theory of Knowledge (2nd ed., 2024)ORCID: 0009-0000-1736-8555† In memoriam (1920–1994) DOI: 10.5281/zenodo.19263676 https://zenodo.org/uploads/19263676 ABSTRACT Internal self‑contradiction remains a critical failure mode in Large Language Models (LLMs), limiting their reliability in high‑stakes reasoning. While current mitigation strategies like Chain‑of‑Thought (CoT) prompting improve performance, they lack formal guarantees of logical stability. This paper introduces a novel framework for diagnosing and regulating LLM coherence by formalizing Historical Genetic Logic as a Nonlinear Dynamical System. We demonstrate that the reasoning process in autoregressive models can be modeled as a trajectory in a recursive metric space D=⋃n=0∞DnD=⋃n=0∞Dn with Dn+1=[0,1]2×Pfin(Dn)Dn+1=[0,1]2×Pfin(Dn). Our core theoretical contribution, the Xenopoulos Spectral Invariance Theorem (Theorem 7.1), proves that CoT prompting leaves the Lyapunov spectrum invariant, merely extending unstable trajectories without suppressing the underlying chaotic divergence. To address this, we propose the Xenopoulos Layer, a spectral feedback controller that dynamically intervenes in the Jacobian operator Fγ=F−γIFγ=F−γI. By enforcing a negative Lyapunov exponent λ1(γ)<0λ1(γ)<0, the controller provides formal guarantees of stability and coherence. The 34th Principle establishes that any sufficiently expressive autoregressive system with nonlinear reinforcement and memory feedback necessarily admits regions of positive Lyapunov growth—implying that absolute coherence is structurally unattainable, and spectral regulation is therefore essential. Experimental validation across GPT‑4, Claude, Gemini, and DeepSeek architectures shows an 80–100% reduction in logical contradictions compared to state‑of‑the‑art self‑correction methods. Scaling analysis on the Epistemology of Logic corpus (7,816 sentences) demonstrates zero XEPTQLRI instability and τ9τ9 meta‑transcendence, proving that Historical Genetic Logic provides the optimal structural foundation for coherent AI reasoning. The results suggest that transitioning from representation‑level prompting to operator‑level spectral control is essential for the next generation of safe and aligned Artificial Intelligence. Keywords: LLM Coherence, Nonlinear Dynamics, Lyapunov Exponents, Historical Genetic Logic, AI Safety, Spectral Control, Xenopoulos Layer, 34th Principle 1.1 The Problem of Dynamic Reasoning Classical logic was designed to formalize valid inference under the assumption of static propositions and reversible operations. In such systems, truth values are fixed, negation is involutive, and inference rules operate independently of historical accumulation. These assumptions ensure formal clarity but exclude a fundamental property of real reasoning processes: historical evolution. Modern reasoning systems—biological or artificial—do not operate in static propositional spaces. They accumulate memory, amplify internal tensions through nonlinear feedback, and remain subject to stochastic perturbations. Consequently, their behavior may exhibit sensitivity to initial conditions, bounded divergence, and regime transitions—phenomena typically studied in nonlinear dynamical systems rather than in formal logic. The central theoretical difficulty is therefore the following: How can reasoning be modeled as a mathematically rigorous dynamical process that incorporates memory growth, nonlinear reinforcement, and measurable stability properties without reducing it to static Boolean inference? 1.2 The Case of Large Language Models Autoregressive language models generate text by recursively predicting the next token based on previous context. This process can be viewed as a trajectory in a high‑dimensional space, where each step depends on the accumulated history. While such models achieve remarkable performance, they remain prone to internal contradictions, hallucinations, and logical inconsistencies—particularly in long‑form reasoning tasks. Current mitigation strategies, such as Chain‑of‑Thought (CoT) prompting, improve performance by encouraging intermediate reasoning steps but do not provide formal guarantees of logical stability. This gap motivates a dynamical systems approach to reasoning coherence. 1.3 The Theoretical Gap Existing approaches fall into three broad categories: Classical Logic Extensions: Extend Boolean systems but retain reversibility and static semantics. Probabilistic / Bayesian Models: Model uncertainty but not dynamical instability. Optimization‑Based Views: Focus on training dynamics, not reasoning trajectory dynamics. None of these frameworks provide a mathematical language for measuring, predicting, or controlling the emergence of self‑contradiction as a dynamical phenomenon. 1.4 Historical Genetic Logic as a Dynamical System Epameinondas Xenopoulos (1920–1994) developed Historical Genetic Logic as an alternative to static formal logic. His central thesis was that contradiction is not an error to be eliminated but a creative force that drives development. In his framework: Identity is genetic: A→A′A→A′, not A=AA=A Negation is dialectical: ¬D(A)¬D(A) preserves AA while generating its evolution Contradiction is tension: the product of a proposition and its dialectical negation Historicity is memory: the present state incorporates the past These philosophical principles were formalized in a system of 33 principles, 10 axioms, and 5 theorems (Xenopoulos, 2024; Xenopoulou, 2026). The present work builds upon this foundational framework, applying its dynamical core—specifically the memory‑structured recurrence and the instability functional—to model and regulate coherence in Large Language Models. Table 1 summarizes the structural correspondence between the philosophical principles and their mathematical counterparts as used in this work. Table 1: Structural Correspondence: Philosophy to Mathematics Philosophical Principle Mathematical Counterpart Historicity Ht={xτ:τ<t}Ht={xτ:τ<t} Memory‑structured evolution xt+1=F(xt,xt−1,…,xt−m+1)xt+1=F(xt,xt−1,…,xt−m+1) Dialectical intensity at=θt−Atat=θt−At Historical mean μt=1m∑i=1mat−iμt=m1∑i=1mat−i Nonlinear amplification Tt=κat2(1+βtanh(μt))Tt=κat2(1+βtanh(μt)) For the complete mathematical formulation of the foundational system, we refer the reader to the cited works. 1.5 Main Contributions A. Foundational Framework (from Xenopoulos, 2024; Xenopoulou, 2026) A complete metric historical state space for reasoning systems. A non‑Boolean algebra (XLDA) with non‑involutive negation. An irreversible non‑reductive closure principle (INRC). A memory‑structured nonlinear recurrence with positive Lyapunov exponent. A compact partially hyperbolic attractor (XDA). An extended dialectical metric (XDM). A measurable instability functional (XEPTQLRI). B. Contributions of This Work (LLM Application)8. Proof of bounded divergence and analytic ceiling for the recurrence.9. A spectral feedback controller modifying the Jacobian spectrum, applied to LLM trajectories.10. A formal comparison showing that Chain‑of‑Thought does not alter Lyapunov structure.11. A phase transition theory of cognitive regimes in autoregressive models.12. An executable empirical validation protocol for LLM coherence. 1.6 Structure of the Paper Section 2 introduces the formal dialectical state space. Section 3 derives the memory‑structured nonlinear dynamics. Section 4 maps LLM outputs to dynamical trajectories. Section 5 presents the experimental validation framework and summary results. Section 6 develops spectral gap analysis and control. Section 7 compares the framework with Chain‑of‑Thought prompting. Section 8 establishes cognitive phase transition results. Section 9 provides comparative scaling analysis. Section 10 discusses practical logic and developmental interpretation. Section 11 formalizes structural guarantees. Section 12 provides comparative analysis. Section 13 discusses implications and limitations. Section 14 concludes. Section 15 lists references. SECTION 2: FORMAL DIALECTICAL STATE SPACE 2.1 Recursive Construction of the Historical Space Classical logical systems are defined over static propositional domains. In contrast, we define a historically expanding state space. Let D0=[0,1]2×{∅}D0=[0,1]2×{∅} For each n≥0n≥0, define recursively Dn+1=[0,1]2×Pfin(Dn)Dn+1=[0,1]2×Pfin(Dn) where Pfin(Dn)Pfin(Dn) denotes the set of all finite subsets of DnDn. Define the full dialectical space D=⋃n=0∞DnD=n=0⋃∞Dn Interpretation. Each state consists of two bounded components in [0,1]2[0,1]2 and a finite historical memory drawn from lower levels. Thus every element of DD is finitely generated but potentially unbounded in historical depth. 2.2 Dialectical State Definition 2.1 (Dialectical State). A dialectical state is a triple x=(θ,A,H)∈Dnx=(θ,A,H)∈Dn such that: θ,A∈[0,1],H⊂Dn−1,H is finite.θ,A∈[0,1],H⊂Dn−1,H is finite. We interpret θθ as primary assertion component, AA as opposing component, and HH as historical memory. No semantic interpretation is required for formal development. 2.3 Metric Structure We define a recursive metric. Base Level. For x,y∈D0x,y∈D0: d(x,y)=∣θx−θy∣+∣Ax−Ay∣d(x,y)=∣θx−θy∣+∣Ax−Ay∣ Recursive Level. For x,y∈Dn+1x,y∈Dn+1: d(x,y)=∣θx−θy∣+∣Ax−Ay∣+dH(Hx,Hy)d(x,y)=∣θx−θy∣+∣Ax−Ay∣+dH(Hx,Hy) where dHdH is the Hausdorff metric induced by dd: dH(Hx,Hy)=max{suphx∈Hxinfhy∈Hyd(hx,hy), suphy∈Hyinfhx∈Hxd(
We introduce the Theory of Epistemic Abductive Geometry (TEAG), a framework for non-Bayesian inference grounded in admissible-support contraction under possibility theory. The central object is the TEAG quintuple \( \mathcal{E} = (H, \pi, \{H_\alpha\}_{\alpha\in(0,1]}, C, A) \), where evidence acts by contracting the geometry of admissible hypotheses rather than redistributing probabilistic belief mass. The falsification boundary is a tropical variety — exactly. Under the log-admissibility transformation \( \Phi(h) = -\log\pi(h) \), the canonical TEAG conjunctive update becomes tropical addition in the max-plus semiring: \( \Phi^+(h) = \Phi^-(h) \oplus \psi(h) = \max\!\bigl(\Phi^-(h),\,\psi(h)\bigr), \) where \( \psi(h) = -\log\kappa(y\mid h) \) is the surprisal of hypothesis h under observation y. The falsification boundary is the tropical variety of this polynomial: \( \mathcal{F} = \bigl\{h \in H : \Phi^-(h) = \psi(h)\bigr\}. \) This is the exact locus dividing surviving from falsified hypotheses: h is falsified if and only if \( \psi(h) &gt; \Phi^-(h) \); it survives if and only if \( \Phi^-(h) \geq \psi(h) \). Within the class of possibility-theoretic recursive inference systems, this is, to the best of our knowledge, the first exact algebraic expression of Popper's falsification criterion: the boundary is the zero set of a tropical polynomial, determined entirely by the geometry of the prior impossibility and current surprisal fields. Main results. 1. Epistemic Contraction Theorem. Contraction is tropical addition: \( \Phi^+ = \Phi^- \oplus \psi \). Posterior α-cuts satisfy \( H_\alpha^+ = H_\alpha^- \cap E_\alpha(y) \): geometric intersection, not belief redistribution. The falsification boundary is the tropical variety \( \mathcal{F} \). 2. Possibilistic Cramér–Rao Bound (PCRB} For any filter in the class \( \mathcal{F} \) of epistemically admissible, contraction-based recursive estimators satisfying Axioms 2.1–2.5: \( \mathcal{E}_{\pi,k|k} \geq \mathcal{E}_{\pi,k|k-1} + \tfrac{n}{2}\log(1-I_k) \), where \( I_k \) is the Choquet integral of per-hypothesis surprisal against the prior possibility capacity. Within this class, the ESPF [28] is the unique filter achieving this bound with equality, and is therefore the unique minimax-entropy-optimal set-based recursive estimator under bounded epistemic uncertainty. 3. Tropical Hamilton–Jacobi structure (summary). The TEAG update is structurally consistent with a tropical Lagrangian \( L = T - V \), Legendre transform to a tropical Hamiltonian equal to the surprisal field, and a Hamilton–Jacobi equation whose solution is the tropical addition rule. The Euler–Lagrange equations on the epistemic manifold yield geodesic motion with explicit Levi–Civita connection and Christoffel symbols. This structure is interpretive and consistent with the axioms; full derivations are in the companion paper [31]. Taken together, this structure admits a precise interpretation: the TEAG update rule is a max-plus dynamical system whose governing equations have the same algebraic form as the Hamilton–Jacobi equations of classical mechanics, instantiated on hypothesis space rather than physical space. 4. Gaussian collapse. Probability theory is the collapse limit of TEAG as epistemic width \( W \to 0 \): Choquet converges to Lebesgue, the ESPF recovers the Kalman filter, and \( \mathcal{E}_\pi \to \tfrac{1}{2}\log\det\Sigma + \mathrm{const}(n) \). Probability is earned by evidence, not assumed. Epistemic neutrality and knowledge-system synthesis. Because TEAG's axioms require only a hypothesis space, a possibility field, and a contraction operator — not a probability measure, a likelihood function, or a frequentist grounding — heterogeneous knowledge systems can each instantiate the TEAG quintuple independently. Their joint admissible support intersection is the locus of coherence: the set of hypotheses neither system has falsified. No transformation of one system into the other's representational primitives is required. The composition theory (Section 6) formalizes the coupling architecture. Four instantiations provide the unifying structure: the ESPF [28] for recursive state estimation; the Geometry of Knowing [29] for measure-theoretic collapse; the minimax-entropy optimality proof [30]; and the Possibilistic Language Model (PLM, forthcoming [32]).
This is an extended appendix for an unpublished paper. It covers the use of a framework defined in that paper to prove the zero-knowledge of a few zero-knowledge proofs. The first example, covering 3-colourability, is justified and explained. The second, covering boolean circuit satisfiability, is simply given.
In the face of the regulatory failure problem caused by blockchain hidden addresses, existing solutions often fall into a dilemma where 'privacy protection' and 'compliance review' are either one or the other.This paper proposes an innovative integration framework that transforms the behavioural elements in anti-money laundering and other legal provisions (such as 'high-frequency and small-scale transactions') into computable logic.Based on zero-knowledge proof technology, it generates verifiable credentials to determine whether the transaction behaviour is compliant without revealing the true identity of the address.Experiments on a public blockchain transaction dataset (elliptic) show that this framework achieves an average improvement of over 15% in core identification performance compared to traditional non-private rule-based methods, while maintaining an acceptable performance overhead.As a proof-of-concept validation conducted on a transparent dataset with simulated concealment, the actual performance may differ in native privacy-preserving chains.This research provides a new approach that combines legal rigor with technical feasibility for achieving effective on-chain behaviour supervision while protecting user privacy.
Arthur Ramos, Anjolina Grisi de Oliveira, Ruy de Queiroz, Tiago M. L. de Veras
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond property, Newmans lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. All theorems are fully mechanized with zero axioms or sorry statements. We provide complete proofs of de Bruijn substitution infrastructure and demonstrate strong normalization via logical relations. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4.
Applies the Evidence-Based Subjective Logic (EBSL) framework to zero-knowledge reputation systems and decentralised identity. Demonstrates how reputation opinions that are provably correct can be published without revealing the underlying evidence graph, using the EZKL zkML framework for proof generation.
Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel, Ning Luo
Efficient zero-knowledge proofs (ZKPs) have been restricted to NP statements so far, whereas they exist for all statements in PSPACE. This work presents the first practical zero-knowledge (ZK) protocols for PSPACE-complete statements by enabling ZK proofs of QBF (Quantified Boolean Formula) evaluation. The core idea is to validate quantified resolution proofs (Q-Res) in ZK. We develop an efficient polynomial encoding of Q-Res proofs, enabling proof validation through low-overhead arithmetic checks. We also design a ZK protocol to prove knowledge of a winning strategy related to the QBF, which is often equally important in practice. We implement our protocols and evaluate them on QBFEVAL. The results show that our protocols can verify 72% of QBF evaluations via Q-Res proof and 82% of instances' winning strategies within 100 seconds, for instances where such proofs or strategies can be obtained.
Computer-aided cryptography, with particular emphasis on formal verification, promises an interesting avenue to establish strong guarantees about cryptographic primitives. The appeal of formal verification is to replace the error-prone pen-and-paper proofs with a proof that was checked by a computer and, therefore, does not need to be checked by a human. In this paper, we ask the question of how reliable are these machine-checked proofs by analyzing a formally verified implementation of the Line-Point Zero-Knowledge (LPZK) protocol (Dittmer, Eldefrawy, Graham-Lengrand, Lu, Ostrovsky and Pereira, CCS 2023). The implementation was developed in EasyCrypt and compiled into OCaml code that was claimed to be high-assurance, i.e., that offers the formal guarantees of guarantees of completeness, soundness, and zero knowledge. We show that despite these formal claims, the EasyCrypt model was flawed, and the implementation (supposed to be high-assurance) had critical security vulnerabilities. Concretely, we demonstrate that: 1) the EasyCrypt soundness proof was incorrectly done, allowing an attack on the scheme that leads honest verifiers into accepting false statements; and 2) the EasyCrypt formalization inherited a deficient model of zero knowledge for a class of non-interactive zero knowledge protocols that also allows the verifier to recover the witness. In addition, we demonstrate 3) a gap in the proof of the perfect zero knowledge property of the LPZK variant of Dittmer, Ishai, Lu and Ostrovsky (CCS 2022) that the EasyCrypt proof is based, which, depending on the interpretation of the protocol and security claim, could allow a malicious verifier to learn the witness. Our findings highlight the importance of scrutinizing machine-checked proofs, including their models and assumptions. We offer lessons learned for both users and reviewers of tools like EasyCrypt, aimed at improving the transparency, rigor, and accessibility of machine-checked proofs. By sharing our methodology and challenges, we hope to foster a culture of deeper engagement with formal verification in the cryptographic community.
Antoine Bak, Guilhem Jazeron, Pierre Galissant, Léo Perrin
In recent years, many hash functions have been introduced to satisfy the pressing need of some zero-knowledge protocols for such primitives allowing a low degree verification of their round function when arithmetized over a large field.While this can be achieved by restricting their sub-components to low-degree functions (and their inverse), the newest primitives in this category also leverage the intricacies of some proof systems to use “Split-and-Lookup” non-linear functions that essentially apply a small S-box in parallel over the binary representation of a field element.Such components excel at hindering attacks relying on polynomial system solving, but they offer poor security against statistical attacks. On the other hand, low degree monomials offer the opposite guarantees, being strong against statistical attacks. Several primitives have recently been proposed that combine such components in different ways in order to get the best from both.In this paper, we target such primitives by relying on the low degree components to allow a low-cost polynomial solving step. The weakness of Split-and-Lookups against linear attacks is used to simplify these systems, and their weakness against differential attacks is then used to propagate across many rounds the differential patterns obtained during polynomial solving. We instantiate this general approach by attacking round-reduced Monolith, and providing a distinguisher on full-round Skyscraper. These result then shed some light on how to best combine the different types of components to achieve the highest security.