Friday, July 26, 2024

Interactive Theorem Provers: Lean & Coq and my journey through them

 Over the years I've gradually gained understanding and ability with Thereom provers. There's a lot of Computer Science and Math knowledge baked into how they work which made it a slow process of understanding them, but I can do a lot of simple proofs and Coq and now Lean of late.

I started with simple Logic proofs, and implications. And the gradually got into natural number proofs and slammed into some stupid walls. You have to make sure you organize your inductions so the inductive hypothesis remains as general as possible.

I went pretty far through the first Software foundations book, and learned how to construct inductive types, use rewriting and some proof by contradiction techniques.

Eventually, I saw a discussion on the prediction market Manifold about when a Blank Slate AI would be able to prove the Infinitude of Primes.

Conceptually, my thought was, give me your finite list of primes. I'll take the biggest one on the list, take the factorial, and add 1, and now I  must have a prime factor of that massive number which cannot be any of the numbers on the list.

I decided to solve the infinitude of primes myself in Coq, mostly starting from scratch and not using a library.

I had already proven stuff about addition and multiplication of natural numbers, so I brought that in, but I ended up writing a lot of proofs about inequalities and subtraction.

Over 6 months, I claw my way forward slowly, building up my base of lemmas. But sometimes I had to go back and add another lemma I needed for a proof.

My first wall was the divmod function, which I recreated the same definition that the Coq standard library used. It basically does both division and multiplication by keeping track of a sort of dual of the remainder and moving one step at a time.

A subtraction based approach has problems with proving termination, which is a topic  I slammed into later, so I'll wait to talk about that.

I learned through this whole 6 months that having ways to decompose operations is so important, and it very hard to decompose the divmod, for a long time.

I gradually managed to work my way through, and I made a big advance when I went back to the Standard library for inspiration and found divmod_spec:


le u y -> let (q',u') := divmod x y q u in

plus x (plus (times (S y) q) (sub y u)) = plus (times (S y) q') (sub y u') /\ le u' y.


Setting up an ax + b situation which the results of divmod was great, and also learning that I could "remember" the two values of a divmod call and work with them enabled me to complete the divmod lemmas I thought I would need.


Next was simple the process of defining the product of a list of items, defining the factorial, and then showing that n! + 1 has to have a prime factor greater than n.

Unfortunately, the intuitive argument that n! + 1 has a prime factor greater than n relies on a descending repeated division process. A nightmare for termination.

Instead I tried to define a decompose fuction. Writing it was difficult in itself, and proving it's termination and how to set up the syntax was hard, but running proofs with decompose was a nightmare.

The Program Fixpoint operation I used to define Decompose spewed all kinds of extra proof terms all over my proofs, and they were all completely unfamiliar concepts to me.

I tried to fight this battle, but for a month or two I was stuck.

I was trying to figure out another way to prove the infinitude of primes idea when I came up with this lemma.

If you have a property of the natural numbers, it either is always false, or else there exists some n which is the minimal or first time the property is true.

We can use this with the property of : does u divide a natural number n, to get the smallest divisor of a number. If a divisor of a number can be factored, then it is not the smallest divisor, either of it's factors would be a smaller divisor.

So we can get a prime divisor for any number n by getting the smallest divisor (other than 1). And we can prove that this divisor of n! + 1 cannot be <= n.

There were still a few battles and chains of additional lemmas, but the final proof in Coq was done soon after that.

Months after finishing the proof in Coq, I kept seeing impressive new efforts in formalizing math in Lean. I tried Lean, but I had troubles setting it up in VS code. After trying several times, I managed to get it working.

I decided to translate my proof of the infinitude of primes into Lean, in order to learn that prover. I am interested in exploring Lean's real numbers and analysis capabilities eventually.

I had a lot of stumbles in the process of understanding Lean, and had another issue with the Lean environment crashing before I got it straightened out.


Several lemmas in the Coq version were left out as the standard library already had the same lemmas for me. I used the existing operations for +, * and -, but I'm using the Coq version of divmod, to avoid a ton of rewriting, but I may reconsider for now.

