Papers Gcic Graph Rigidity

Graph rigidity

Graph rigidity is a established result in Recognition Science about ratio energy, the total cost of mismatch between neighboring values on a graph, measured by the reciprocal cost function J. The theorem states that on any finite connected graph, if the ratio energy vanishes on every edge, then the positive field is constant across the whole graph. In plain language, zero total mismatch forces perfect uniformity.

The proof has two parts. First, the unique zero of J at unity means an edge cost of zero forces the two endpoint values to be equal. Second, connectivity propagates that local agreement along paths to every pair of vertices. The full characterization is an iff: a positive field has zero ratio cost on every edge exactly when it is constant.

This is machine-verified in Lean 4 as Result 1 of the GCIC paper, with no unverified axioms. The theorem gives a precise sense in which the reciprocal cost function is rigid: it cannot hide local variation while reporting zero total cost.

THEOREM ratio_rigidity · IndisputableMonolith/Papers/GCIC/GraphRigidity.lean

THEOREM ratio_rigidity_iff · IndisputableMonolith/Papers/GCIC/GraphRigidity.lean

THEOREM edge_cost_zero_iff · IndisputableMonolith/Papers/GCIC/GraphRigidity.lean

THEOREM constant_of_preconnected · IndisputableMonolith/Papers/GCIC/GraphRigidity.lean

What this page does not claim

This answer does not claim that the GCIC paper's other results are verified. This answer does not claim that the rigidity theorem applies to fields that are not positive.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Papers/GCIC/GraphRigidity.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: