DE
plain-language theorem explainer
DE defines the discrete edge rule requiring that an integer-valued potential p on recognition structure M increases by exactly δ along every edge of the recognition relation R. Researchers formalizing T4 uniqueness and affine ledger properties cite this predicate when proving constancy of differences along reachability components. The definition is a direct predicate packaging the edge condition with no auxiliary lemmas or proof obligations.
Claim. Let $M$ be a recognition structure with universe $U$ and binary relation $R$. An integer-valued potential $p:U→ℤ$ satisfies the discrete edge rule with increment $δ∈ℤ$ when $p(b)-p(a)=δ$ for every pair $a,b$ such that $a$ $R$ $b$.
background
Pot is the abbreviation for integer-valued functions on the universe $U$ of a RecognitionStructure $M$. The structure $M$ supplies the recognition relation $R$ (defined via recog in the Recognition module and specialized in Cycle3). The module supplies dependency-light T4 uniqueness lemmas on discrete reach sets, using the Kin kinematics derived from $R$. Upstream, the ContinuumBridge.as structure identifies Laplacian actions with weighted edge differences, while the Pot abbreviation directly supplies the codomain $ℤ$ for the potentials appearing in DE.
proof idea
This is a direct definition of the edge-increment predicate. No lemmas are applied inside the declaration; the body simply quantifies over $M.R$ edges and equates the potential difference to the constant $δ$.
why it matters
DE supplies the central hypothesis for the T4 uniqueness chain in the Potential module, appearing in downstream results such as increment_on_ReachN (quantization along ReachN), diff_const_on_component (constancy of differences), and IsAffine (affine ledgers via phi). It encodes the discrete potential rule that follows from the recognition relation in the T4 step of the forcing chain, enabling the eight-tick octave and spatial dimension derivations to proceed on integer potentials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.