I've completed all the proofs for add, mul, inequalities, and subtraction and now I'm starting on divmod.


Differences from Lean and Coq:

  • In many cases in Lean, you don't need to finish the obvious last line of the proof. if you rewrite a term, and you get an obvious equality, or a case where assumption would apply, Lean does it automatically.
    • Seems to work for rw and simp mostly.
  • In Coq, reflexivitity is stronger than simpl for equalities proofs, in Lean, simp is stronger.
  • simp completes almost all proofs that it can in Lean, in Coq you usually have to simp and then apply a tactic to finish the proof.
  • No Qed / Defined in Lean, and no end in matches.
  • Lean handles operators for + , *, - with no fiddling about with scopes.
  • Lean handles numbers without trying to decide on Peano or Binary number representations.
  • Lean has a proper Real number type that doesn't require deep study to use.
  • Coq has fold in addition to unfold. I just learned a way to re-"fold" in Lean but it wasn't obvious.
  • Unfolding / refolding expressions in general seems harder in Lean, although I've learned a few more tools to deal with it.
  • if you have a more general statement as an inductive hypothesis, you have to specialize it with a have statement before applying it, in Lean. In Coq it will usually just auto-specialize it.
  • Coq uses in, Lean uses at.
  • Apply at was only available with the Mathlib, I use that a lot. You can do have H2 : result := by apply blah but that's more tedious. Now that I use mathlib exclusively it's not a problem.
  • Lean usually replaces succ n with n + 1, which drove me crazy until I understood that it still could be used in proofs that refer to the successor.
  • Lean normal syntax for a proof is def lemma (params : type), and these params are automatically introduced, and need to be reverted if you want your inductive hypothesis to be most useful.
  • reverting teams seems pretty easy and it's nice to not have to intro when you don't need to revert.
  • Having all the proofs in the Nat scope available with context search is so helpful. This context based search is very helpful in general. 
  • Massive Math library in Lean is nice to have, and I'll eventually explore more of it once I finish formalizing the infinitude of primes again.
  • It appears like termination criteria is easier to work with in Lean. in another project I was toying with I was able to establish well-founded criteria pretty simply.
  • I'm not sure if there's a way to rewrite all references of a term, like in Coq's rewrite ?eq
  • I hated Lean's use of symbols not on the keyboard at first, but I've found the backslash codes for them to be not bad.
  • induction and cases explicitly forcing you to organize proofs better is nice. Instead of just chaotically solving sub-goals without noting it in the proof script.


Monday, July 1, 2024

Space Prince Arrives at the 5th Grade

Saionji Misao seemed like a good enough cover identity. His personal guardian would go by Kaji. He would have Sai as a nickname

`Sai` had been speaking Japanese with his guard team over the past few months. Only having `Kaji` on planet would have made him nervous, but the planet had no Class A threats to his person (or even Class B or C).

His personal staff had insisted on learning local customs around attire, and now he was wearing a rather nice blue suit, and bow tie. Kaji followed me into the school. It was a little early, so I only saw a few students heading to class.

Ms. Kirasawi was my teacher. Other than a few specialist subjects, I would be in her class for the whole day. We had chosen this school because of it's excellent physical fitness program and early leadership program, but I would have to prove to the school that I was capable of its programs.

I would have to go through a few boring years before I could into the best programs in the school. Kaji at least would challenge me to continue my martial arts training.

"Little Star," he said, "I'll be nearby in case anything untoward happens. We've screened the planet, there's no assassins that we can detect. Your third uncle is keeping his eyes on the planet. Fifth Armada is 17 light years away now, but they can divert if needed."

"It would be best if Fifth Armada returns to it's operational program. Have first uncle detach a small squadron to operate within 40 LY of this planet," I said.

There was no reason to keep a whole armada away from the more important defensive positions.

"Yes your highness. Good luck in class."

I opened the door into the classroom, and found only one other student had arrived as of yet.

