Encyclopedia Gravity Gravity Seven Gaps Ledger Energy Bridge General Antisymmetric Strain Can Violate

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Ledger Energy Bridge General Antisymmetric Strain Can Violate

A machine-checked proof shows that a proposed bridge from discrete records to geometry only works for a restricted class of deformations, and gives a concrete counterexample for why.

Verify this page

The boundary of a bridge

In the Recognition Science framework, a ledger is a discrete record of events, and the framework's central cost function J(x) = (x + 1/x)/2 - 1 measures the price of a recognition event. A key question is how this ledger connects to the geometry of space. The bridge under examination here would say that the ledger's total cost for a deformation equals a geometric curvature energy. The declaration general_antisymmetric_strain_can_violate_rcl is a theorem that proves this bridge is not universally valid.

The bridge is built on a gate condition. For a strain field s, which assigns a number to each ordered pair of cells, the ledger's cost is well-defined only if a certain inequality, the RCL gate, holds. The theorem shows that for a general strain field that is antisymmetric (s i j = -s j i), this gate can fail. The proof exhibits a specific strain on three cells, defined by gateViolatingStrain, where the inequality is violated. This is a concrete counterexample, not a vague possibility.

The construction therefore works only for a restricted class of strains: those that are coboundaries. A strain is a coboundary if it can be written as a difference of a single potential function, s i j = f i - f j. For these, the gate holds, and the bridge is a theorem. The proof that the gate can fail for general antisymmetric strains is what makes this restriction a theorem-backed necessity, not a convenience. The framework is not claiming the bridge works everywhere; it is precisely mapping where it does and does not.

This result is part of a larger effort to correct an earlier, failed bridge. The corrected bridge uses a quadratic curvature energy, defined purely from geometric hinge data, and matches it to the ledger's cost for coboundary strains. The theorem coboundary_totalCost_quadratic_matching provides this match. A further result shows that a pure shear deformation, which the old bridge was blind to, carries strictly positive ledger energy, meaning the new bridge sees it. The failure of the general antisymmetric case is the sharp edge that defines the bridge's valid domain.

What the declaration does not claim is equally important. It does not claim that the bridge fails for all antisymmetric strains, only that it can fail. It does not claim that the corrected bridge is a complete theory of gravity; the comparison against independently derived Regge geometry remains open. The theorem is a precise, negative result that scopes the valid domain of a construction, and in doing so, it clarifies what the framework can and cannot yet say about the link between its discrete ledger and continuous geometry.

THEOREM general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:313 
/-- **THEOREM (honest scoping witness).** A general ANTISYMMETRIC strain
field need not yield an RCL-subadditive cost: on three cells, the
antisymmetric strain with s 0 2 = 1 but s 0 1 = s 1 2 = 0 gives
J(exp(s 0 2)) > 0 = R(J(exp(s 0 1)), J(exp(s 1 2))). This is why
`coboundaryStrainLedger` is scoped to coboundary strains: the scoping is
forced, not chosen. -/
theorem general_antisymmetric_strain_can_violate_rcl :
    ∃ s : Fin 3 → Fin 3 → ℝ, (∀ i j, s i j = - s j i) ∧
      ¬ (Cost.Jcost (Real.exp (s 0 2)) ≤
          RecognitionLedger.rclGate (Cost.Jcost (Real.exp (s 0 1)))
            (Cost.Jcost (Real.exp (s 1 2)))) := by
  refine ⟨gateViolatingStrain, gateViolatingStrain_antisymm, ?_⟩
  obtain ⟨h02, h01, h12⟩ := gateViolatingStrain_vals
  rw [h02, h01, h12, Real.exp_zero, Cost.Jcost_unit0]
  have hgate : RecognitionLedger.rclGate 0 0 = 0 := by
    unfold RecognitionLedger.rclGate
    ring
  rw [hgate]
  have hone : (1 : ℝ) < Real.exp 1 :=
    lt_trans (by norm_num) Real.exp_one_gt_d9
  have hpos : 0 < Cost.Jcost (Real.exp 1) :=
    Cost.Jcost_pos_of_ne_one _ (Real.exp_pos 1) (ne_of_gt hone)
  linarith
