pith. machine review for the scientific record. sign in
def definition def or abbrev high

blend_step

show as:
view Lean formalization →

The blend_step definition supplies the single-step update rule for node activation under linear blending: new value equals (1-η) times current activation plus η times incoming signal. Researchers modeling discrete causal graphs in Recognition Science cite it when deriving hop decay and ordering preservation on directed chains. The definition is a direct algebraic expression with no lemmas or case analysis.

claimThe blended activation is given by $(1 - η) ψ_{current} + η ψ_{incoming}$, where η is the blend rate and ψ denotes node activation.

background

The Causal Propagation Ordering module examines whether SpMV propagation on directed graphs preserves causal ordering and whether the 8-tick octave suffices for multi-hop reach. The blend rate η is fixed at 1/φ² in RS-native units, matching the engineering constant ETA_BLEND. The fundamental time quantum is the tick τ₀ = 1, with one octave defined as 8 ticks.

proof idea

This is a direct definition that implements the convex combination formula in one algebraic line. No upstream lemmas are invoked; the expression is written verbatim from the propagation model described in the module doc-comment.

why it matters in Recognition Science

The definition supplies the core update rule underlying module results such as hop_ordering_preserved and effective_reach_bound. It operationalizes the propagation step inside the 8-tick octave framework (T7) and connects to the question of whether directed chains maintain ordering before shortcuts appear. The module doc-comment explicitly ties it to the blended = (1-η)·my_psi + η·prop model.

scope and limits

formal statement (Lean)

  48def blend_step (current : ℝ) (incoming : ℝ) (η : ℝ) : ℝ :=

proof body

Definition body.

  49  (1 - η) * current + η * incoming
  50
  51/-- Activation at hop distance d from source after t ticks of pure blend,
  52    assuming the source has unit activation and directed chain topology.
  53    At distance d, signal arrives at tick d and decays as η^d per hop. -/

depends on (11)

Lean names referenced from this declaration's body.