IndisputableMonolith.Mathematics.ProjectionMultiplicityMethod
Defines the projection-multiplicity method for classical extremal problems: visible objects, a counted relation, size and event readouts, then lift data, finite windows, and certificates that beat linear bounds by a polynomial factor. Combinatorialists and RS analysts cite it when converting multiplicity lower bounds into polynomial gains. The module is mostly structure and certificate definitions plus one gain theorem.
claimA classical extremal problem is a tuple of a ground set of visible objects, a relation $R$ whose instances are events, a visible-size functional, and an event-count functional. Lift data, finite windows, and projection-multiplicity certificates supply a candidate that beats any linear bound by a polynomial gain factor.
background
The module sits in the Mathematics layer of the monolith and packages a classical extremal setup before any Recognition-specific forcing. A classical extremal problem, per the module doc, consists of visible objects, a relation whose instances are counted, and two numerical readouts: visible size and event count.
Around that core it introduces lift data (how a configuration is pulled back or projected), finite windows (local supports on which multiplicity is measured), and the comparison predicate that a construction beats a linear bound by a stated factor. Projection-multiplicity candidates and certificates are the certificate objects that turn a multiplicity lower bound into a quantitative gain.
Only Mathlib is imported; the development is self-contained combinatorial bookkeeping rather than an appeal to the T0–T8 forcing chain.
proof idea
This is primarily a definition module. It declares the classical extremal problem structure, lift data, finite windows, the beats-linear-by relation, projection-multiplicity candidates, and certificates. The one substantive theorem is that a valid projection-multiplicity certificate yields a polynomial gain over the linear bound; the argument is by unpacking the certificate fields and applying the recorded multiplicity and window hypotheses, not by a long tactic script.
why it matters in Recognition Science
The module supplies the combinatorial substrate for any later RS argument that needs a polynomial improvement over a linear extremal bound via projection multiplicities. Downstream consumers (not yet wired in the graph) would be gain lemmas and existence theorems that instantiate ProjectionMultiplicityCertificate and invoke certificate_gives_polynomial_gain. It does not itself touch J-uniqueness, phi, the eight-tick octave, or D = 3; it is reusable pure mathematics that those layers can call when an extremal counting step appears.
scope and limits
- Does not prove existence of a projection-multiplicity certificate for any concrete problem.
- Does not connect to J-cost, RCL, phi-ladder, or the T0–T8 forcing chain.
- Does not claim optimality of the polynomial gain exponent.
- Does not treat infinite or continuous extremal settings beyond finite windows.