THEOREM gateViolatingStrain_vals · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
gateViolatingStrain_vals · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:300 
/-- **THEOREM.** Values of the gate-violating strain on the relevant pairs.
(Uses `decide` only for `Fin 3` literal disequalities.) -/
theorem gateViolatingStrain_vals :
    gateViolatingStrain 0 2 = 1 ∧ gateViolatingStrain 0 1 = 0 ∧
      gateViolatingStrain 1 2 = 0 := by
  have h20 : ¬((2 : Fin 3) = 0) := by decide
  have h02 : ¬((0 : Fin 3) = 2) := by decide
  have h12 : ¬((1 : Fin 3) = 2) := by decide
  have h10 : ¬((1 : Fin 3) = 0) := by decide
  refine ⟨?_, ?_, ?_⟩ <;>
    · unfold gateViolatingStrain
      norm_num [h20, h02, h12, h10]
THEOREM rclGate_Jcost_eq · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
rclGate_Jcost_eq · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:227 
/-- **THEOREM (the panel's key identity).** The RCL gate evaluated on two
J-costs is EXACTLY the J-cost of the product ratio plus the J-cost of the
quotient ratio: R(J(x), J(y)) = J(xy) + J(x/y) for x, y > 0. Since
J(x/y) ≥ 0, the gate inequality J(xy) ≤ R(J(x), J(y)) follows with
identified slack J(x/y). Pure algebra from `Cost.dalembert_identity`. -/
theorem rclGate_Jcost_eq {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
    RecognitionLedger.rclGate (Cost.Jcost x) (Cost.Jcost y)
      = Cost.Jcost (x * y) + Cost.Jcost (x / y) := by
  have h := Cost.dalembert_identity hx hy
  unfold RecognitionLedger.rclGate
  linarith
THEOREM rectangleShear_ledgerEnergy_pos · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
rectangleShear_ledgerEnergy_pos · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:519 
/-- **THEOREM (shear-visibility gate).** The pure-shear rectangle strain
carries strictly positive ledger energy for every h ≠ 0. Shear is VISIBLE
to the corrected J-ledger bridge: the cell cost on the horizontal edge is
J(exp h) = cosh h − 1 > 0, and all cell costs are nonnegative. This is
exactly the transverse-traceless sector on which the conformal-average
ansatz was proved blind
(`Gravity.conformal_ansatz_cannot_recover_gravitational_waves`). -/
theorem rectangleShear_ledgerEnergy_pos (h : ℝ) (hh : h ≠ 0) :
    0 < RecognitionLedger.totalCost
      (coboundaryStrainLedger (rectangleShearPotential h)) := by
  classical
  unfold RecognitionLedger.totalCost
  have hval : rectangleShearPotential h 0 - rectangleShearPotential h 1
      = h := (rectangleShearPotential_strains h).1
  have hterm :
      0 < (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 1 := by
    show 0 < Cost.Jcost (Real.exp
      (rectangleShearPotential h 0 - rectangleShearPotential h 1))
    rw [hval, Cost.Jcost_exp_cosh]
    have hcosh : 1 < Real.cosh h := Real.one_lt_cosh.mpr hh
    linarith
  have hinner :
      0 < ∑ j, (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 j := by
    have hle := Finset.single_le_sum
      (f := fun j => (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 j)
      (fun j _ => (coboundaryStrainLedger (rectangleShearPotential h)).nonneg 0 j)
      (Finset.mem_univ 1)
    linarith
  have houter := Finset.single_le_sum
    (f := fun i => ∑ j, (coboundaryStrainLedger (rectangleShearPotential h)).cost i j)
    (fun i _ => Finset.sum_nonneg fun j _ =>
      (coboundaryStrainLedger (rectangleShearPotential h)).nonneg i j)
    (Finset.mem_univ 0)
  exact lt_of_lt_of_le hinner houter

What this page does not claim

The bridge fails for all antisymmetric strains, only that it can fail. The corrected bridge is a complete theory of gravity, as the comparison against independently derived Regge geometry remains open. The theorem establishes the physical recognition-to-linking bridge, which is itself an open target.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND