Which discovery procedures are initially available? [ftip-00N6]
Which discovery procedures are initially available? [ftip-00N6]
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.