Physics Anchor Policy Model Equal Z At Any

The equal-Z rule

In particle physics, a coupling constant is a number that measures the strength of an interaction, and it changes with the energy scale at which you probe it. The Recognition Science framework has a machine-checked library of formal theorems that models this scale-dependence through a residue function, a stand-in for the complicated multi-loop corrections of the Standard Model. The declaration equalZ_at_any establishes a simple identity: if two fermions have the same anchor value, denoted Z, then their residue functions are equal at every scale. In plain terms, if two particles share the same anchor, they stay identical in their scale-dependent behavior throughout the entire energy range, not just at one special point.

The theorem is proved in the model by definition, not by physical argument. The residue function f_residue_model is defined to ignore its scale argument entirely and simply return the gap of the anchor value. Because it is constant in scale, the derivative and second derivative are zero at every point, which the library states as stationary_at_any and stability_bound_at_any. The equal-Z rule then follows immediately: if the anchors are equal, the constant values are equal, so the functions coincide everywhere. This is a formal consequence of the model's definition, not an empirical discovery or a derived law of nature.

The model exists because the repository does not currently implement multi-loop renormalization-group kernels, threshold policies, and numerical integration inside the proof assistant. The actual Standard-Model residue is treated as an opaque interface, an axiom, while this model provides a computable stand-in. The value of equalZ_at_any is that it makes downstream algebraic consequences executable and avoids axiom dependencies when working in this simplified setting. It is a definitional model, explicitly documented as not a proof of the Standard-Model renormalization-group statement.

In Recognition Science, the declaration supports the practical work of testing algebraic consequences of the anchor policy without waiting for full physics kernels to be formalized. It lets the framework explore the structure of equal-anchor degeneracy in a way that is checkable by computation. The honest scope is narrow: this is a formal identity inside a deliberately simplified model, useful for building the library's executable surface, not a claim about how real coupling constants behave.

/-- Equal-Z degeneracy holds by definition in the model. -/
theorem equalZ_at_any {f g : Fermion} (hZ : ZOf f = ZOf g) (mu : ℝ) :
    f_residue_model f mu = f_residue_model g mu := by
  simp [f_residue_model, hZ]

/-- 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]

/-- 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

Not a proof that real Standard-Model coupling constants are scale-independent. Not a derivation of the anchor value Z from first principles. Not a claim that two particles with equal Z are physically indistinguishable in all respects.

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: