Pot
Pot defines the type of all integer-valued functions on the universe U of a RecognitionStructure M. Kinematics and uniqueness results in the Potential module cite this type when proving that potential differences remain constant along reach components. The declaration is a direct abbreviation for the function type M.U → ℤ with no additional axioms or computation.
claimLet $M$ be a RecognitionStructure with universe $U$. Then Pot$(M)$ is the set of all functions $p : U → ℤ$.
background
A RecognitionStructure consists of a type U together with a binary relation R : U → U → Prop that encodes recognition edges. The structure is imported from IndisputableMonolith.Recognition and IndisputableMonolith.Chain, where it is defined minimally with U and R; some variants add reflexivity and symmetry. The Potential module supplies dependency-light T4 uniqueness lemmas on discrete reach sets, using Pot as the carrier type for functions that will later satisfy the discrete edge rule DE.
proof idea
Direct abbreviation: Pot is introduced as the function type M.U → ℤ. No lemmas or tactics are invoked; the declaration simply renames the arrow type for use in downstream definitions such as DE and the reach lemmas.
why it matters in Recognition Science
Pot supplies the type for all subsequent potential statements, including DE (the discrete edge rule) and the family of T4 uniqueness results (diff_const_on_component, T4_unique_on_component, increment_on_ReachN). These lemmas establish that potentials change by exact multiples of δ along reaches, anchoring the discrete kinematics that feed the forcing chain (T5–T8) and the quantization of increments in RS-native units. It touches the open question of lifting the discrete potential to the continuous case in the full Recognition Science derivation.
scope and limits
- Does not fix any particular increment δ.
- Does not assume the recognition graph is connected.
- Does not impose continuity or smoothness on the functions.
- Does not relate the discrete potential to any continuous field.
formal statement (Lean)
12abbrev Pot (M : Recognition.RecognitionStructure) := M.U → ℤ
proof body
Definition body.
13
14/-- Discrete edge rule: along any edge, `p` increases by `δ` on `M.R`. -/