FrustrationRegion
plain-language theorem explainer
FrustrationRegion packages a positive galactic radius in kpc with a positive first Betti number to represent a non-contractible loop in the parity bundle of the ℤ³ carrier. Cosmologists modeling dark matter as delocalized topological frustration rather than particles cite this structure when constructing the gravity-only coupling certificate. The declaration is a direct structure definition that supplies the input type for the downstream theorems on alpha_t bounds and J-cost gradients.
Claim. A FrustrationRegion is a pair consisting of a radius $r > 0$ (in kpc) together with a positive integer $b_1$ (the first Betti number) that counts non-contractible loops on the parity bundle.
background
Recognition Science treats dark matter as diffuse phase-saturation in the ℤ³ carrier that failed to condense into baryons. The module presents this as VIEW 2 of the phantom sector: the σ=0, Z≠0 projection at galactic scale, where nonzero accumulated Berry phase produces β₁ > 0. The structure therefore encodes the minimal data needed to assert that a region carries nontrivial first homology and therefore couples only through the J-cost gradient.
proof idea
The declaration is a structure definition that directly records the four fields radius_kpc, radius_pos, betti1 and betti1_pos. No lemmas are applied; the object is simply the carrier for the positivity hypotheses used by frustration_gravity_only and GravityOnlyCoupling.
why it matters
FrustrationRegion supplies the domain for DarkMatterTopologyCert and the theorem frustration_gravity_only, which together establish that any such region interacts only gravitationally. It realizes the module claim that dark matter equals nonzero Betti-1 homology at galactic scale and is tied to the phi-ladder via the ILG kernel α_t = ½(1 − φ⁻¹). The open falsifier remains detection of a discrete particle at a new phi-rung (distinct from the K-gate W-image at 1.79 GeV).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.