bidirectional_destroys_ordering
A positivity lemma shows that the product of blend rate η and reverse-edge weight w_back stays strictly positive when both factors are positive. Researchers modeling causal signal flow on graphs with bidirectional shortcuts would cite this algebraic fact when proving that reverse activation can match forward speed and thereby erase strict temporal order. The argument is a direct one-line application of the multiplication-positivity lemma to the two given hypotheses.
claimLet $w_>0$, $w_<0$, and $η>0$ be real numbers. Then $η·w_<0$.
background
The module examines whether sparse-matrix-vector multiplication preserves causal ordering on graphs that combine directed chains with bidirectional shortcuts. The blend rate η is the per-hop attenuation factor, conventionally set to 1/φ² in RS-native units. The fundamental time quantum is the tick τ₀ = 1, and one octave spans eight ticks. Upstream results supply the tick definition as the RS time quantum together with structural predicates that certify collision-free graphs and edge-length assignments.
proof idea
The proof is a one-line wrapper that applies the mul_pos lemma directly to the positivity hypotheses on η and w_back.
why it matters in Recognition Science
The lemma supplies the algebraic positivity required to conclude that a reverse-edge contribution remains strictly positive, which is the key step showing that bidirectional shortcuts (SBERT kNN edges) destroy causal ordering. It supports the module's diagnostic claim that SpMV flattens causality rather than preserving it, and it sits inside the Recognition Science derivation of the eight-tick octave and three spatial dimensions from the J-uniqueness fixed-point equation.
scope and limits
- Does not prove the full ordering-destruction statement for arbitrary graphs.
- Does not quantify hop reach or octave sufficiency.
- Does not invoke the specific numerical value of the blend rate beyond positivity.
- Does not address multi-hop propagation bounds.
formal statement (Lean)
118theorem bidirectional_destroys_ordering (w_forward w_back : ℝ)
119 (hf : 0 < w_forward) (hb : 0 < w_back) (η : ℝ) (hη : 0 < η) :
120 η * w_back > 0 := by
proof body
Term-mode proof.
121 exact mul_pos hη hb
122
123/-! ## Effective Reach Bounds -/
124
125/-- Signal strength at hop distance d: η^d.
126 This is the peak activation a node at distance d ever achieves
127 (occurring at the tick when signal first arrives). -/