Ecosystem
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.
claimAn 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 in Recognition Science
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.
scope and limits
- Does not compute total rung or apply the $Z_{life}$ threshold.
- Does not encode time evolution or continuous rung dynamics.
- Does not force the support relation to be symmetric or undirected.
- Does not embed the graph in physical space or higher dimensions.
formal statement (Lean)
85structure Ecosystem (n : ℕ) where
86 /-- Baseline rung of each species (intrinsic, before bond support). -/
87 baseline : Fin n → ℝ
88 /-- Support `i → j` from each species i to each species j. -/
89 support : Fin n → Fin n → ℝ
90 /-- All baselines positive. -/
91 baseline_pos : ∀ i : Fin n, 0 < baseline i
92 /-- All supports non-negative. -/
93 support_nonneg : ∀ i j : Fin n, 0 ≤ support i j
94
95/-- Total rung of species `j` under a "live" set `L` (only live
96species contribute support). -/