The girl wore a green dress and didn't even glance over my way as I entered. She was writing on a pad of paper. 

I took a front row seat in the middle, while the girl was sitting two rows back on the right side by the window.

I much preferred the local people's mechanical pencils to the other devices they gave the same name to. My staff promised that they had found the best brand of mechanical pencil for me. There were twelve neatly slotted in a gray case, which also contained a gray eraser.

I pulled out my notebook also, and wrote my Japanese name on the inside cover.

I got distracted thinking about the recent raids on the Epsilon sector, and I started writing a few notes about the situation. It tested my ability to think in Japanese, and I had to pause once to consider how to phrase something.

Rapid Response needed. Raiders are almost guaranteed to be unofficially Seventh Dynasty forces. They are feeling threatened from recent colonization in their sphere of influence. Or our technological advances.

Standard Hyperspace fighters aren't strong enough to resist the raiders. We need a heavy and fast fighter, or a small ship that's inexpensive enough to widely deploy for counter-incursion. And training to recognize and respond. Maybe some work on the planetary defense systems. 

MilProd is still skewed to mainline combat ships, but maybe a slight allocation to this frigate or heavy fighter would help. If we can make them adaptive enough to also be useful in a fleet battle. 

We need to expand supply ships to make up for the lackluster supply situation of hyperspace fighters and frigates. Maybe a periodic resupply circuit to resupply all of these regional response forces.

We could even consider making this part of a political push to reassure local authorities that some decentralization is coming. Put the response forces under local authority, and then replace any incompetent local military leadership.


Many students had already filled in as I looked up. I turned the page to start fresh. Ms. Kirasawi arrived, and soon after the class started.

"Welcome students, welcome, welcome. Most of you are continuing on from last year, but we do have three new students. Ms. Nishio Takeyo. Please stand up. Ms. Takeyo is transferring from Okinawa. She is already recognized for her artwork, and will be working closely with Mrs. Sugi, our art teacher.

Secondly, Ms. Rieko Matsutoya. Ms. Matsutoya has arrived from one of our neighbor schools. Ms. Matsutoya lives with her grandparents and likes to help with their gardening.

Lastly, Mr. Saionji Misao. Mr. Misao, can you introduce yourself? I was not informed on where you have transferred from or your situation?"

I was prepared for this. Best just to alter the facts as little as possible. "Yes Mrs. Kirasawi. My uncle and I have recently moved to Japan. We both worked hard to immerse ourselves in your language so we could be prepared. I believe my uncle has some business opportunities he is pursuing here but I don't know, he doesn't tell me a lot.

I've lived with my uncles since I was four. Um, I like Martial arts, and hope to get into your school's Martial Arts Program."

"Thank you, Mr. Misao," the teacher said. "Now lets begin. Open your history textbooks to the Preface, page XIII."

After reciting the national anthem on that page, they continued on to discuss the earliest history of Japan. Very little was known about Japan before things were altered by Chinese influence. There were a few historical sites and temples with claims to be before Chinese "corruption."

We studied the earliest origins of Shinto and the differences with modern belief. Finally, Ms. Kirasawi switched to math. Using the whiteboard each student was instructed to take a word problem written in Japanese and then solve it out using `Arabic` numerals.

I sighed in relief that my team had identified another language hidden in this world's mathematics, and I was trained on that as well. Quickly, I calculated 23 * 18 = 414.

The school's math instruction was pretty primitive. We jumped around practicing basics like these two digit multiplications, and then working with geometric figures, and then some very practical studies with a tape measure or estimating how many candies were in a small jar. She promised to give anyone a treat who guessed exactly the right answer.

Before long the class broke up, and several classes of students followed along into the stadium. While tiny compared to the public venues I was used to, it was an impressive stadium for a small school like this one.

After we were crowded in the stands, the Physical Fitness instructor amplified his voice and spoke. "Welcome to a new year, beginning again the pursuit of health. All students already classified by ability level, please come on down to the field, join your Group Leaders."

About a third of the students went down onto the field after that.

