frustration_gravity_only
plain-language theorem explainer
Frustration regions with positive Betti-1 homology couple exclusively through the J-cost gradient. Cosmologists treating dark matter as delocalized topological frustration cite the result to exclude electromagnetic and strong channels at galactic scales. The proof is a direct term construction that assembles the three fields of GravityOnlyCoupling from the trivial propositions and the supplied betti1_pos hypothesis.
Claim. Let $R$ be a frustration region with positive Betti number $0 < R.betti1$. Then $R$ satisfies gravity-only coupling: it has no electromagnetic interaction, no strong interaction, and interacts gravitationally via its positive Betti number.
background
In the Recognition Science spatial projection of the phantom sector, dark matter is modeled as nonzero Betti-1 homology on the parity bundle of the ℤ³ carrier. A FrustrationRegion consists of a positive galactic radius together with a positive integer Betti number β₁. GravityOnlyCoupling is the structural proposition that such a region interacts solely through the J-cost gradient (gravity), with the electromagnetic and strong channels fixed to the trivial proposition True.
proof idea
The proof is a term-mode construction of the GravityOnlyCoupling structure. It supplies the no_em and no_strong fields by the trivial proposition and the gravity field by the betti1_pos hypothesis carried inside the input region R.
why it matters
The theorem supplies the gravity_only field required by the downstream DarkMatterTopologyCert certificate. It thereby closes one link in the module-level claim that dark matter is diffuse phase-saturation rather than a new particle on the φ-ladder. The module falsifier remains detection of a discrete DM particle at an unassigned φ-rung; the present result is consistent because it rules out non-gravitational channels without introducing new mass scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.