NeutronStarCert
plain-language theorem explainer
NeutronStarCert packages a structure asserting exactly five neutron-star crustal regimes whose densities form a geometric sequence with common ratio phi and remain strictly positive. Recognition Science researchers connecting the phi-ladder to astrophysical layering or modelers of neutron-star interiors would cite the structure. It is a direct structure definition that records the three properties without invoking lemmas or tactics.
Claim. Let NSRegime be the inductive type with five constructors (outer crust, inner crust, nuclear pasta, outer core, inner core). Let density(k) := phi^k for natural k. NeutronStarCert is the structure whose fields assert that the cardinality of NSRegime equals 5, that density(k+1)/density(k) = phi for every k, and that density(k) > 0 for every k.
background
The module treats neutron-star crusts as five canonical regimes matching configDim D = 5: outer crust, inner crust, nuclear pasta, outer core, inner core. NSRegime is the inductive type enumerating these cases and deriving Fintype, DecidableEq, and Repr. The sibling definition density(k) := phi^k places successive regimes on the phi-ladder so that adjacent densities differ by the golden ratio. Upstream, phi_ratio supplies the inverse 1/phi as a convex energy proxy minimized at that value, while Constants supplies phi itself.
proof idea
The declaration is a structure definition that directly encodes the three certification properties: Fintype.card NSRegime = 5, the ratio of consecutive densities equals phi, and positivity of all densities. No lemmas are applied and no tactics are used; the structure simply serves as a typed container for later instantiation.
why it matters
The structure is instantiated by the downstream definition neutronStarCert, which supplies the concrete witnesses nsRegime_count, density_ratio, and density_pos. It records the Recognition Science assertion that neutron-star layering exhibits five regimes on the phi-ladder with density ratio phi, consistent with the self-similar fixed point forced at T6. The module states zero sorry or axiom, thereby closing a formal gap for phi-ladder applications in astrophysics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.