The initial controller class in Definition [ftip-00MJ] is part of the endowment. It is not enlarged after an assisted discovery by inserting a program tailored to that discovery. A concrete specification can supply a finite collection of initial controllers, or an executable procedure that generates further controllers. In the latter case, generation, execution, comparison and selection occur within the campaign and consume its budget. The generator's fixed code and constants are themselves initial resources.

For example, let a campaign generate a program \(A_Z\) using a random variable \(Z\), and let its later interaction depend on the observed results. Its score averages over that declared generation and subsequent execution. Showing that one realization \(A_z\) constructs a useful representation cheaply does not show that the campaign finds that realization cheaply. Replacing the campaign by this selected program changes the initial endowment unless a legal route to its availability has been supplied.

This distinction does not forbid an ingenious algorithm. A procedure already admitted from the public task-family description is a legitimate closed alternative even if nobody has tested it. A lower bound must cover it. Conversely, a proof quantifying over all programs with arbitrary family-specific constants grants more advice than a fixed model lineage possesses. Uniformity across input sizes does not alone remove that advice: a single finite program can already contain the decisive family-wide idea. The theorem must state which controller access it grants.

An existential mathematical upper bound may describe a particular admitted program without proving that a person will discover its proof. The operational claim that a fixed lineage can acquire that program is stronger. It requires an available initial program or a charged causal construction from its accessible state. Keeping these claims distinct prevents both free advance knowledge and the exclusion of legitimate internal discoveries.

Fix a difficulty \(n\) and task-family parameter, the truth contract, fresh evaluation law and deployment cap of Definition [ftip-00MM]. For an allowed frozen artifact \(f\), including the failure artifact \(\bot \), let \(q_n(f)\) be its expected fresh-task score under that evaluation. The expectation includes fresh tasks and deployment randomness; set \(q_n(\bot )=0\). Evaluation begins with exactly the retained state permitted by the specification. Define

If the comparison randomizes a shared family parameter, apply this definition conditionally on that parameter and then average the resulting scores. This class is defined for mathematical analysis; membership need not be decidable or cheaply recognizable during research. It includes any artifact with the required performance: explicit lemmas, learned libraries, new architectures, implicit weights, and methods that avoid the contributor's representation entirely, whenever those artifacts are allowed.

For a random final artifact \(F_P\), the acquisition score is \(Q_{\mathrm {acq}}(P)=\mathbb E[q_n(F_P)]\). The desired lower bound must control this expectation for every admitted closed campaign. It cannot merely show that one named representation is unlikely to appear. Nor is a bound on reaching \(\mathcal U_{n,\tau }\) automatically a bound below \(\tau \): many outcomes just below the threshold can still have high mean score. A proposed proof must connect its event or structural quantity to the complete score distribution, as the explicit hypotheses of proposition [ftip-00MP] illustrate.

The contributor need not transmit an entire solution. A question, analogy or example may change which experiments the recipient attempts. The resulting interpretation, validation and learning remain charged. Acquisition is established only by the frozen recipient's performance on fresh instances; an insightful exchange by itself establishes neither that performance nor a lower bound on unaided discovery.

The proof direction is to begin with a concrete developmental asymmetry: some task-relevant experience available to a contributor is absent from the lineage's initial data and observed traces. From a specified family and computational model, derive that acquiring any equally useful capability exceeds the closed budget. The absence of that experience is a premise. The absence of every affordable substitute is the desired conclusion, and must not be included as another premise.

Three arguments are needed. A bounded developmental process must produce reusable structure with a stated probability before fresh target instances are revealed. A charged interaction and learning procedure must turn that structure into recipient capability. A lower-bound argument must cover all closed histories admitted by the initial endowment and execution semantics, including adaptive tools, simulations, generated programs, training, changed architectures and alternative representations. The first two arguments describe a constructive assisted procedure; the third establishes why the closed lineage cannot match it at the chosen resources.

A necessary-event estimate becomes useful only after the family and operations justify both its necessity and its probability bound. Assuming that every successful route requires a rare conceptual event simply moves the central difficulty into an assumption. Likewise, absence from a corpus does not imply computational inaccessibility: affordable experiments or derivations may supply a substitute. A proof must explain what the particular environment makes accessible and why the admitted closed operations cannot obtain an equally useful substitute within budget.

Both inequalities in § [ftip-00MN] remain open for the intended conceptual-discovery mechanism. The conditional transfer estimate in proposition [ftip-00MW] and simulation proposition in proposition [ftip-00MX] do not prove them. The research objective is a positive separation proof, beginning with a sufficiently concrete account of development, access and cost. Any restriction used to make the mathematics tractable must be visible in the claim; a result for a narrow action class does not establish a ceiling for all model lineages.