Gravity Seven Gaps Ledger Energy Bridge Rectangle Shear Potential Strains

The shear pattern

Shear is the deformation that turns a square into a rhombus of the same area: one pair of opposite sides stretches while the other pair compresses by the same amount. The declaration rectangleShearPotential_strains is a theorem in the framework's machine-checked library of formal theorems. It states, for any real number h, that the potential (0, −h, 0, −h) on the four corners of a rectangle produces exactly this pattern: the horizontal edge differences are h and −h, and the vertical edge differences are −h and h.

In plain terms, the theorem certifies that the chosen potential is a faithful encoding of pure shear. The potential assigns a number to each corner; the strain between two corners is the difference of their numbers. The theorem proves that these differences match the shear pattern: horizontal strain h, vertical strain −h, and the two diagonal differences also equal h and −h. This is a definitional check, not a physical law. The theorem does not say that shear is the only deformation, nor that this potential is unique.

The theorem matters because it is the hinge of a larger result. The same library proves that this shear pattern carries strictly positive ledger energy for any nonzero h, and that its quadratic hinge energy is also strictly positive. That means the corrected bridge between the ledger and geometry sees shear, where an earlier conformal-average ansatz was blind. The declaration itself, however, only establishes the strain pattern; the positivity results are separate theorems.

In Recognition Science, the ledger is a discrete record of events with a forced cost. Here the ledger is built from the potential differences, and the cost is the J-cost. The theorem does not claim that the ledger is the only way to describe shear, nor that the potential (0, −h, 0, −h) is physically realizable. It is a mathematical statement about a specific encoding.

/-- **THEOREM.** The rectangle shear potential realizes the pure-shear
strain pattern: horizontal strains h, vertical strains −h.
(Uses `decide` only for `Fin 4` literal disequalities.) -/
theorem rectangleShearPotential_strains (h : ℝ) :
    rectangleShearPotential h 0 - rectangleShearPotential h 1 = h ∧
    rectangleShearPotential h 2 - rectangleShearPotential h 3 = h ∧
    rectangleShearPotential h 1 - rectangleShearPotential h 2 = -h ∧
    rectangleShearPotential h 3 - rectangleShearPotential h 0 = -h := by
  have h01 : ¬((0 : Fin 4) = 1) := by decide
  have h03 : ¬((0 : Fin 4) = 3) := by decide
  have h21 : ¬((2 : Fin 4) = 1) := by decide
  have h23 : ¬((2 : Fin 4) = 3) := by decide
  have h13 : ¬((1 : Fin 4) = 3) := by decide
  have h31 : ¬((3 : Fin 4) = 1) := by decide
  unfold rectangleShearPotential
  norm_num [h01, h03, h21, h23, h13, h31]

/-- **THEOREM.** The rectangle shear potential realizes the pure-shear
strain pattern: horizontal strains h, vertical strains −h.
(Uses `decide` only for `Fin 4` literal disequalities.) -/
theorem rectangleShearPotential_strains (h : ℝ) :
    rectangleShearPotential h 0 - rectangleShearPotential h 1 = h ∧
    rectangleShearPotential h 2 - rectangleShearPotential h 3 = h ∧
    rectangleShearPotential h 1 - rectangleShearPotential h 2 = -h ∧
    rectangleShearPotential h 3 - rectangleShearPotential h 0 = -h := by
  have h01 : ¬((0 : Fin 4) = 1) := by decide
  have h03 : ¬((0 : Fin 4) = 3) := by decide
  have h21 : ¬((2 : Fin 4) = 1) := by decide
  have h23 : ¬((2 : Fin 4) = 3) := by decide
  have h13 : ¬((1 : Fin 4) = 3) := by decide
  have h31 : ¬((3 : Fin 4) = 1) := by decide
  unfold rectangleShearPotential
  norm_num [h01, h03, h21, h23, h13, h31]

What this page does not claim

The theorem does not claim that shear is the only deformation pattern. The theorem does not claim that the potential (0, −h, 0, −h) is physically realizable. The theorem does not claim that the ledger energy of shear is positive; that is a separate theorem.

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/Gravity/SevenGaps/LedgerEnergyBridge.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: