gallium_implies_phi_pos
plain-language theorem explainer
The gallium anomaly structure, when derived from the ledger, forces phi to be positive. Experimental modelers of solar neutrino deficits would cite this to anchor the base of the phi-ladder mass formula in Recognition Science units. The proof is a one-line term application that returns the hypothesis directly.
Claim. If the gallium anomaly arises from the ledger, then $0 < phi$.
background
In the Experimental.GalliumAnomalyStructure module the gallium anomaly is encoded as a ledger-derived proposition. The sibling definition gallium_anomaly_from_ledger is the Prop 0 < phi. This places the result inside the Recognition Science forcing chain where phi is the self-similar fixed point obtained after T5 J-uniqueness.
proof idea
Term-mode proof consisting of a single application of the hypothesis h, which is exactly the required positivity statement.
why it matters
The theorem supplies the positivity of phi required by the mass formula yardstick * phi^(rung - 8 + gap(Z)) and by the eight-tick octave. It feeds no downstream theorems in the current graph but closes the experimental-to-foundational link for the gallium anomaly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.