A Core-Only Lean 4 Formalization of a Position-Invariant Account of Stakes, Readings, and Partiality

This paper describes a formalization in Lean 4, using only the core library, of the formal part of Connection Theology, an account of how a situated reader stands to the things that depend on other things. The development is parametric in a frame consisting of a type of things, a type of magnitudes with one distinguished element and no order or addition, a type of positions, and a map from positions to things. Nothing else is assumed. On this basis the file defines contexts and the unique context with no outside; stakes as a holder together with a magnitude, where the magnitude does not depend on any position; readings from a position, factored into an estimate (what a reader can see of a stake’s size: nothing, one size, or several) and a weighting (what the reader does with a size when acting); accounts and their filing; partiality as a closed hand, that is, a weighting that alters some size the reader’s own estimate admits for a stake in view; a floor below which a reading does not count as a vantage; love as a vantage whose hand is open on everything in view; the three predicates held, seen, and felt; exclusion; dependency and reach; and several derived notions. Sixty-six theorems are inventoried. The #print axioms command reports that sixty-four of them depend on no axioms and that two depend only on propext, Classical.choice, and Quot.sound: unique_no_outside, which concludes an equality of predicates from their agreement on every argument, and not_partial_loving, which takes one classical step and on which nothing else depends. No axiom specific to the subject matter is used; all content enters through definitions, which are given in full. We state what the formalization establishes, namely that the account is internally consistent with its own prose statement, and what it does not establish, namely whether its one substantive definition is true of the world. We also record the most recent revision, in which a counterexample supplied by a reader of a draft of this paper showed that the previous definition of partiality, as asymmetry across stakes of equal size, admitted a reader that excluded every stake of one size while favoring none; the definition was replaced and the earlier form is now a theorem. The declared idealizations are listed: no order on magnitudes, stakes taken as primitive, no type of actions, feeling represented as a Boolean, and no history in the self.