"Now, for those of you who do not know, we have minimum standards for students who wish to be part of the Physical Fitness program. Senior High students, you must reach a minimum standard of 5 kyu to stay in the program. Students between 1 and 5 kyu will join the Standard Senior High group. For those who reach more advanced levels, we have groups for 1-2 dan, 3 dan and our top student group for those who reach a 4 dan evaluation. So all 9th graders, and Senior High transfers, please come down for evaluation."

Kaji had told me before that most schools on planet weren't that focused on martial arts, the two hour block for Physical Fitness was quite rare. This was one of the school most focused on these arts on planet. Obviously they didn't have any knowledge or ability to train in Transcendent arts, but I still have Kaji to work on that.

Each student being evaluated sparred for a few minutes with one of the student assistants. It was a quick process, with five assistants, and each evaluation only took a minute or so. After 20 minutes, roughly half of those being evaluated were encouraged to train during their own time at home, and left the stadium. They hadn't reached 5 kyu grading he assumed.

Of the students who had reached that standard, some were directed to three student assistants that stood next to the teacher. Others joined the Standard senior high group right away.

A few of the new students were directed to the 1 and 2 dan training group, where the best student of the Senior High group had a chance to spar with the teacher himself.

But after another minute, that student was also directed to the 1 and 2 dan group. After that, Mr. Uesato spoke up again. "For our Junior High students, the minimum standard is an evaluation of 8 kyu. Those of you who reach the 5 kyu student in Junior High will be part of our Advanced Junior High group, and the other qualifiers will be part of the Standard Junior high group. If you have not been evaluated since entering Junior High, come on down."

After another twenty minutes, the Junior High students were evaluated. 

"Lastly, 5th Grade is the youngest age we accept for the program. We are very strict in only accepting the top 5th graders. Those of you who don't make it today, remember, many Junior High students enter the program after not making it in their 5th grade year. It is really just an early training year for our most promising students. 5th graders, please come on down."

I followed our whole class as well as the other 5th grade classes as we went out onto the field. We joined the third of five lines as the same student assistants began sparring with students in front of us.

The assistants seemed to be quite quick and brutal considering the size different between them and the small fifth graders. While I was taller than normal for my grade, these assistants would still loom over me.

There were actually a few fifth graders who cried after being hit by the assistant's blows, but most of the students were silent.

After very quickly going through the students in front of me, I reached the assistant assigned to my line.

I bowed to the girl. "Get ready," she said, and then swiftly approached me and tried to strike my chest with her right palm.

My elbow collided with hers and her strike was adjusted just enough. I responded with a sweep with my right foot, trying to knock her off balance. She wobbled but adjusted her stance, overpowering my returning fist.

I couldn't overpower her volley of kicks, so I darted backwards, and then hit her left side with my right elbow, going past her.

The concentration of qi was a sign of the assistant escalating the fight. I controlled my power level, sticking to what Kaji had showed me was reasonable for a very talented but not ridiculous fifth grader.

The blurring fist of her qi powered blow was deflected by the energy shield formation I formed with quick hand seals.

We were in a tense standoff. Lightning currents were running between the girl's hands but she didn't unleash them yet.

I prepared my hand seals in case this girl's intentions were hostile. The 1st Technique of the Dragon was the least revealing offensive ability I had. I found myself translating mystic language into Japanese and finding that it was a reasonable language for explaining such abilities.

"Enough!" Mr. Uesato said. "This student demonstrated enough skill to enter the Early Elementary Student's Group after 5 seconds. Step back, and your sensei will practice with the bright young student."

"Yes, sensei," the girl said. Lightning disappearing from her hands. She bowed and stepped back.

"Now let's see those hand seals. A rare ability even for Senior High students. We do have a few experts in the more esoteric ways of these seals."

The 1st Technique only took three seals, but they were very precise, and continuing the series into the 2nd Technique required immediately proceeding to use eight more seals.

I stuck to just the 1st Technique. My hands were wreathed in a fire that didn't hurt, but was composed of dozens of tiny sparks which could attack an enemy or deflect the enemy's own attacks.

"A fire technique in three seals? And a flexible one, make the fire wisps attack me," the teacher said.

I did as he said, and he had to step back to have enough time to deal with each of the fire wisps.

"Very impressive, and your name student?"

"Saionji Misao, sir," I said.

"I am restricted by the school board, join the Early Elementary group. But I would like to speak with you after today's session. I have a pass for your teacher."

We had two Senior High students leading our Early Elementary group. From all the 5th grade classes, there were only 5 of us.

Surprisingly, this artist from my classroom, Ms. Takeyo, had also become part of these group. Truly, a girl skilled in multiple areas.

"Don't think about the fancy techniques you hear in stories. Start with our own school's Way of Discipline. When you can perform the first three katas, you can begin to specialize and study a unique art."

We went through a few very simple maneuvers, focusing on basics of footwork, movement of the body and hand position and movement.

Finally, the two hour session was done, and I went to speak with Mr. Uesato. He lead me into his office at the stadium. 

"With power comes responsibility, Mr. Misao. I recognize the technique you used was just the first of a series. The way you immediately stopped, though you had an inclination to continue, gave it away. It is not my place to know how or why you learned a powerful style at such an early age, but Mr. Misao, it is my job to protect my students. Please don't use this series in my class. It is exceptionally difficult to dispel. Students won't be able to avoid it, and someone could be hurt badly.

The only time you may use that technique is sparring with myself or other professionals, if we have specifically asked you to. 

And one more thing, Mr. Misao. While I can't officially assign you to the 1-2 dan group or any Junior High group, I would like to continue your training as our schedules permit. I will approach you in a few weeks after the early foolishness is dealt with."

"Thank you, Mr. Uesato," I said. "May I have the pass for my teacher?"

He wrote something up for me and I headed to lunch. The lunch room was quite full, and so I had to sit with a group of older students.

"Ms. Higashi lost her cool when this kid was able to respond to her attacks," one of the 10th graders said.

"The Ice Queen challenged by a fifth grader?" the girl sitting next to the first boy said.

Another girl said, "She was defeated by our class representative."

"Yeah, he's a legend, that still means she should be more than able to demolish even the world's best 5th grader."

"Hey kid, never saw you in the 4th grade fitness groups. This is the first we've heard about a superstar kid coming up," the first girl said.

"I'm a transfer,' I said. "Saionji Misao. It is good to meet you, senior students."

The boy was Ryosho. The only one of the group still in Mr. Uesato's class. The three girls were Misha, Totsushi (Tots) and Satsushi (Satsu).

"We do some training outside of school. Ryosho has taught us a few things, but we still keep him humble, don't we girls? You should come some time, if your parents are okay with it," Tots said.

"I live with my uncles, I'll see what they think. Let me know where and when."

Lunch was pretty awful. I was going to have Kaji bring something back from home, but I was delayed and never had a chance, plus I couldn't exactly eat a separate meal at a full table of students without attracting attention.

The afternoon lessons with Ms. Kirasawi were rather boring. Science lessons that were hundreds of years old. Really these lessons would maybe have been covered in History of Science. The lesson was at a very high level, covering a summary of scientific areas, like Biology, Chemistry and Physics. Ms. Kirasawi said we would be getting into Chemistry in future sessions and doing some labs. To be cordial, I paid attention as much as I could, and even answered a question when the teacher asked.

After science there were a few minutes of local civics. They were encouraged to ask the road wardens for help if they had any trouble on the way home.

I met up with Kaji after school. We had purchased a house which was quite cheap in the local currency despite it's size. As we walked home, Kaji filled me in on his day.

"I wasn't around at lunch because I was pulled into the Headmistress' office and I had to explain myself. It's a matter of honesty and decorum but not revealing too much. I guess she thinks you are a son of one of the local Imperial family's cadet branches. Basically, akin to your second and third cousins. Of course, you would be under an assumed name. Your performance during the fitness evaluation confirmed that view in her mind.

"I got carried away," I said.

"This girl did too. The Headmistress confirmed the girl goes a bit overboard in everything she does. I will show you another attack series that should be more low key and appropriate for training with your juniors," he said.

"Teacher Uesato recognized that I was used the first attack in a series. I didn't tell him anything but he figured out as much."

"Impressive. Your martial arts teacher is perceptive, well at least you can use this training series. You shouldn't need more than the second step."

They separated from the wave of students as they turned down another street approaching their new home. It wasn't just students, there was nobody on this street at all.

He heard the sound of someone muttering but couldn't find it's source.


* * *

Professor Tsuyame didn't usually travel in this part of the city. As second in command of the road wardens in addition to his study of Hostile Paranormal Entities, he guarded the boundaries of the safe routes to and from the college.

But he had heard someone bought the old mansion in the epicenter of the city's paranormal activity. His studies demanded he get close to the enemy, which meant he needed to be a strong martial artist in addition to scientist.

The first day of school wasn't just significant to students and parents, it was spiritually significant to the enemy. How many times have the unwary been caught out by the relative calm before the start of term? Countless times.

But here it was again, a battle between humans and malevolent beings, caused by the human's stepping away from the safe roadways.

Sometimes the strongest fighters had the biggest stumbling blocks when it came to safety, and he decided that was the case as he came upon the two of them.

The adult caused massive emanations in the force lines as he destroyed smaller spirits one after another, keeping them away from the child. His techniques were lightning aligned.

Foolishly, while he fought the lesser beings, the child fought a greater spirit, something akin to a coyote, the monster snapped his jaws at the boy, and was only barely resisted with a whole technique series.

Fire tattoos glowed on the boy's forehead and on both arms. Spouts of flame blasted the Coyote, and the spirit responded by empowering it's bite still further, and then howling.

"Only until the fifth step, --" the man shouted, and then turned to him. "Who are you?"

"I am Professor Tsuyame with the road wardens, I'm here to help you escape the malevolent spirits. I have some questions after we get back to safety."

The man turned and once again destroyed a wave of minor spirits with his arts.

Professor Tsuyame rushed forward, speaking briefly to the boy. "Go!"

The man finally spoke as the Professor began dissolving the spirit's hook on existence.

"I am Kajihara Nakata, and this is Misao Saionji."

It took only a few applications of the shielding charm, and he had the greater spirit displaced from existence.

Nakata and the boy, Sai, had proceeded to clear the way to retreat, and Professor Tsuyame lead them back away from the danger zone into safety. A couple of spirits even followed into the safe zone, and Tsuyame knew he would have to have a serious conversation with the Chief Warden about increasing patrols in this area and rearranging the safe corridor.

There wasn't a lot of foot traffic where the spirits had impinged on the safe zone, so he retreated with the two to a diner nearby.

As they waited for their food, he asked the two why they were off the safe zone.

The boy spoke up, "I am a bit of a Martial Arts hobbyist. So my uncles researched and found the school here was the best martial arts school in the world. Today was my first day of course.

Last week, we walked back and forth down the same road a dozen times. My uncles' servants went out to get food and supplies for the house, and no one reported any issues. We had heard about the dangers, but we didn't realize it was so serious."

"And this house was outside the safe zone?" the Professor asked.

"We found the place when we were looking for housing in the city. It was a reasonable size for our needs, and less expensive than the other options. We had a little trouble converting our currency at first, so we don't have as much Yen as we originally hoped. The place fit."

"And is this the place?" the Professor asked, showing a polaroid picture.

He could tell from their reactions that it was. The idiots had just doomed themselves. At least the boy was safe.

"Are there any other children in your family here?" he asked. If there was a child in danger at the epicenter, he would take a risk and go in, not before asking for lots of backup of course.

"No other children. My two uncles, and seven personal staff, plus Kaji, chief of security, I guess you could call them."

The boy had seven servants working for him, and not random people but highly skilled? This Kaji's ability to deal with swarming spirits would give him a sure job with the Road wardens or any other organization.

