Ecosystem
plain-language theorem explainer
The Ecosystem structure packages a finite set of n species together with strictly positive baseline rungs and a non-negative support matrix that encodes recognition bonds. Ecologists working on Recognition Science extinction models cite it as the basic data type on which ledger-bankruptcy cascades are defined. It is introduced directly as a structure definition whose four fields enforce the required positivity and non-negativity conditions.
Claim. An ecosystem on $n$ species consists of a baseline function $b : [n] → ℝ_{>0}$ and a support function $s : [n] × [n] → ℝ_{≥0}$, where $b(i)$ is the intrinsic rung of species $i$ and $s(i,j)$ is the rung contribution from species $i$ to species $j$.
background
The module treats an ecosystem as a finite recognition graph in which each vertex carries a current rung drawn from the phi-ladder and each directed edge carries a non-negative support weight. Total rung of a live species is its baseline plus the sum of supports received from currently live neighbors. The life-ignition threshold is fixed at $Z_{life} = φ^{19}$ (imported via upstream constants). Upstream structures supply the rung calibration: NucleosynthesisTiers.of gives nuclear-density tiers on the phi-ladder, PhiForcingDerived.of encodes the J-cost functional, and PrimitiveDistinction.from supplies the seven-axiom origin of the four structural conditions used here.
proof idea
This is a structure definition. It directly assembles the baseline map, support matrix, and the two positivity axioms into a single type that downstream functions such as cascadeStep and cascadeIterate accept as input.
why it matters
Ecosystem is the input type for the entire cascade-closure development (cascadeIterate, cascadeStep, and their monotonicity lemmas). It supplies the concrete finite-graph setting required by the Q2 ledger-bankruptcy track, connecting the abstract J-cost and phi-forcing results from PhiForcingDerived and DAlembert.LedgerFactorization to the ecological extinction dynamics. The definition thereby closes the structural gap between the eight-tick octave and phi-ladder rung arithmetic on one side and monotone fixed-point iteration on the other.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.