Physics Anchor Policy Model Stationary At Any

A definitional stand-in

The declaration stationary_at_any is a theorem in a machine-checked library of formal theorems. It states that a particular function, called the model residue, has a derivative of zero at every scale. In plain terms, the function does not change as the energy scale changes. The theorem is proved for any fermion and any scale point, and the proof is a direct simplification: the model residue ignores its scale argument entirely, so the function is constant by definition.

The model residue is a stand-in. The library's authors treat the Standard-Model renormalization-group residue as an opaque interface, because the repository does not implement the full multi-loop kernels, threshold policy, and numerical integration inside the formal system. Instead, this file defines a computable model where the residue is, by definition, equal to a display function called gap(Z). The theorem stationary_at_any is a consequence of that definitional choice, not a proof about the physical Standard Model.

What the theorem does establish is a clean algebraic fact: in this model, the residue is stationary at every point, and the second derivative is also identically zero, hence bounded. A companion theorem shows that if two fermions have the same Z value, their model residues are equal at every scale. These results make downstream algebraic consequences executable and avoid axiom dependencies when working in the model. They are useful for testing the machinery, not for claiming physical predictions.

In Recognition Science, this declaration sits in a specific role. It is a definitional model, not a derivation. The framework's own documentation says plainly: this is not a proof of the Standard-Model renormalization-group statement. The residue is constant in scale because the model sets it to be constant, not because physics forces it to be. The honest summary is that the theorem proves a property of a chosen definition, and the physical content remains an open target.

/-- In the model, the residue is constant in `t`, hence stationary at every point. -/
theorem stationary_at_any (muStar : ℝ) (f : Fermion) :
    deriv (fun t => f_residue_model f (Real.exp t)) (Real.log muStar) = 0 := by
  -- `f_residue_model` ignores its scale argument, so the function of `t` is constant.
  simp [f_residue_model]

@[simp] theorem f_residue_model_at (f : Fermion) (mu : ℝ) :
    f_residue_model f mu = gap (ZOf f) := rfl

/-- 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 theorem does not claim any physical stationarity for the real Standard-Model residue. The model does not derive the residue's value from first principles. The theorem does not establish that the second derivative is bounded in any physical sense.

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: