Physics Anchor Policy Model Stability Bound At Any

A stability bound in the model

In physics, a coupling constant (a number that sets the strength of an interaction) often changes with the energy scale at which you measure it. The question of whether such a running value stays bounded, or blows up, matters for whether a theory remains well-behaved. The declaration stability_bound_at_any in the Recognition Science framework's machine-checked library of formal theorems addresses this question, but only inside a deliberately simplified stand-in model, not for the full Standard Model.

The framework models a physical system using a ledger (a discrete record of recognition events, where recognition is the framework's term for a cost-forced measurement). The relevant residue, a leftover correction term from renormalization-group running, is represented by a function f_residue_model. By definition, this model residue ignores the scale argument entirely and simply equals a fixed gap value. Because the residue is constant in scale, its first derivative is zero at every point, and its second derivative is also identically zero. The theorem then states that for any chosen scale, there exists a positive bound such that the absolute value of this second derivative stays below it. Since zero is less than any positive number, the bound holds trivially.

The theorem is a formal consequence of the model's definition, not an empirical discovery. It establishes that, in this simplified setting, the residue is stationary and stable at every energy scale: it never curves sharply, so it never threatens to destabilize the anchor point where the model's value is fixed. This makes downstream algebraic consequences executable and easy to compute with, which is the model's purpose.

What the theorem does not claim is the real physics. The framework's own documentation is explicit: this is not a proof of the Standard Model renormalization-group statement. The actual residue is treated as an opaque interface, an axiom, because the repository does not yet implement multi-loop kernels, threshold policy, and numerical integration inside Lean. The model exists to make algebra work, not to settle whether the real residue stays bounded. The gap between the model and the physical theory remains an open target.

/-- In the model, the second derivative is also identically zero, hence bounded. -/
theorem stability_bound_at_any (muStar : ℝ) :
    ∃ (ε : ℝ), 0 < ε ∧ ∀ (f : Fermion),
      |deriv (deriv (fun t => f_residue_model f (Real.exp t))) (Real.log muStar)| < ε := by
  refine ⟨1, by norm_num, ?_⟩
  intro f
  -- Second derivative of a constant is 0.
  simp [f_residue_model]

/-- A computable stand-in for the RG residue: constant in scale and equal to the display `gap(Z)`.

This encodes the single-anchor closed form as a *definition* rather than a phenomenology axiom. -/
noncomputable def f_residue_model (f : Fermion) (_mu : ℝ) : ℝ :=
  gap (ZOf f)

What this page does not claim

This is not a proof about the actual Standard Model renormalization-group running. The model does not claim that the real residue is constant or stable. No claim is made that the bound is tight or physically meaningful.

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/Physics/AnchorPolicyModel.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: