Glen writes: <lol/>
The model captures the key ideas from the suggestion:
Subject
Cheapest Posture
Why
typicalPerson
playAlong (10)
Much cheaper than queryMechanism (80)
historian
correct (20)
Cheaper than stayQuiet (60)!
rolePlayer
playAlong (5)
"Authenticity" costs 200
historian at energy 15
none
Neither option affordable
The theorem more_energy_more_options proves that higher energy strictly expands
what's available.
Key features formalized:
* Energy is primary - selection is constrained by available energy first
* Cost profiles vary by subject - the historian finds correction cheaper
than silence
* Schema evolution requires surplus - canEvolveSchema checks for energy
beyond the current posture cost
* Mismatch tolerance scales - mismatchTolerable requires a buffer
proportional to the mismatch
-- Subjective energy and posture selection
-- Energy is primary, matching/impedance is secondary
structure AsIfPosture where
objectiveCategory : String
embodiedInstance : String
subjectiveVocabulary : String
treatedAsObjective : Bool
acknowledgesEmbodiment : Bool
acknowledgesDiscursive : Bool
selfAware : Bool
structure PostureCost where
postureName : String
cost : Nat
deriving Repr
structure Subject where
name : String
baseEnergy : Nat
postureCosts : List PostureCost
deriving Repr
-- Different subjects have different cost profiles
def typicalPerson : Subject := {
name := "typical",
baseEnergy := 100,
postureCosts := [
{ postureName := "playAlong", cost := 10 },
{ postureName := "queryMechanism", cost := 80 }
]
}
def historian : Subject := {
name := "historian",
baseEnergy := 100,
postureCosts := [
{ postureName := "correct", cost := 20 },
{ postureName := "stayQuiet", cost := 60 } -- harder to stay quiet!
]
}
def rolePlayer : Subject := {
name := "no-authentic-self",
baseEnergy := 100,
postureCosts := [
{ postureName := "playAlong", cost := 5 },
{ postureName := "beAuthentic", cost := 200 } -- "authenticity" expensive
]
}
-- Find minimum cost posture that's affordable
def cheapestAffordable (energy : Nat) (costs : List PostureCost) : Option
PostureCost :=
let affordable := costs.filter (λ pc => pc.cost ≤ energy)
affordable.foldl (λ acc pc =>
match acc with
| none => some pc
| some best => if pc.cost < best.cost then some pc else some best
) none
-- Schema evolution requires energy surplus
def canEvolveSchema (energy : Nat) (currentCost : Nat) (evolutionThreshold :
Nat) : Bool :=
energy > currentCost + evolutionThreshold
-- Mismatch tolerance depends on energy
def mismatchTolerable (energy : Nat) (mismatchCost : Nat) : Bool :=
energy > mismatchCost * 2
-- Theorem: higher energy means more options available
theorem more_energy_more_options (e1 e2 : Nat) (costs : List PostureCost)
(h : e1 < e2) :
(costs.filter (λ pc => pc.cost ≤ e1)).length ≤
(costs.filter (λ pc => pc.cost ≤ e2)).length := by
induction costs with
| nil => simp
| cons head tail ih =>
simp [List.filter]
split <;> split <;> simp_all
· omega
· omega
-- Examples:
-- #eval cheapestAffordable 100 typicalPerson.postureCosts
-- => playAlong (cost 10)
-- #eval cheapestAffordable 100 historian.postureCosts
-- => correct (cost 20), not stayQuiet (cost 60)
-- #eval cheapestAffordable 15 historian.postureCosts
-- => none (neither affordable)
-- #eval canEvolveSchema 100 10 50 => true (surplus)
-- #eval canEvolveSchema 100 80 50 => false (no surplus)
-----Original Message-----
From: Friam <[email protected]> On Behalf Of glen
Sent: Monday, November 24, 2025 10:56 AM
To: [email protected]
Subject: Re: [FRIAM] mental imagery
Yes. But it's more a matter of available energy than impedance matching.
Mismatches are tolerable when there's plenty of energy available, intolerable
otherwise. It's also scalable, composite. Matching in a crowd is different from
matching with an individual. Energy is primary, matching secondary.
I can easily imagine that for *some*, it takes more energy to entertain others'
"as if postures" than it does to well-place them in an arching structure. For
example, it may be *easier* for a historian to politely correct someone at a
dinner party than to simply stay quiet and allow a mistake to persist. Or for a
good faith steelmanner to ask critical path questions. That may be less
expensive to them than role-playing. (For those of us who can't do anything but
role-play, with no identifiable "authentic self", attempts at authenticity are
more expensive.)
The schema only evolve *if* I have enough energy to break them in little ways.
Otherwise, they're static shunts for avoiding benefit-less costs, like querying
a newly certified reiki masseuse about the mechanism of action. It's much much
cheaper to simply play their game. As I age, my energy wanes. 8^D
On 11/24/25 7:36 AM, Marcus Daniels wrote:
> I think in your own description of role-playing at parties, you've described
> "as if" as data collection, not a grand unified theory. The counterparty is
> described by an evolving schema that is just good enough to "pass"?
>
> -----Original Message-----
> From: Friam < <mailto:[email protected]> [email protected]>
> On Behalf Of glen
> Sent: Monday, November 24, 2025 6:41 AM
> To: <mailto:[email protected]> [email protected]
> Subject: Re: [FRIAM] mental imagery
>
> I don't understand how we can instantiate our ability to hold a
> counterfactual posture. The very existence of AsIfPosture argues it can
> obtain or not. We can turn it on and off, use it or not, without changing the
> discourse. That's what "as if" means. But I don't see it in the formalism.
>
> It's something like a complement to AsIfPosture, while retaining
> metaPosture. Or maybe the dependency is backwards, AsIfPosture should
> instead derive from metaPosture, because the only context in which you
> can even have AsIfPosture is when you can have a metaPosture. (Yes, I
> know. I'm lazy and *should* do the homework myself.)
>
> On 11/23/25 8:59 AM, Marcus Daniels wrote:
>> Migraine and dog examples, tested in a MCP server controlled by Claude.
>>
>> *Key aspects:*
>>
>> 1. *Universe-level encoding* - |Discourse.{u} : Type (u+1) := Type
>> u| allows self-reference through the type hierarchy without triggering
>> non-positivity errors 2. *The three layers* captured in |AsIfPosture|:
>>
>> * |treatsAsReal| - treating "migraine aura" as an objective category
>> * |acknowledgesEmbodiment| - Nick's particular, embodied instance
>> * |acknowledgesDiscursive| - the vocabulary comes from shared
>> discourse
>>
>> 3. *Self-awareness* - the |selfAware| field and |metaPosture| show
>> that the posture can reflect on itself 4. *All theorems verify* -
>> proving we can coherently adopt this stance
>>
>> This achieves the coinductive spirit (self-referential structures that can
>> contain references to themselves) in a way that Lean 4's type checker
>> accepts.
>>
>> -- Migraine aura example with self-reference via universe levels
>>
>> -- (Lean 4's way of encoding coinductive-style structures)
>>
>> -- A discourse at universe level u references discourses at level u
>>
>> def Discourse.{u} : Type (u+1) := Type u
>>
>> -- Properties of a discourse state
>>
>> structure DiscourseState (D : Type) where
>>
>> category : String
>>
>> body : String
>>
>> treatedAsObjective : Bool
>>
>> acknowledgesEmbodiment : Bool
>>
>> acknowledgesDiscursive : Bool
>>
>> property : D → Prop
>>
>> -- Nick's migraine aura as a discourse state
>>
>> def MigraineAuraType : Discourse := Unit
>>
>> def migraineState : DiscourseState MigraineAuraType := {
>>
>> category := "migraine aura",
>>
>> body := "Nick",
>>
>> treatedAsObjective := true,
>>
>> acknowledgesEmbodiment := true,
>>
>> acknowledgesDiscursive := true,
>>
>> property := λ _ => True
>>
>> }
>>
>> -- The "as if" posture structure
>>
>> structure AsIfPosture where
>>
>> objectiveCategory : String
>>
>> embodiedInstance : String
>>
>> subjectiveVocabulary : String
>>
>> treatsAsReal : Bool
>>
>> acknowledgesEmbodiment : Bool
>>
>> acknowledgesDiscursive : Bool
>>
>> selfAware : Bool
>>
>> -- The posture adopted when saying "Nick is experiencing his own migraine
>> aura"
>>
>> def migrainePosture : AsIfPosture := {
>>
>> objectiveCategory := "migraine aura",
>>
>> embodiedInstance := "Nick",
>>
>> subjectiveVocabulary := "aural sensation",
>>
>> treatsAsReal := true,
>>
>> acknowledgesEmbodiment := true,
>>
>> acknowledgesDiscursive := true,
>>
>> selfAware := true
>>
>> }
>>
>> -- What it means to adopt this posture
>>
>> def adoptsPosture (p : AsIfPosture) : Prop :=
>>
>> p.treatsAsReal = true ∧
>>
>> p.acknowledgesEmbodiment = true ∧
>>
>> p.acknowledgesDiscursive = true ∧
>>
>> p.selfAware = true
>>
>> -- Verify we can adopt the migraine posture
>>
>> theorem can_adopt_migraine_posture : adoptsPosture migrainePosture :=
>> by
>>
>> unfold adoptsPosture migrainePosture
>>
>> exact ⟨rfl, rfl, rfl, rfl⟩
>>
>> -- The self-referential twist: we can have a posture about postures
>>
>> def metaPosture : AsIfPosture := {
>>
>> objectiveCategory := "epistemic posture",
>>
>> embodiedInstance := "speaker",
>>
>> subjectiveVocabulary := "stance-taking",
>>
>> treatsAsReal := true,
>>
>> acknowledgesEmbodiment := true,
>>
>> acknowledgesDiscursive := true,
>>
>> selfAware := true
>>
>> }
>>
>> -- We can reflect on the posture itself
>>
>> theorem can_reflect_on_posture : adoptsPosture metaPosture := by
>>
>> unfold adoptsPosture metaPosture
>>
>> exact ⟨rfl, rfl, rfl, rfl⟩
>>
>> -- Key property: the posture acknowledges all three layers
>> simultaneously
>>
>> theorem posture_three_layers :
>>
>> migrainePosture.treatsAsReal = true ∧
>>
>> migrainePosture.acknowledgesEmbodiment = true ∧
>>
>> migrainePosture.acknowledgesDiscursive = true := by
>>
>> unfold migrainePosture
>>
>> exact ⟨rfl, rfl, rfl⟩
>>
>> #check can_adopt_migraine_posture
>>
>> #check can_reflect_on_posture
>>
>> #check posture_three_layers
>>
>>
>> Now the dog example…
>>
>> *Cross-species coordination* (|humanDogFairnessCoordination|) - Dogs
>> can have a sense of fairness similar enough to humans for empathy and
>> coordination to work
>>
>> *Embodiment matters* (|cone_adds_shared_features|) - The cone-snout
>> study: changing embodiment features (adding "snout" to the human)
>> improved gaze-following coordination from failure to success
>>
>> *Coordination isn't guaranteed*
>> (|coordination_not_guaranteed_by_similarity|) - Even identical
>> embodiment features don't guarantee successful coordination, as shown
>> by human-to-human failures
>>
>> This formalizes the gradient you described: as similarity increases,
>> coordination quality improves, but there's no deterministic guarantee. The
>> cone-snout example is particularly nice because it shows how specific
>> embodiment features affect what can be intersubjectively stabilized.
>>
>> The formalization also captures the point about lacking "high-quality
>> understanding" - we can model that coordination succeeds or fails, but the
>> structure doesn't claim to explain /why/ the similarities are sufficient in
>> some cases and not others. It just tracks that they matter.
>>
>> -- Formalizing "as if" postures in discourse
>>
>> -- Extended: similarity, embodiment, and coordination failure
>>
>> structure ObjectiveCategory where
>>
>> name : String
>>
>> supposedlyReal : Prop
>>
>> structure EmbodiedInstance (C : ObjectiveCategory) where
>>
>> body : String
>>
>> embodimentFeatures : List String
>>
>> noDisembodiedAccess : Prop
>>
>> intersubjectivelyVerifiable : Prop
>>
>> -- Coordination can succeed or fail
>>
>> inductive CoordinationResult where
>>
>> | success : CoordinationResult
>>
>> | failure : CoordinationResult
>>
>> structure CoordinationAttempt (C : ObjectiveCategory) where
>>
>> instance1 : EmbodiedInstance C
>>
>> instance2 : EmbodiedInstance C
>>
>> result : CoordinationResult
>>
>> -- EXAMPLE 1: Cross-species fairness coordination
>>
>> def fairnessCategory : ObjectiveCategory := {
>>
>> name := "sense of fairness",
>>
>> supposedlyReal := True
>>
>> }
>>
>> def humanInstance : EmbodiedInstance fairnessCategory := {
>>
>> body := "human",
>>
>> embodimentFeatures := ["face", "hands", "upright"],
>>
>> noDisembodiedAccess := True,
>>
>> intersubjectivelyVerifiable := True
>>
>> }
>>
>> def dogInstance : EmbodiedInstance fairnessCategory := {
>>
>> body := "dog",
>>
>> embodimentFeatures := ["snout", "quadruped", "tail"],
>>
>> noDisembodiedAccess := True,
>>
>> intersubjectivelyVerifiable := True
>>
>> }
>>
>> -- We can coordinate on fairness with dogs (enough similarity for
>> empathy)
>>
>> def humanDogFairnessCoordination : CoordinationAttempt
>> fairnessCategory := {
>>
>> instance1 := humanInstance,
>>
>> instance2 := dogInstance,
>>
>> result := CoordinationResult.success
>>
>> }
>>
>> -- EXAMPLE 2: The gaze-following / cone-snout study
>>
>> def gazeCategory : ObjectiveCategory := {
>>
>> name := "gaze direction",
>>
>> supposedlyReal := True
>>
>> }
>>
>> def humanGaze : EmbodiedInstance gazeCategory := {
>>
>> body := "human",
>>
>> embodimentFeatures := ["eyes", "face"],
>>
>> noDisembodiedAccess := True,
>>
>> intersubjectivelyVerifiable := True
>>
>> }
>>
>> def dogGaze : EmbodiedInstance gazeCategory := {
>>
>> body := "dog",
>>
>> embodimentFeatures := ["eyes", "snout"],
>>
>> noDisembodiedAccess := True,
>>
>> intersubjectivelyVerifiable := True
>>
>> }
>>
>> -- Without cone-snout: marginal to poor coordination
>>
>> def humanDogGazeBaseline : CoordinationAttempt gazeCategory := {
>>
>> instance1 := humanGaze,
>>
>> instance2 := dogGaze,
>>
>> result := CoordinationResult.failure
>>
>> }
>>
>> -- With cone-snout: improved coordination due to shared snout feature
>>
>> def humanWithConeSnout : EmbodiedInstance gazeCategory := {
>>
>> body := "human",
>>
>> embodimentFeatures := ["eyes", "face", "snout"],
>>
>> noDisembodiedAccess := True,
>>
>> intersubjectivelyVerifiable := True
>>
>> }
>>
>> def humanDogGazeWithCone : CoordinationAttempt gazeCategory := {
>>
>> instance1 := humanWithConeSnout,
>>
>> instance2 := dogGaze,
>>
>> result := CoordinationResult.success
>>
>> }
>>
>> -- Shared features predicate
>>
>> def hasSharedFeature (C : ObjectiveCategory) (i1 i2 :
>> EmbodiedInstance
>> C) : Prop :=
>>
>> ∃f, f ∈i1.embodimentFeatures ∧f ∈i2.embodimentFeatures
>>
>> -- Theorem: The cone-snout intervention adds shared features
>>
>> theorem cone_adds_shared_features :
>>
>> hasSharedFeature gazeCategory humanWithConeSnout dogGaze ∧
>>
>> (∃f, f = "snout" ∧f ∈humanWithConeSnout.embodimentFeatures ∧f
>> ∈dogGaze.embodimentFeatures) := by
>>
>> constructor
>>
>> · unfold hasSharedFeature humanWithConeSnout dogGaze
>>
>> exists "eyes"
>>
>> · exists "snout"
>>
>> -- EXAMPLE 3: Coordination can fail even between identical instances
>>
>> def humanInstance2 : EmbodiedInstance fairnessCategory := {
>>
>> body := "human",
>>
>> embodimentFeatures := ["face", "hands", "upright"],
>>
>> noDisembodiedAccess := True,
>>
>> intersubjectivelyVerifiable := True
>>
>> }
>>
>> def humanHumanFailure : CoordinationAttempt fairnessCategory := {
>>
>> instance1 := humanInstance,
>>
>> instance2 := humanInstance2,
>>
>> result := CoordinationResult.failure
>>
>> }
>>
>> -- Theorem: Even identical embodiment doesn't guarantee coordination
>>
>> theorem coordination_not_guaranteed_by_similarity :
>>
>> humanInstance.embodimentFeatures =
>> humanInstance2.embodimentFeatures ∧
>>
>> humanHumanFailure.result = CoordinationResult.failure := by
>>
>> constructor
>>
>> · rfl
>>
>> · rfl
> --
--
¡sıɹƎ ןıɐH ⊥ ɐןןǝdoɹ ǝ uǝןƃ
ὅτε oi μὲν ἄλλοι κύνες τοὺς ἐχϑροὺς δάκνουσιν, ἐγὰ δὲ τοὺς φίλους, ἵνα σώσω.
smime.p7s
Description: S/MIME cryptographic signature
.- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. FRIAM Applied Complexity Group listserv Fridays 9a-12p Friday St. Johns Cafe / Thursdays 9a-12p Zoom https://bit.ly/virtualfriam to (un)subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: 5/2017 thru present https://redfish.com/pipermail/friam_redfish.com/ 1/2003 thru 6/2021 http://friam.383.s1.nabble.com/
