Gravity Seven Gaps Stationarity Bridge Closure Concrete Stationarity Bridge Log

A signed example

The declaration concreteStationarityBridge_logRatio_signed establishes a concrete, non-vacuous example within the Recognition Science framework. It proves that for a specific configuration of a recognition bridge, the logarithm of the ratio at one hinge is strictly positive, while at the other it is strictly negative. This is a formal, machine-checked theorem, meaning the result is derived from the framework's axioms and prior theorems without any unproven assumptions.

The example itself is a small system with two hinges (labeled 0 and 1), a channel count of four, a mesh scale of 1/8, and signed geometric deficits of +1/16 and -1/16. The framework models this as a recognition bridge, a structure that links a discrete record of events to a derived ratio. The theorem concreteStationarityBridge_logRatio_signed states that the log of the ratio at hinge 0 is greater than zero, and the log of the ratio at hinge 1 is less than zero. This confirms that the bridge can represent both expansion and contraction, not just a trivial uniform state.

The significance is that this example is not a degenerate or empty case. It demonstrates that the general constructor, which builds a bridge from stationarity conditions, can produce a meaningful instance with signed behavior. The proof of this signed behavior is a theorem in the framework's machine-checked library, and it relies on the explicit constitutive action and J-stationarity, not on the ratio relation being assumed as a hypothesis. This is a key step in showing the bridge construction is real and not merely a formal possibility.

/-- **THEOREM (T4, signed log ratios).** The concrete instance's log
ratios carry the deficit signs: log x_0 > 0 (source +1/16) and
log x_1 < 0 (source -1/16). The derived bridge genuinely stores signed
information in log x, which the ledger-deficit observables cannot carry
(`ratioBridge_separates_deficit_observables`); at concrete numbers this
non-vacuity is fully discharged. -/
theorem concreteStationarityBridge_logRatio_signed :
    0 < Real.log (concreteStationarityBridge.xRatio 0) ∧
      Real.log (concreteStationarityBridge.xRatio 1) < 0 := by
  constructor
  · refine ofStationarity_log_xRatio_pos 4 (by norm_num) (fun _ => 1)
      (fun σ => if σ = 0 then (1 : ℝ) / 16 else -(1 / 16)) (1 / 8)
      (by norm_num) concreteBridge_hdom 0 ?_
    show (0 : ℝ) < 1 * (if (0 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16))
    rw [if_pos rfl]
    norm_num
  · refine ofStationarity_log_xRatio_neg 4 (by norm_num) (fun _ => 1)
      (fun σ => if σ = 0 then (1 : ℝ) / 16 else -(1 / 16)) (1 / 8)
      (by norm_num) concreteBridge_hdom 1 ?_
    show (1 : ℝ) * (if (1 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16)) < 0
    have h10 : ¬((1 : Fin 2) = 0) := by decide
    rw [if_neg h10]
    norm_num

/-- **THEOREM (T4 non-vacuity record).** The concrete instance has: the
prescribed signed deficits (+1/16 at hinge 0, -1/16 at hinge 1), a
STRICTLY NEGATIVE deficit at hinge 1 (the signed-deficit non-vacuity of
`ratioBridge_admits_negative_deficit`), mesh 1/8, unit coupling, and the
derived remainder constant remBound = 4/6 = 2/3 inherited from the cubic
error lemma. (Uses `decide` only for the Fin 2 literal disequality
1 ≠ 0, as in `RecognitionRatioBridge`.) -/
theorem concreteStationarityBridge_nonvacuous :
    concreteStationarityBridge.geometricDeficit 0 = 1 / 16 ∧
    concreteStationarityBridge.geometricDeficit 1 = -(1 / 16) ∧
    concreteStationarityBridge.geometricDeficit 1 < 0 ∧
    concreteStationarityBridge.meshScale = 1 / 8 ∧
    concreteStationarityBridge.remBound = 2 / 3 ∧
    (∀ σ, concreteStationarityBridge.kappa σ = 1) := by
  have h0 : concreteStationarityBridge.geometricDeficit 0 = 1 / 16 := by
    show (if (0 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16)) = 1 / 16
    rw [if_pos rfl]
  have h1 : concreteStationarityBridge.geometricDeficit 1 = -(1 / 16) := by
    show (if (1 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16)) = -(1 / 16)
    have h10 : ¬((1 : Fin 2) = 0) := by decide
    rw [if_neg h10]
  refine ⟨h0, h1, ?_, rfl, ?_, fun _ => rfl⟩
  · rw [h1]
    norm_num
  · show ((4 : ℕ) : ℝ) / 6 = 2 / 3
    norm_num

What this page does not claim

This theorem does not claim that the bridge is derived from the bare RecognitionLedger alone. It does not claim that the specific numeric values (like 1/16 or 1/8) are derived from first principles rather than chosen for the example. It does not claim that this example represents a physically realized system.

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