Physics Without Choice

The derivation of physical structure from one distinction needs no axiom of choice, and every step that asks for more than construction is located and priced exactly. We audit one derivation of physical structure, the recognition derivation, statement by statement in intuitionistic logic, in a dependent type theory with quotient types and no choice of any kind. The list has 130 rows: 128 statements of the derivation, from the arithmetic of records through the cost of comparison J(x) = ½(x + 1/x) − 1, the golden ratio, three dimensions and the eight-tick cycle to identities among constants in native units, and two forms added to locate prices. The physics sits in four named premises, which this paper neither derives nor tests. Read literally, 118 of the 128 statements are free. Seven are each equivalent to one principle: two to Markov's principle, one to the strong extensionality of integer-valued maps on the line, and four decide an exact tie between real quantities, at LLPO, LPO, WLPO and the function form of WLPO. Three more are bounded and not free. Read by Bishop's rule, 125 are free. Sheaf models show that no priced statement is free. For laws read as schemas over states, testing a law at a stated tolerance is free, and only deciding it exactly costs omniscience. Version 1.1 removes the comparison of the derivation's constant formulas with measured values, which lies outside the paper's subject; the audit and its prices are unchanged.