supplyChainTierCount
plain-language theorem explainer
The declaration fixes the number of supply chain tiers in the Recognition Science model at five. Researchers deriving economic structures from the J-cost functional equation would reference this result to anchor the dimensionality of their supply chain graphs. The proof proceeds by a single decision procedure that counts the constructors of the inductive definition of the tier type.
Claim. The finite set of canonical supply chain tiers has cardinality five: $|S| = 5$, where $S$ consists of the five stages raw materials, components, assembly, distribution, and retail.
background
In the Supply Chain from RS module the supply chain is modeled with five canonical tiers corresponding to raw materials, components, assembly, distribution, and retail. This count is identified with the configuration dimension D set to 5. Supply chain disruption is identified with positive J-cost while the optimal chain satisfies J equal to zero; the bullwhip effect appears through phi-ladder scaling of variance.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality of the Fintype cardinality to 5. The tactic succeeds directly from the derived Fintype instance on the inductive type whose five constructors are enumerated by the decision procedure.
why it matters
This result supplies the five_tiers field inside the supplyChainCert definition that certifies the optimal supply chain configuration. It implements the module statement that five tiers equal configDim D = 5 and thereby connects the economic model to the J-uniqueness and phi-ladder structures of the Recognition Science framework, with the optimal chain located at J = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.