Gravity Seven Gaps Ledger Bridge No Go Even And Odd Forces Zero

The even-odd exclusion

In mathematics, a function is even when flipping the sign of its input leaves it unchanged, and odd when flipping the sign of its input also flips the sign of its output. The only real number that is both its own negative is zero. So if an even function and an odd function are forced to be equal everywhere, the only possible value for either of them is zero at every point. This is the content of the theorem even_and_odd_forces_zero in the framework's machine-checked library of formal theorems.

Within Recognition Science, the result lands in a specific debate. The framework models physical structure as a ledger, a discrete record of recognition events whose cost is forced by a proved uniqueness theorem. A proposed bridge would equate the ledger's deficit at each cell with a raw geometric hinge deficit, a signed quantity that can be positive or negative. The framework proves two obstructions. First, ledger deficits are sums of nonnegative costs, so any such bridge forces the geometric deficit to be nonnegative on its image, ruling out any specification with a strictly negative deficit. Second, for the natural family of exponential strain ratios, the induced ledger deficit is an even function of the deformation parameter, while the signed Regge deficit response is odd. The even-odd exclusion then forces both to vanish identically, meaning no signed linear response can be realized.

The theorem itself is a pure statement about real functions, proved with no framework-specific axioms. What it establishes is a parity obstruction: a J-ratio ledger family with the natural ratio parity cannot match a signed linear-response deficit on any symmetric interval. The framework's corrected bridge target is therefore not the raw signed deficit but a nonnegative curvature-quadratic energy. The geometric premise that two-sided weak-field deformation classes contain negative deficits and odd leading responses is not formalized in the file; it is a stated assumption that motivates the no-go result.

/-- **THEOREM (even vs. odd exclusion).** An even function of ε can equal an
odd function of ε only if both vanish identically. -/
theorem even_and_odd_forces_zero (g d : ℝ → ℝ)
    (hg : ∀ ε, g (-ε) = g ε) (hd : ∀ ε, d (-ε) = - d ε)
    (hmatch : ∀ ε, g ε = d ε) (ε : ℝ) :
    g ε = 0 ∧ d ε = 0 := by
  have h1 : d ε = - d ε := by
    calc d ε = g ε := (hmatch ε).symm
      _ = g (-ε) := (hg ε).symm
      _ = d (-ε) := hmatch (-ε)
      _ = - d ε := hd ε
  have h2 : d ε = 0 := by linarith
  exact ⟨(hmatch ε).trans h2, h2⟩

/-- **THEOREM (sign obstruction, positive form).** Any bridge satisfying the
assumed deficit-matching condition forces the geometric deficit to be
nonnegative at every hinge in the image of the comparison map `x_sigma`.
Direct consequence of `RecognitionLedger.deficit_nonneg`: ledger deficits
are sums of nonnegative J-costs. -/
theorem bridge_forces_nonneg_geometricDeficit
    {Λ : Type*} [Fintype Λ] [DecidableEq Λ] {H : Type*}
    (L : RecognitionLedger.RecognitionLedger Λ)
    (B : LedgerToHingeBridge H L) (i : Λ) :
    0 ≤ B.geometricDeficit (B.x_sigma i) := by
  rw [← B.bridge_assumed i]
  exact RecognitionLedger.deficit_nonneg L i

/-- **THEOREM (parity no-go, deficit form).** The J-ratio deficit at every
cell is an EVEN function of the deformation parameter ε. Its response to a
deformation therefore has no odd part: the leading term is O(ε²), never the
signed O(ε) linear response of a weak-field Regge deficit. -/
theorem jRatioDeficit_even {Λ : Type*} [Fintype Λ] (s : Λ → Λ → ℝ) (ε : ℝ)
    (i : Λ) :
    jRatioDeficit s (-ε) i = jRatioDeficit s ε i := by
  unfold jRatioDeficit
  exact Finset.sum_congr rfl fun j _ => jRatioCellCost_even s ε i j

/-- **THEOREM (parity no-go, ledger-family linear-response form).** No
one-parameter family of recognition ledgers with parity-covariant J-ratio
costs can have a deficit matching a signed linear response c·ε (c ≠ 0) on
any symmetric interval. -/
theorem no_ledger_family_linear_response
    {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
    (L : ℝ → RecognitionLedger.RecognitionLedger Λ)
    (r : ℝ → Λ → Λ → ℝ)
    (hpos : ∀ ε i j, 0 < r ε i j)
    (hcost : ∀ ε i j, (L ε).cost i j = Cost.Jcost (r ε i j))
    (hpar : ∀ ε i j, r (-ε) i j = (r ε i j)⁻¹)
    (i : Λ) (c a : ℝ) (hc : c ≠ 0) (ha : 0 < a) :
    ¬ (∀ ε : ℝ, |ε| ≤ a → RecognitionLedger.deficit (L ε) i = c * ε) := by
  intro hmatch
  have hpa : RecognitionLedger.deficit (L a) i = c * a :=
    hmatch a (le_of_eq (abs_of_pos ha))
  have habs : |(-a)| = a := by
    rw [abs_neg]
    exact abs_of_pos ha
  have hna : RecognitionLedger.deficit (L (-a)) i = c * (-a) :=
    hmatch (-a) (le_of_eq habs)
  rw [ledger_family_deficit_even_of_ratio_parity L r hpos hcost hpar a i]
    at hna
  have hca : c * a = 0 := by linarith
  rcases mul_eq_zero.mp hca with h | h
  · exact hc h
  · exact absurd h (ne_of_gt ha)

What this page does not claim

The geometric premise that two-sided weak-field Regge classes contain negative deficits and odd leading response is not proved in this file. The theorem does not rule out all possible bridges, only those with parity-covariant J-ratio costs. The framework does not derive the fine-structure constant or any specific coupling constant from this result.

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/LedgerBridgeNoGo.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: