Encyclopedia Gravity Gravity Seven Gaps Stationarity Bridge Closure Of Stationarity Minimizer Groundi

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Stationarity Bridge Closure Of Stationarity Minimizer Groundi

A machine-checked theorem shows that the ratio between two linked structures is forced by a minimization principle, not by assumption.

Verify this page

What the minimizer grounding proves

The declaration ofStationarity_minimizer_grounding is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes that a certain quantity, called the sourced action, has a unique global minimizer. The theorem states that for any input configuration, the value of the sourced action at this minimizer is less than or equal to its value at any other configuration, and if another configuration achieves the same value, it must be identical to the minimizer. In plain terms, the framework proves that among all possible arrangements, exactly one minimizes the cost, and that arrangement is the one the framework uses.

This uniqueness result is the load-bearing step in a larger construction. The framework defines a bridge structure that connects two linked entities, and it sets the ratio between them as the exponential of the total strain of this unique minimizer. The theorem ofStationarity_minimizer_grounding is what guarantees that this ratio is well-defined: because the minimizer is unique, the ratio is a single, unambiguous number rather than a choice among many. The framework's library then proves that this ratio satisfies a cubic error bound, meaning the derived ratio is close to a simple linear relation up to a term that shrinks as the mesh scale goes to zero.

What the theorem does not claim is just as important. It does not claim that the ratio relation follows from the bare Recognition Ledger alone. The framework explicitly records that the route from the bare ledger is dead and circular; the derivation requires an additional constitutive premise, the deficit-source coupling, which is a MODEL, not a theorem. The declaration ofStationarity_minimizer_grounding assumes this coupling as given and proves the uniqueness of the minimizer under it. The framework's own status flags state this plainly: the bridge is closed, but the derivation from the bare ledger remains permanently false.

The theorem also does not claim that the minimizer exists for every conceivable input. It requires a structural bound: the product of the coupling strength and the deficit must be dominated by the mesh scale at every hinge. Without this bound, the uniqueness proof does not go through. The framework provides a concrete example at four channels with a mesh of one-eighth and signed deficits, showing that the conditions are satisfiable and the result is not vacuous.

THEOREM ofStationarity_minimizer_grounding · IndisputableMonolith/Gravity/SevenGaps/StationarityBridgeClosure.lean
ofStationarity_minimizer_grounding · IndisputableMonolith/Gravity/SevenGaps/StationarityBridgeClosure.lean:260 
/-- **THEOREM (stationarity grounding, re-export of
`sourced_unique_minimizer` for the constructed bridge).** The
configuration whose total strain the constructed bridge exponentiates is
the GLOBAL minimizer of the sourced action at each hinge, and it is the
UNIQUE minimizer. So the bridge's ratio field is pinned by J-stationarity
of the constitutive action: no other configuration could have produced
it. -/
theorem ofStationarity_minimizer_grounding {H : Type*}
    (n : ℕ) (kappa geomDeficit : H → ℝ) (σ : H) (t : Fin n → ℝ) :
    sourcedAction n (kappa σ * geomDeficit σ)
        (sourcedMinimizer n (kappa σ * geomDeficit σ))
      ≤ sourcedAction n (kappa σ * geomDeficit σ) t ∧
      (sourcedAction n (kappa σ * geomDeficit σ) t
          = sourcedAction n (kappa σ * geomDeficit σ)
              (sourcedMinimizer n (kappa σ * geomDeficit σ)) →
        t = sourcedMinimizer n (kappa σ * geomDeficit σ)) :=
  sourced_unique_minimizer n (kappa σ * geomDeficit σ) t