"I'm sorry to tell you, but unless you have one of the five best martial artists in the world, your family and staff are probably dead already."

He was grim. Though he spoke matter-of-factly, he did not make light of any losses to the evil spirits.

"My uncles did not pursue such arts. They are masters of business. Is there anything you can do Kajihara," the boy asked.

"What sorts of threats would our people face at the house?"

"It is a local epicenter of malevolent spirits. Foes much greater then the one Student Misao fought are there," the professor said.

"I am sorry, Little Star. We should find a hotel and rest for the night."

"Stay safe, and keep to the safe roads. Follow the wardens' instructions," he said.

"Thank you, Professor," the boy and his `chief of security` said.


When he got back to headquarters, he reported in to his boss.

"What do you have to report Professor Tsuyame?"

"I have rescued two people. They were off the safe roads. Both of them were skilled martial artists. At least 5 dan by my reckoning."

"What's their excuse?" his boss asked.

"New arrivals. The manor has changed hands again. And most likely, the boy's parents were killed after the spirits showed up for start of term.

"What's this about a boy?"

"One of the two we rescued was a child, maybe 13 or 14? The adult was fighting the minor spirits while the boy fought a major coyote spirit until I intervened."

"A true prodigy."

"The adult told me they had sought out the best Martial Arts primary school and found our school."

"I will keep watch on the school. Find one of your subordinates to watch over the college, and I want you to investigate what will happen next with the manor. How do they keep putting that manor on the market. It's a increasing amount of blood on our hands if we can't get that place off the listings.

"Yes sir."

* * * 

Most of our money was back at the house, the house we couldn't get to. Our fleet communicator was also there. And the people, servants I had known since I was little. And my uncles.

Losing Sumi and Kesaimi, that hit me hardest. And if we needed to go back, how would we communicate with the fleet? If they had feared anything like this, Kaji would have insisted on a regular check in policy with the elite. This was a Class B threat. Not an assassin, but an unforseen danger that truly put them in peril. They would never have come here at all if they knew about it.

Spirits of that kind had been purged from the Kingdom for hundreds of years. To encounter that old danger here, was odd and terrifying.

Sumi and Kesaimi were friends. They were older than him, in their early twenties, but young enough that they could interact and joke without being so formal.

"What if we used Transcendent power, rescue whoever is still alive, and then leave. We can figure out other classes on a world that isn't cursed," I asked Kaji.

"The fleet is too far out. By the time we get here we'll be drowning in assassins and enemy fleets," Kaji said. "You know I wasn't trained for gentleness. You have to take this situation like a soldier, discipline yourself and get revenge. Your Highness, I think we will shape you into a worthy king. You have a mission now, to end these spirits."

"I asked for a challenge. To learn and grow in Martial Arts.  Sumi and Kesaimi had some other training in mind, but my focus will have to be on these arts," I reasoned.

"I need some time to steady myself," I told Kaji.

"I will have to think on our next steps. We will need money to find a new place to stay. I might have to work with the locals to pay our way through the next few years.

"There will be some benefit in this for you too, Uncle."

* *  *

It was a frantic morning as we used the last of our funds to rent a few weeks of room and board at the hotel and get a few simple changes of clothing for each of us.

Staying busy was suitable for me, it kept me from getting mired in my thoughts. I had to keep going for now. Morning classes were not my focus, I let the information come in, and I would work on the two assignments I received tonight, but I was focused on the two hours of Fitness.

I was surprised when I was pulled aside as I was headed with our class over to the stadium

"Mr. Misao, are you aware of the spiritual emanations caused by emotion."

"No ma'am. Spiritual emanations?" I said.

"It's only in extreme cases, but yes. These emanations are a sign my office uses to help those who need counseling. Please follow me," she said.

"But I was headed to the stadium for my fitness class," I said, protesting.

"Come with me, Mr. Misao. Trying to avoid facing your emotions by staying busy, especially with exercise and martial minded hobbies, isn't going to help. I've unfortunately seen it many times."

