pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.CrossDomain.OncologyLattice

show as:
view Lean formalization →

The OncologyLattice module supplies finite set structures for HallmarkCluster, TreatmentModality, and OncogeneFamily to model oncology multiplicatively inside the Recognition Science cross-domain layer. Researchers extending the J-cost and phi-ladder formalism to biology would cite these definitions when comparing product versus sum scalings. The module consists solely of type definitions, cardinality functions, and surjectivity statements with no proofs.

claimThe module defines finite sets $H$ (HallmarkCluster), $M$ (TreatmentModality), $O$ (OncogeneFamily) together with cardinality maps and the relation $|H| |M| |O| > |H| + |M| + |O|$.

background

The module sits in the cross-domain extension of Recognition Science, where the Recognition Composition Law governs multiplicative rather than additive combination of structures. It introduces HallmarkCluster as the finite collection of core cancer properties, TreatmentModality as the set of intervention classes, and OncogeneFamily as the set of driver gene families. Cardinality functions and surjectivity maps are defined using Mathlib primitives; the supplied module comment stresses the inequality 125 > 15 for three factors of five.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the basic objects required for any cross-domain oncology application of the Recognition framework. It demonstrates how the multiplicative composition from the RCL can be instantiated outside physics, feeding the general claim that the same J-uniqueness and phi fixed-point structure governs both physical and biological lattices. No downstream theorem is listed, but the definitions close the gap between the eight-tick octave and concrete biological counting.

scope and limits

declarations in this module (14)