pith. sign in
module module high

IndisputableMonolith.Potential

show as:
view Lean formalization →

The Potential module defines the discrete potential p on the recognition monolith M such that p increases by a fixed increment δ along every edge in the relation M.R. Researchers analyzing causal structure or ledger properties in Recognition Science cite it to ground potential differences. The module supplies a set of definitions and invariance lemmas rather than a single central proof.

claimThe potential function $p$ on monolith $M$ satisfies $p(y)-p(x)=δ$ for every edge $(x,y)$ belonging to the relation $M.R$.

background

This module sits inside the Recognition Science framework and imports the core Recognition module whose opening statement is T1 (MP): Nothing cannot recognize itself. It also imports Causality.Basic to supply the underlying edge relation. The module introduces the potential Pot together with auxiliary notions DE and Kin, plus lemmas such as edge_diff_invariant and diff_const_on_ReachN that track how differences behave on reachable sets.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the discrete edge rule that feeds directly into the LedgerUniqueness module. It encodes the potential increment rule as a foundational piece of the Recognition Science monolith, enabling later uniqueness arguments on the ledger.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)