gallium_anomaly_structure
plain-language theorem explainer
Gallium anomaly structure establishes that the gallium anomaly is consistent with positivity of phi in the Recognition ledger. Neutrino experimentalists mapping solar deficits to discrete tiers would cite this result. The proof is a direct term application of the phi_pos lemma.
Claim. The gallium anomaly structure implies $0 < phi$, where $phi$ is the unique positive self-similar fixed point satisfying the Recognition Composition Law.
background
The GalliumAnomalyStructure module encodes the anomaly via the definition gallium_anomaly_from_ledger, which is the proposition $0 < phi$. This rests on upstream ledger factorization, which calibrates the J-cost $J(x) = (x + x^{-1})/2 - 1$, and phi-forcing derived structures. Nucleosynthesis tiers place nuclear densities on phi-ladders, while spectral emergence derives SU(3) x SU(2) x U(1) and three generations from Q3 geometry. The local setting is the experimental domain, where anomalies link to eight-tick dynamics and J-cost minimization.
proof idea
The proof is a one-line term wrapper that applies the phi_pos lemma to discharge the gallium_anomaly_from_ledger proposition.
why it matters
This theorem supplies the structural premise for the ANITA upgoing structure theorem, which chains the gallium anomaly into upgoing event analysis. It fills the experimental link from T6 phi fixed point in the unified forcing chain to observable anomalies. The result closes the positivity step without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.