pith. machine review for the scientific record. sign in
theorem proved term proof high

ratio_rigidity

show as:
view Lean formalization →

On a connected graph, vanishing J-cost on every edge forces any positive vertex field to be constant. Holography derivations in the GCIC paper and brain models cite this to obtain global uniformity from local zero-cost conditions. The term-mode proof invokes the preconnected constancy lemma after reducing each adjacent ratio to unity via the unique zero of J.

claimLet $G=(V,adj)$ be a graph such that the reflexive-transitive closure of $adj$ relates every pair of vertices. Suppose $x:V→ℝ$ satisfies $0<x(v)$ for all $v$ and $J(x(v)/x(w))=0$ whenever $adj(v,w)$. Then $x(v)=x(w)$ for all $v,w∈V$.

background

The module establishes graph rigidity for ratio-based energies in the GCIC framework. The J-cost function satisfies $J(y)=0$ if and only if $y=1$ for $y>0$, as stated in Jcost_zero_iff_one. Connectivity is expressed via Relation.ReflTransGen adj, the smallest reflexive transitive relation containing adj. Upstream results include the definition of Jcost from the multiplicative recognizer and its equivalence to the hyperbolic cosine form.

proof idea

The proof is a one-line wrapper applying constant_of_preconnected to the connectivity hypothesis. For each adjacent pair, positivity of the ratio allows Jcost_zero_iff_one to conclude the ratio equals 1, after which algebraic rearrangement via div_eq_iff and one_mul yields equality of the field values.

why it matters in Recognition Science

This theorem is Result 1 of the GCIC paper and supplies the rigidity step in multiple downstream derivations, including boundary_encodes_bulk and brain_holography_inevitable. It closes the gap from local J-minima to global constancy, enabling the holographic principle that boundary data determines the bulk. In the Recognition Science chain it rests on T5 uniqueness of J and feeds the eight-tick octave and D=3 emergence by ensuring uniform fields on connected structures.

scope and limits

Lean usage

theorem cache_nodes_uniform (cache : LocalCache V) (v w : V) : cache.field v = cache.field w := ratio_rigidity cache.graph_connected cache.field_positive cache.at_J_minimum v w

formal statement (Lean)

  67theorem ratio_rigidity {adj : V → V → Prop}
  68    (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
  69    {x : V → ℝ} (hpos : ∀ v, 0 < x v)
  70    (hzero : ∀ v w, adj v w → Jcost (x v / x w) = 0) :
  71    ∀ v w : V, x v = x w := by

proof body

Term-mode proof.

  72  apply constant_of_preconnected hconn
  73  intro v w hvw
  74  have hdiv_pos : 0 < x v / x w := div_pos (hpos v) (hpos w)
  75  have h1 : x v / x w = 1 := Jcost_zero_iff_one hdiv_pos (hzero v w hvw)
  76  rwa [div_eq_iff (ne_of_gt (hpos w)), one_mul] at h1
  77
  78/-- **Converse:** constant positive fields have zero ratio cost on every edge. -/

used by (14)

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

depends on (11)

Lean names referenced from this declaration's body.