pith. machine review for the scientific record. sign in
def definition def or abbrev moderate

Z_break6Q

show as:
view Lean formalization →

This definition supplies a modified integer mass label for each particle species by substituting a broken charge integerization into the standard quark Z formula. Researchers examining the stability of the Recognition Science anchor relation under perturbations to charge quantization would cite it when building contradiction arguments for the certified anchor. The definition is a direct one-line expression that mirrors the structure of the baseline Z map but replaces the charge term with the broken variant.

claimFor a species $i$, the broken Z-value is defined by $Z(i) := 4 + q(i)^2 + q(i)^4$, where $q$ is the broken integerization of the charge parameter.

background

In the Ablation module this definition supports tests of whether the anchor relation survives changes to integerization. The baseline Z map from the Anchor module computes an integer for up and down quarks by forming Q6 = 6Q from the rational charge and then evaluating 4 + Q6² + Q6⁴. Species is the inductive type classifying particles as fermions, W, Z or Higgs bosons. The broken variant replaces the standard charge integerization step with a perturbed version to probe uniqueness of the anchor.

proof idea

One-line definition that directly substitutes the broken charge parameter into the quadratic and quartic terms of the standard quark Z expression.

why it matters in Recognition Science

It is invoked inside ablation_contradictions to show that the anchor-equality predicate fails under this perturbation, thereby confirming that the certified anchor cannot be recovered from a broken integerization. This step tests the necessity of the precise charge quantization inside the mass formula on the phi-ladder. It touches the open question of how tightly the eight-tick octave and D=3 structure constrain the integer map.

scope and limits

formal statement (Lean)

  30noncomputable def Z_break6Q (i : Species) : Int :=

proof body

Definition body.

  31  4 + (tildeQ_broken3 i)^2 + (tildeQ_broken3 i)^4
  32
  33/-- Anchor-equality predicate for a candidate Z-map: residues must match the original. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.