Lean Block 04 — mathematical proof guide
Machine-Native Reasoning · Reviewed Core 0.2 · Cumulative formal companion 0.4.0
The source book is unchanged. New result-level coverage is Core 3.8 and 5.6, bringing the cumulative total to eleven of 27. The finite probability definitions reuse Instrument.mass, push, applyKernel, IsDist, normalize, and Law. The common policy is the inherited Instrument.Policy, whose input is a list of observed action/report pairs.
1. One convention for total variation
Variation.tv p q is literally
All later estimates use that convention. tv_push_le proves contraction when coordinates are aggregated. kernel_contraction proves contraction under a common normalized nonnegative kernel. Neither is assumed as an axiom or imported as an unproved external claim.
For heterogeneous fine and coarse spaces, push_kernel_step shows that a uniform error between the aggregated fine kernel columns and the coarse columns gives
The proof first aggregates the exact fine mixture, replaces its rows with the approximate rows, and then propagates the difference between initial aggregate and approximate beliefs through the common coarse kernel. The finite triangle inequality and column normalization supply every step. This avoids assuming the projected fine state is itself Markov.
2. A real full-history object
ApproximateHistory.Path X A O H stores the initial state and H chronological action/report/successor triples. law is an actual recursively constructed probability law: at each step it multiplies the previous history mass by the policy's action probability and the corresponding instrument entry. law_succ establishes the literal product formula, and law_dist proves normalization at every horizon.
observed removes all state coordinates before the policy is called. project keeps all state positions but applies the fine-to-coarse map to each. The identity project_observed makes the common-policy information boundary explicit.
The row discrepancy is over the joint report/next-coarse-state law, not a report marginal, state marginal, or isolated likelihood entry. stepRow_error mixes those bounds using the common action probabilities. pathKernel_error adds the same recorded prefix without increasing the error. Applying push_kernel_step inductively gives
The cap one is justified by the proved normalization of both actual path laws. Time-dependent instruments are permitted, but at each time the same observation-only policy is used on both sides. The row assumptions are stated for all represented actions and fine states, not estimated from sampled histories.
Main endpoints: whole_history_bound, observed_history_bound.
3. Why the conditioning denominator is a maximum
For two distributions P,Q and one common event E, let u,v be the restrictions and let p,q be their masses. Equal total mass implies that the difference on the complement of E has signed mass q-p. Its absolute sum is at least |p-q|. Therefore
Adding and subtracting v/p in u/p-v/q gives a normalization estimate with denominator p. Swapping P,Q gives the analogous estimate with denominator q. The stronger of the two uses max(p,q). condition_bound proves precisely
Both masses must be strictly positive. conditional_output_bound then projects to any requested output. The full-history theorem uses this lemma for the same event in the same constructed history laws, and projects to the final coarse state.
The event-probability inequality is also sharp:
Consequently, a mass strictly above d_H on either side forces both masses positive. Equality does not suffice. No theorem calls an algebraic normalization at zero a posterior.
Main endpoints: restricted_discrepancy, condition_bound, conditional_output_bound, conditional_final_bound, history_event_positive.
4. A changed policy needs a uniform fixed-policy premise
For each fixed policy i, use its own actual pair of path laws P_i,Q_i and the same loss function f_i on those paths. If 0 <= f_i <= B, expectation_bound proves
Assume this distance is at most d for every policy in one common finite catalogue. Let c minimize approximate risk and let b minimize true risk. Then
The range [0,B] also bounds regret by B. uniform_policy_regret obtains min(B,2Bd). The same proof compares the chosen policy to any catalogue member, so specializing to a true minimizer gives the source statement. minimizing_policies_exist uses the previously checked finite-minimum construction to establish that both minimizers really exist.
history_policy_error and history_selected_policy_regret instantiate this argument with the newly constructed complete fine/coarse history laws. They do not merely assume the final history bound as an unexplained input.
For a finite class of observation trees, the general theorem applies once their actual common bounded path losses and corresponding laws are supplied. Padding terminal choices into a common absorbing record is one admissible encoding, but its validity is not automatically established for arbitrary host programs by this block. The result neither constructs hidden action permissions nor certifies a hard budget.
Main endpoints: same_policy_error, uniform_policy_regret, minimizing_policies_exist, history_policy_error, history_selected_policy_regret.
5. Exact controls and calibrations
Rare-event amplification
The four-point laws rareP delta and rareQ delta share mass 1-delta on an ordinary outcome and put delta on different states inside the same rare-report event. Their total variation is delta, both event masses are delta, and conditional output distance is one. This is proved for every 0 < delta <= 1, rather than sampled at several small values.
unequal_mass_sharp uses event masses 1/10 and 1/5, whole-law distance 1/10, and conditional distance 1/2. Thus the stronger maximum-denominator bound can be attained. positive_threshold_is_strict shows why an event mass equal to the whole-law bound need not have a positive counterpart.
Exact regret factor
The true binary law has P(true)=3/4 and the approximate law is uniform. Under classification loss, both choices minimize approximate risk. Choosing false gives true risk 3/4, whereas choosing true gives true risk 1/4. The law distance is 1/4 and regret is 1/2=2*TV. checked_selected_regret applies the actual general theorem to this example. The sharpness uses permitted approximate ties; no favorable tie-breaking rule is assumed.
Misspecified sensor
calibrated37 gives the fine eight-world sensor a calibration accuracy 37/50. The coarse reference retains the inherited accuracy 3/4. For every world, the total variation of the joint report/coarse-successor row is exactly 1/100. sensor_all_history_error applies whole_history_bound for all priors, all report-history policies, and every finite H, obtaining min(1,H/100).
For three observations and complete loss bound 23/20, kernel-checked arithmetic gives a fixed-policy allowance 69/2000 and changed-policy allowance 69/1000. These are bounds derived from the model contract, not a measured regret or a proof that the old adaptive sensor tree remains optimal after its likelihood changes. The general finite-policy theorem is instantiated on the binary classification example above; the displayed sensor margins are exact coefficient specializations.
History is not the final state
Two different initial bits followed by the same reset have identical final-state laws but disjoint complete path laws. Both claims are proved. A method that compared only the final state would miss the initial history entirely.
6. What this completes, and what it does not
The exact filtering and planning results remain untouched. This block adds the quantitative relationship between their histories and supports selection under a uniform approximate-model error. Core 4.1, which combines a probability-record error with a separate response approximation and a Lipschitz loss, is not silently included: it requires its own response interface and proof.
The proof library uses finite types, exact real numbers, normalized laws, and explicit bounded losses. It does not identify a physical instrument from data, derive statistical confidence from the examples, justify neural generality, prove arbitrary host-program semantics, or reconstruct missing operational permissions. Same-kernel replay and complete transitive axiom audits are recorded separately from the mathematical assumptions.