Reluctantly I followed the staff member to her office.

"I am Assistant Counselor Hara. I'm here to listen, whenever."

I didn’t have anything to say at first.

“I’ve seen a lot of kids not say anything, just holding it all in. The ones who talk recover a lot better.”

"I grew up knowing about death. My mother died six months after my father. It took a long time to find people I could trust. Sami and Kesaimi, I could trust them. We can’t even bury them.”

"Did you know about the safe zones and safe roads when you came here?" the counselor asked.

Really I was letting it all get to me in front of other people. That was embarrassing. I had to be better for my people.

"No. We heard about dangers but we had seen warnings for many of the places we checked, so we just thought it was local fears, and we would be able to deal with whatever we encountered."

"The city needs to do everything to make the dangers more apparent. This happens multiple times a year, unfortunately. Not always with someone going to the school here, but often. Your home was outside the safe zone, and it was attacked by the spirits?"

"Kaji and I encountered the spirits on the way to our new house. We had been there for a few days prior with no trouble, but yesterday, we were suddenly faced with a lot of spirits. Hundreds of minor spirits and a major spirit.

Professor Tsuyame arrived, and help us escape from the swarm. He said there was no way we could reach our house without a huge group of the best martial artists in town. So we had to go rent a hotel room last night. A lot of our money was in that house too.

Sumi and Kesaimi were two members of my personal staff. My uncle was there also. He was in charge of the household. And there were other personal staff, cooks, people to look after Uncle and myself. Now Kaji is going to look for work so we can pay for a place to live."

"I know the Professor quite well. If he was involved, this was no minor incursion of spirits around your house. Mr. Kaji should spend some time at the college studying warding. It is an important subject regionally, to know how to protect your home. There are many passive ways to defend the home from spirits, in addition to active techniques. The Japanese board of tourism really should warn about this region."

"I wanted to go home, but we don't have any quick way to do that, and Kaji convinced me to work harder, to make something out of a bad thing. So that's why I want to go to Fitness,"
I said.

"Come back tomorrow also, and then maybe we'll find a different time of day for counseling. This is not a minor thing, Mr. Misao. Losing family and friends is not something you'll got over in a few days.

* * * 

Mr. Uesato stormed into the head counselor's office. "You pulled my newest star out of class? Who do you think you are?"

He leaned against the woman's desk. She was just a staff person. Unless the Headmistress approved it, he would release Student Misao from the Counseling department. They would hold onto students for months, keeping them away from important classes, including his own.

"Did you hear about the battle near Hondou road yesterday? Hundreds of minor spirits defeated, and a coyote-type major spirit."

"What does that have to do with this?" he asked.

"Student Misao and his security detail defeated most of those," the counselor said.

"All the more reason to continue the young student's training."

"They say they were headed to a house they just purchased last week," she said.

"during the Calm -- The manor, those idiots. Why do the strongest students have the worst parents?"

"We don't know it was the manor, but according to what I've heard, the battle Student Misao was in was just the outermost region of a massive conflagration of spirits. Whoever was still at the manner is surely dead now."

"And so, Student Misao needs counseling."

"In some ways, he is doing quite well, all things considered. I will reach out to the city about his situation.”

***

I actually got to the cafeteria on time, and ended up sitting with three girls in my class. They invited me to sit there.

One of them was Ms. Takeyo the other girl from class in my fitness group.

Ms. Ueyemi, Ms. Picard (an odd name I thought), and Ms. Mitikihara were the other three girls.

“Fighting the Ice Queen, are you really a fifth grader,” Ueyemi asked. 

Takeyo ignored her saying, “we’ve got a little training group going, if you want to stop by sometime.”

First the senior high students and now fifth graders. Did every friend group have a sparring club?

“We’ve been calling her the Phantasm, Takeyo can make her art real, and just a fifth grader and now we have to come up with a nickname for you?” Picard said.

“You don’t have to,” I said.

I had fought the spirits the day before so it didn’t take more than a moment to recognize the cause of the sudden disturbance.