THEOREM ofStationarity_minimizer_grounding · IndisputableMonolith/Gravity/SevenGaps/StationarityBridgeClosure.lean
ofStationarity_minimizer_grounding · IndisputableMonolith/Gravity/SevenGaps/StationarityBridgeClosure.lean:260 
/-- **THEOREM (stationarity grounding, re-export of
`sourced_unique_minimizer` for the constructed bridge).** The
configuration whose total strain the constructed bridge exponentiates is
the GLOBAL minimizer of the sourced action at each hinge, and it is the
UNIQUE minimizer. So the bridge's ratio field is pinned by J-stationarity
of the constitutive action: no other configuration could have produced
it. -/
theorem ofStationarity_minimizer_grounding {H : Type*}
    (n : ℕ) (kappa geomDeficit : H → ℝ) (σ : H) (t : Fin n → ℝ) :
    sourcedAction n (kappa σ * geomDeficit σ)
        (sourcedMinimizer n (kappa σ * geomDeficit σ))
      ≤ sourcedAction n (kappa σ * geomDeficit σ) t ∧
      (sourcedAction n (kappa σ * geomDeficit σ) t
          = sourcedAction n (kappa σ * geomDeficit σ)
              (sourcedMinimizer n (kappa σ * geomDeficit σ)) →
        t = sourcedMinimizer n (kappa σ * geomDeficit σ)) :=
  sourced_unique_minimizer n (kappa σ * geomDeficit σ) t
THEOREM stationarityBridgeClosureStatus_flags · IndisputableMonolith/Gravity/SevenGaps/StationarityBridgeClosure.lean
stationarityBridgeClosureStatus_flags · IndisputableMonolith/Gravity/SevenGaps/StationarityBridgeClosure.lean:579 
/-- Status flags record (rfl-forced; documentation, not new
mathematics). -/
theorem stationarityBridgeClosureStatus_flags :
    stationarityBridgeClosureStatus.constitutive_stationarity_bridge_closed
        = true ∧
      stationarityBridgeClosureStatus.derivation_from_bare_ledger = false :=
  ⟨rfl, rfl⟩
THEOREM recognitionRatioBridge_ofStationarity · IndisputableMonolith/Gravity/SevenGaps/StationarityBridgeClosure.lean
recognitionRatioBridge_ofStationarity · IndisputableMonolith/Gravity/SevenGaps/StationarityBridgeClosure.lean:176 
/-- **THEOREM-tier constructor (T3, the headline).** Builds a
`RecognitionRatioBridge` from the constitutive deficit-source action data,
PROVING the `ratio_relation` field from J-stationarity.

Hypothesis audit (every hypothesis is structural; NONE is the ratio
relation or equivalent to it):
* `hn : 1 ≤ n` — at least one recognition channel (positivity side
  condition of `sourced_ratio_cubic_error`).
* `hh : 0 < h` — positive mesh scale (the structure's own
  `meshScale_pos` field).
* `hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ n * h` — source domination: the
  total source strength at each hinge is bounded by the mesh budget n*h.
  This bounds the INPUT data (coupling times deficit); it says nothing
  about xRatio, log xRatio, or the remainder, so it cannot smuggle the
  conclusion.

Fields produced BY DERIVATION:
* `xRatio σ := exp(n * arsinh(kappa σ * geomDeficit σ / n))` — DEFINED as
  the exponential of the total strain of the unique global minimizer of
  the sourced action `sourcedAction n (kappa σ * geomDeficit σ)`
  (`sourcedMinimizer`; uniqueness and global minimality are
  `sourced_unique_minimizer`, re-exported for this bridge as
  `ofStationarity_minimizer_grounding`).
* `remBound := n / 6` — the explicit constant inherited from the 1/6 of
  `sourced_ratio_cubic_error`.
* `ratio_relation` — PROVED, by `stationaryRatio_cubic`; not passed in.

MODEL disclosure: the sourced action's coupling term is the explicit
deficit-source constitutive choice of `HingeStationarityCore`. Every
bridge this constructor produces is derived from an explicit
deficit-source constitutive action plus J-stationarity, never from the
bare RecognitionLedger. -/
noncomputable def recognitionRatioBridge_ofStationarity {H : Type*}
    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) :
    RecognitionRatioBridge H where
  xRatio := fun σ =>
    Real.exp ((n : ℝ) * Real.arsinh (kappa σ * geomDeficit σ / n))
  xRatio_pos := fun _ => Real.exp_pos _
  kappa := kappa
  geometricDeficit := geomDeficit
  meshScale := h
  meshScale_pos := hh
  remBound := (n : ℝ) / 6
  remBound_nonneg := by positivity
  ratio_relation := fun σ =>
    stationaryRatio_cubic n hn (kappa σ * geomDeficit σ) h (hdom σ)

What this page does not claim

The theorem does not prove that the ratio relation follows from the bare Recognition Ledger alone. The theorem does not establish the existence of a minimizer without the structural domination bound. The theorem does not assign a physical meaning to the deficit-source coupling.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND